cubical-0.2.0: examples/equivTotal.cub

module equivTotal where

import elimEquiv

-- equivalence on total space

lem3Sub : (A:U) (P: A -> U) (a:A) -> Id U (Sigma (singl A a) (\ z -> P z.1)) (P a)
lem3Sub A P a = lemContrSig (singl A a) (singContr A a) (\ x -> P x.1) (a,refl A a)

-- a corollary of equivalence

allTransp : (A B : U) -> hasSection (Id U A B) (Equiv A B) (IdToEquiv A B)
allTransp A B = equivSec (Id U A B) (Equiv A B)  (IdToEquiv A B) (univAx A B)

-- an induction principle for isEquiv

transpRef : (A : U) -> Id (A->A) (id A) (transport A A (refl U A))
transpRef A = funExt A (\ _ -> A) (id A) (transport A A (refl U A)) (transportRef A)

elimIsEquiv : (A:U) -> (P : (B:U) -> (A->B) -> U) -> P A (id A) -> 
              (B :U) -> (f : A -> B) -> isEquiv A B f -> P B f
elimIsEquiv A P d = \ B f if -> rem2 B (f,if)
 where 
  rem1 : P A (transport A A (refl U A))
  rem1 = subst (A->A) (P A) (id A) (transport A A (refl U A)) (transpRef A) d

  rem : (B:U) -> (p:Id U A B) -> P B (transport A B p)
  rem = J U A (\ B p ->  P B (transport A B p)) rem1

  rem2 : (B:U) -> (p:Equiv A B) -> P B p.1
  rem2 B = allSection (Id U A B) (Equiv A B) (IdToEquiv A B) (allTransp A B) 
                (\ p -> P B p.1) (rem B)

-- a simple application; with the problem with eta conversion resolved

equivSigId : (A B :U) (f:A -> B) 
         -> isEquiv A B f -> (Q : B -> U) -> Id U (Sigma A (\ x -> Q (f x))) (Sigma B Q)
equivSigId A = elimIsEquiv A P (\ Q -> refl U (Sigma A Q))
 where 
   P : (B:U) -> (A-> B) -> U
   P B f =  (Q : B -> U) -> Id U (Sigma A (\ x -> Q (f x))) (Sigma B Q)

-- application to equivalences between total spaces

liftTot :  (A:U) (P Q : A -> U) (g : (x:A) -> P x -> Q x) -> Sigma A P -> Sigma A Q
liftTot A P Q g z = (z.1,g z.1 z.2)

lem3Sub : (A:U) (P: A -> U) (a:A) -> Id U (Sigma (singl A a) (\ z -> P z.1)) (P a)
lem3Sub A P a = lemContrSig (singl A a) (singContr A a) (\ x -> P x.1) (a,refl A a)

lem2Sub : (A:U) (P: A -> U) (a:A) 
         -> Id U (fiber (Sigma A P) A (\x -> x.1) a) 
                 (Sigma (Sigma A (\ x -> Id A x a)) (\ z -> P z.1))
lem2Sub A P a = 
 isoId F T (\ u -> ((u.1.1,u.2),u.1.2)) (\ v -> ((v.1.1,v.2),v.1.2)) (refl T) (refl F)
  where
   T : U
   T = Sigma (Sigma A (\ x -> Id A x a)) (\ z -> P z.1)

   F : U
   F = fiber (Sigma A P) A (\x -> x.1) a

lem1Sub : (A:U) (P: A -> U) (a:A) -> Id U (fiber (Sigma A P) A (\ z -> z.1) a) (P a)
lem1Sub A P a =
 comp U (fiber (Sigma A P) A (\ x -> x.1) a) 
        (Sigma (singl A a) (\ z -> P z.1)) (P a) (lem2Sub A P a) (lem3Sub A P a)

equivTot : (A:U) (P Q : A -> U) (g : (x:A) -> P x -> Q x) ->
           isEquiv (Sigma A P) (Sigma A Q) (liftTot A P Q g) -> (a:A) -> Id U (P a) (Q a)
