cubical-0.2.0: examples/epi.cub

-- the notion of surjection functions

module epi where

import omega
import exists

-- surjective and epi maps

isEpi : (A B: U) -> (A -> B) -> U
isEpi A B f = (X:U) -> set X -> (g h:B->X) -> Id (A->X) (\ a -> g (f a)) (\ a -> h (f a)) -> Id (B->X) g h

isSurj : (A B:U) -> (A->B) -> U
isSurj A B f = (y:B) -> exists A (\ x -> Id B (f x) y)

-- these properties should be equivalent

surjIsEpi : (A B : U) (f : A -> B) -> isSurj A B f -> isEpi A B f
surjIsEpi A B f sf X sX g h egh = funExt B (\ _ -> X) g h rem
 where
  rem : (y:B) -> Id X (g y) (h y)
  rem y = rem6
    where
     G : U
     G = Id X (g y) (h y)

     rem1 : prop G
     rem1 = sX (g y) (h y)

     rem2 : exists A (\ x -> Id B (f x) y)
     rem2 = sf y

     rem4 : (x:A) -> Id X (g (f x)) (h (f x))
     rem4 a = appId A X a (\ x -> g (f x)) (\ x -> h (f x)) egh

     rem3 : (x:A) -> Id B (f x) y -> G
     rem3 x p = subst B (\ z -> Id X (g z) (h z)) (f x) y p (rem4 x)

     rem5 : (Sigma A (\ x -> Id B (f x) y)) -> G
     rem5 z = rem3 z.1 z.2

     rem6 : G
     rem6 = exElim A (\ x -> Id B (f x) y) G rem1 rem5 rem2

-- the converse is interesting

epiIsSurj : (A B : U) (f : A -> B) -> isEpi A B f -> isSurj A B f
epiIsSurj A B f ef = rem6
 where 
   rem : (g h : B -> Omega) -> Id (A -> Omega) (\ x -> g (f x)) (\ x -> h (f x)) -> Id (B -> Omega) g h
   rem = ef Omega omegaIsSet

   g : B -> Omega
   g y = (Unit,propUnit)

   h : B -> Omega
   h y =  (exists A (\ x -> Id B (f x) y),squash (Sigma A (\ x -> Id B (f x) y)))

   rem1 : (x:A) -> isTrue (h (f x))
   rem1 x = inc (Sigma A (\ z -> Id B (f z) (f x))) (x,refl B (f x))

   rem2 : (x:A) -> Id Omega (g (f x)) (h (f x))
   rem2 x = lemIsTrue (g (f x)) (h (f x)) (\ _ -> rem1 x) (\ _ -> tt)

   rem3 : Id (A -> Omega) (\ x -> g (f x)) (\ x -> h (f x))
   rem3 = funExt A (\ _ -> Omega)  (\ x -> g (f x)) (\ x -> h (f x)) rem2

   rem4 : Id (B -> Omega) g h 
   rem4 = rem g h rem3

   rem5 : (y:B) -> Id Omega (g y) (h y)
   rem5 y = appId B Omega y g h rem4

   rem6 : (y:B) -> isTrue (h y)
   rem6 y = subst Omega isTrue (g y) (h y) (rem5 y) tt