equivTot A P Q g igl a = rem5
 where
  F : Sigma A P -> U
  F z = Id A z.1 a

  T : U
  T = Sigma (Sigma A P) F

  G : Sigma A Q -> U
  G z = Id A z.1 a

  V : U
  V = Sigma (Sigma A Q) G

  rem : Id U T (P a)
  rem = lem1Sub A P a

  rem1 : Id U V (Q a)
  rem1 = lem1Sub A Q a

  F1 : Sigma A P -> U
  F1 z = G (liftTot A P Q g z)

  T1 : U
  T1 = Sigma (Sigma A P) F1

  rem2 : Id U T1 V
  rem2 = equivSigId (Sigma A P) (Sigma A Q) (liftTot A P Q g) igl G

  rem3 : Id U T T1
  rem3 = mapOnPath (Sigma A P -> U) U (Sigma (Sigma A P)) F F1 eFF1
      where fFF1 : (z : Sigma A P) -> Id U (F z) (F1 z)
            fFF1 z = refl U (Id A z.1 a)

            eFF1 : Id (Sigma A P -> U) F F1
            eFF1 = funExt (Sigma A P) (\ _ -> U) F F1 fFF1

  rem4 : Id U T V
  rem4 = comp U T T1 V rem3 rem2

  rem5 : Id U (P a) (Q a)
  rem5 = compUp U T (P a) V (Q a) rem rem1 rem4

-- now we should be able to show that any map Id (Pi A B) f g -> (x:A) -> Id (B x) (f x) (g x)
-- is an equivalence

singlPi : (A:U) (B:A->U) -> Pi A B -> Pi A B -> U
singlPi A B g f = (x:A) -> Id (B x) (f x) (g x)

singlPiContr : (A:U) (B:A->U) (g:Pi A B) -> contr (Sigma (Pi A B) (singlPi A B g))
singlPiContr A B g = subst U contr  ((x:A) -> Sigma (B x) (C x)) (Sigma (Pi A B) (\ z -> (x:A) -> C x (z x))) rem1 rem
 where
  C : (x:A) -> B x -> U
  C x y = Id (B x) y (g x)

  rem : contr ((x:A) -> Sigma (B x) (C x))
  rem = isContrProd A (\ x -> Sigma (B x) (C x)) (\ x -> singContr (B x) (g x))

  rem1 : Id U ((x:A) -> Sigma (B x) (C x)) (Sigma (Pi A B) (\ z -> (x:A) -> C x (z x)))
  rem1 = idTelProp A B C

-- we have enough to deduce that Id (Pi A B) f g and (x:A) -> Id (B x) (f x) (g x) are equal
eqIdProd : (A:U) (B:A->U) -> (f g : Pi A B) -> Id U (Id (Pi A B) f g) ((x:A) -> Id (B x) (f x) (g x))
eqIdProd A B f g = equivTot T P Q G rem f
 where 
  P : (Pi A B) -> U
  P z = Id (Pi A B) z g

  Q : (Pi A B) -> U
  Q z = (x:A) -> Id (B x) (z x) (g x)

  T : U
  T = Pi A B

  G : (z:Pi A B) -> P z -> Q z
  G z ez x = mapOnPath (Pi A B) (B x) (\ u -> u x) z g ez

  rem1 : contr (Sigma T P)
  rem1 = singContr (Pi A B) g

  rem2 : contr (Sigma T Q)
  rem2 = singlPiContr A B g

  rem : isEquiv (Sigma T P) (Sigma T Q) (liftTot T P Q G)
  rem = equivContr (Sigma T P) rem1 (Sigma T Q) rem2 (liftTot T P Q G)

-- it follows from this that a product of sets is a set

isSetProd : (A:U) (B:A->U) (pB : (x:A) -> set (B x)) -> set (Pi A B)
isSetProd A B pB f g = substInv U prop  (Id (Pi A B) f g) ((x:A) -> Id (B x) (f x) (g x)) rem2 rem1
 where
  rem : (x:A) -> prop (Id (B x) (f x) (g x))
  rem x = pB x (f x) (g x)

  rem1 : prop ((x:A) -> Id (B x) (f x) (g x))
  rem1 = isPropProd A (\ x -> Id (B x) (f x) (g x)) rem

  rem2 : Id U (Id (Pi A B) f g) ((x:A) -> Id (B x) (f x) (g x))
  rem2 = eqIdProd A B f g