done with the definition of two (maybe)

examples/collection.cub

@@ -1,6 +1,5 @@
 module collection where
 
-import axChoice
 import sigma
 import univalence
 

examples/function1.cub

@@ -0,0 +1,117 @@
+module function1 where
+
+import sigma
+
+-- some general facts about functions
+
+-- g is a section of f
+section : (A B : U) (f : A -> B) (g : B -> A) -> U
+section A B f g = (b : B) -> Id B (f (g b)) b
+
+injective : (A B : U) (f : A -> B) -> U
+injective A B f = (a0 a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1
+
+retract : (A B : U) (f : A -> B) (g : B -> A) -> U
+retract A B f g = section B A g f
+
+retractInj : (A B : U) (f : A -> B) (g : B -> A) ->
+             retract A B f g -> injective A B f
+retractInj A B f g h a0 a1 h' =
+  compUp A (g (f a0)) a0 (g (f a1)) a1 rem1 rem2 rem3
+  where
+  rem1 : Id A (g (f a0)) a0
+  rem1 = h a0
+
+  rem2 : Id A (g (f a1)) a1
+  rem2 = h a1
+
+  rem3 : Id A (g (f a0)) (g (f a1))
+  rem3 = mapOnPath B A g (f a0) (f a1) h'
+
+hasSection : (A B : U) -> (A -> B) -> U
+hasSection A B f = Sigma (B -> A) (section A B f)
+
+-- isContr
+
+lemPropAnd : (A B :U) -> prop A -> (A -> prop B) -> prop (and A B)
+lemPropAnd A B = propSig A (\ _ -> B)
+
+isContr : U -> U
+isContr A = and (prop A) A
+
+isContrProp : (A:U) -> prop (isContr A)
+isContrProp A = lemPropAnd (prop A) A (propIsProp A) (\ h -> h)
+
+fiber : (A B:U) -> (A->B) -> B -> U
+fiber A B f y = (x:A) * Id B (f x) y
+
+isEquiv : (A B:U) -> (A->B) -> U
+isEquiv A B f = (y:B) -> isContr (fiber A B f y)
+
+idIsEquiv : (A:U) -> isEquiv A A (\ x -> x)
+idIsEquiv A y = (rem1 y,rem2 y)
+ where
+  T : A -> U
+  T = fiber A A (\ x -> x)
+
+  rem2 : (y:A) -> T y
+  rem2 y = (y,refl A y)
+
+  rem : (y x:A) (p:Id A y x) (x':A) (p':Id A y x') -> Id (T y) (x,inv A y x p) (x',inv A y x' p')
+  rem y = J A y (\ x p -> (x':A) (p':Id A y x') -> Id (T y) (x,inv A y x p) (x',inv A y x' p')) lem
+   where lem : (x':A) (p':Id A y x') -> Id (T y) (y,refl A y) (x',inv A y x' p')
+         lem = J A y (\ x' p' -> Id (T y) (y,refl A y) (x',inv A y x' p')) (refl (T y) (y,refl A y))
+
+  rem1 : (y:A) -> prop (fiber A A (\ x -> x) y)
+  rem1 y f f' = rem y f.1 (inv A f.1 y f.2) f'.1 (inv A f'.1 y f'.2)
+
+propIsEquiv : (A B : U) -> (f : A -> B) -> prop (isEquiv A B f)
+propIsEquiv A B f = propPi B (\ y -> isContr (fiber A B f y))
+                             (\ y -> isContrProp (fiber A B f y))
+
+isEquivEq : (A B : U) -> (f : A -> B) -> isEquiv A B f -> Id U A B
+isEquivEq A B f is = isoId A B f g s t
+ where
+   rem1 : (y:B) -> prop (fiber A B f y)
+   rem1 y = (is y).1
+
+   rem2 : (y:B) -> fiber A B f y
+   rem2 y = (is y).2
+
+   g : B -> A
+   g y = (rem2 y).1
+
+   s : (y:B) -> Id B (f (g y)) y
+   s y = (rem2 y).2
+
+   rem3 : (x:A) -> Id B (f (g (f x))) (f x)
+   rem3 x = s (f x)
+
+   rem4 : (x:A) -> Id (fiber A B f (f x)) (g (f x),rem3 x) (x,refl B (f x))
+   rem4 x = rem1 (f x) (g (f x),rem3 x) (x,refl B (f x))
+
+   t : (x:A) -> Id A (g (f x)) x
+   t x = mapOnPath (fiber A B f (f x)) A (\ z -> z.1)  (g (f x),rem3 x) (x,refl B (f x)) (rem4 x)
+
+-- a test
+
+isEquivSection : (A B : U) (f : A -> B) (g : B -> A) -> section A B f g ->
+                 ((b : B) -> prop (fiber A B f b)) -> isEquiv A B f
+isEquivSection A B f g sfg h b = (h b,(g b,sfg b))
+
+injProp : (A B : U) (f : A -> B) -> injective A B f -> prop B -> prop A
+injProp A B f injf pB a0 a1 = injf a0 a1 (pB (f a0) (f a1))
+
+injId : (X : U) -> injective X X (id X)
+injId X a0 a1 h = h
+
+involutive : (A : U) -> (A -> A) -> U
+involutive A f = section A A f f
+
+-- one should deduce
+
+Equiv : U -> U -> U
+Equiv A B = Sigma (A->B) (isEquiv A B)
+
+lemIdEquiv : (A B:U) (f g : Equiv A B) -> Id (A->B) f.1 g.1 -> Id (Equiv A B) f g
+lemIdEquiv A B = eqPropFam (A->B) (isEquiv A B) (propIsEquiv A B)

examples/gradLemma.cub

@@ -1,6 +1,6 @@
 module gradLemma where
 
-import axChoice
+import function1
 
 corrstId : (A : U) (a : A) -> prop (fiber A A (id A) a)
 corrstId A a v0 v1 =

examples/join.cub

@@ -254,6 +254,14 @@ s3ToS1JoinS1Inv =
         (mapJoin S1 S1 (join Bool Bool) S1 bjbToS1Inv.1 (\z -> z) x)))
   ,refl S3 north)
 
+-- The map e from 7.3
+s3ToS1JoinS1 : ptMap ptS3 (ptJoin (ptS1) S1)
+s3ToS1JoinS1 =
+  (\x -> mapJoin (join Bool Bool) S1 S1 S1 bjbToS1.1 (\z -> z)
+          (r2l Bool Bool S1
+            (mapJoin Bool S2 Bool (join Bool S1) (\b -> b) (suspJoin S1)
+              (suspJoin S2 x)))
+  ,refl (join S1 S1) (inl base))
 
 -- The main map alpha from 8
 alpha : join S1 S1 -> S2

examples/loopTrunc.cub

@@ -20,3 +20,14 @@ kappa n A todo p = subst (trunc (suc n) A.1) (\x -> (truncPath A n todo x).1)
 kappaIsPt : (n : N) (A : ptType) (todo : truncated (suc n) (truncType n)) ->
             isPtMap (Omega (ptTrunc (suc n) A)) (ptTrunc n (Omega A)) (kappa n A todo)
 kappaIsPt n A todo = refl (trunc n (Omega A).1) (inc (refl A.1 (pt A)))
+
+
+kappaOne : (A : ptType) -> (Omega (ptTrunc two A)).1 -> trunc one (Omega A).1
+kappaOne A = kappa one A groupoidSET
+
+
+kappaTwo : (A : ptType) -> (Omega (ptTrunc three A)).1 -> trunc two (Omega A).1
+kappaTwo A = kappa two A twogroupoidGROUPOID
+
+ptKappaTwo : (A : ptType) -> ptMap (Omega (ptTrunc three A)) (ptTrunc two (Omega A))
+ptKappaTwo A = (kappaTwo A, kappaIsPt two A twogroupoidGROUPOID)

examples/pi4s3.cub

@@ -0,0 +1,29 @@
+module pi4s3 where
+
+import hopf
+import truncHopf
+import loopTrunc
+
+firstMap : Z -> (itOmega three ptS2).1
+firstMap n =
+  (itMapOmega three (ptJoin ptS1 S1) ptS2 ptAlpha).1
+    ((itMapOmega three ptS3 (ptJoin ptS1 S1) s3ToS1JoinS1).1
+      ((itMapOmega two ptS2 (Omega ptS3) (sigma ptS2)).1
+        ((mapOmega ptS1 (Omega ptS2) (sigma ptS1)).1 (loopIt n))))
+
+lastMap : (itOmega three (ptJoin ptS1 S1)).1 -> Z
+lastMap x = encode base (pi2S2
+  (kappaOne (Omega ptS2)
+    ((mapOmega (Omega (trS2,inc north)) (ptTrunc two (Omega ptS2)) (ptKappaTwo ptS2)).1
+      (pi3S3 
+        ((itMapOmega three (ptJoin ptS1 S1) ptS3 s3ToS1JoinS1Inv).1 x)))))
+
+composition : Z -> Z
+composition n = lastMap (hopfLoop (firstMap n))
+
+oneZ : Z
+oneZ = sucZ zeroZ
+
+brunerie : Z
+brunerie = composition oneZ
+

examples/truncHopf.cub

@@ -0,0 +1,137 @@
+module truncHopf where
+
+import trunc
+import mult
+
+
+apInc : (A : U) (a b : A) (p : Id A a b) -> Id (trunc three A) (inc a) (inc b)
+apInc A = mapOnPath A (trunc three A) inc
+
+trS2 : U
+trS2 = trunc three S2
+
+trS2Trunc : truncated three trS2
+trS2Trunc = truncIsTrunc three S2
+
+incSouthPath : (x : S1) -> Id trS2 (inc south) (inc south)
+incSouthPath x =
+  apInc S2 south south (compInv S2 north south south (merid base) (merid x))
+
+multTwoSouth : S2 -> trS2
+multTwoSouth = hsplit (\_ -> trS2) with
+  north   -> inc south
+  south   -> inc south
+  merid x -> incSouthPath x
+
+
+meridIncSouth : (x y : S1) -> Id trS2 (inc north) (inc south)
+meridIncSouth x y = comp trS2 (inc north) (inc south) (inc south)
+  (apInc S2 north south (merid x)) (incSouthPath y)
+
+idIncNS : U
+idIncNS = Id trS2 (inc north) (inc south)
+
+-- |p|^1 . | !p0 . q |^1
+auxComp : (a b : S2) (p p0 q : Id S2 a b) -> Id trS2 (inc a) (inc b)
+auxComp a b p p0 q = comp trS2 (inc a) (inc b) (inc b)
+  (apInc S2 a b p) (apInc S2 b b (compInv S2 a b b p0 q))
+
+auxCompId : (a b : S2) (p p0 q : Id S2 a b) -> U
+auxCompId a b p p0 q = Id (Id trS2 (inc a) (inc b)) (auxComp a b p p0 q) (auxComp a b q p0 p)
+
+alpha : (a b : S2) (p0 q : Id S2 a b) -> auxCompId a b p0 p0 q
+alpha a = J S2 a (\b p0 -> (q : Id S2 a b) -> auxCompId a b p0 p0 q)
+  (\q -> compIdl trS2 (inc a) (inc a) (apInc S2 a a q))
+
+beta : (a b : S2) (p0 p : Id S2 a b) -> auxCompId a b p p0 p0
+beta a = J S2 a (\b p0 -> (p : Id S2 a b) -> auxCompId a b p p0 p0)
+           (\p -> compInvIdl trS2 (inc a) (inc a) (apInc S2 a a p))
+
+alphaEqBetaDiag : (a b : S2) (p0 : Id S2 a b) ->
+                  Id (auxCompId a b p0 p0 p0) (alpha a b p0 p0) (beta a b p0 p0)
+alphaEqBetaDiag a =
+ J S2 a (\b p0 -> Id (auxCompId a b p0 p0 p0) (alpha a b p0 p0) (beta a b p0 p0))
+   (refl (auxCompId a a (refl S2 a) (refl S2 a) (refl S2 a))
+     (alpha a a (refl S2 a) (refl S2 a)))
+
+
+
+-- lemSetTorus : (E : S1 -> S1 -> U) (sE : set (E base base))
+--               (f : (y:S1) -> E base y) (g : (x:S1) -> E x base)
+--               (efg : Id (E base base) (f base) (g base)) (x y:S1) -> E x y
+
+multTwoMeridMerid : (x y : S1) -> Id idIncNS (meridIncSouth x y) (meridIncSouth y x)
+multTwoMeridMerid =
+  lemSetTorus E sE
+    (\x -> alpha north south (merid base) (merid x))
+    (\x -> beta north south (merid base) (merid x))
+    (alphaEqBetaDiag north south (merid base))
+  where E : S1 -> S1 -> U
+        E x y = Id idIncNS (meridIncSouth x y) (meridIncSouth y x)
+
+        sE : set (E base base)
+        sE = truncIsTrunc three S2 (inc north) (inc south)
+               (meridIncSouth base base) (meridIncSouth base base)
+
+multTwoMerid : (x : S1) (y : S2) -> Id trS2 (inc y) (multTwoSouth y)
+multTwoMerid x = hsplit (\y -> Id trS2 (inc y) (multTwoSouth y)) with
+  north   -> apInc S2 north south (merid x)
+  south   -> incSouthPath x
+  merid y -> substPathPi S2 trS2 inc multTwoSouth north south (merid y)
+                (apInc S2 north south (merid x))
+                (incSouthPath x) (multTwoMeridMerid x y)
+
+-- ts: IdS S2 (\y -> Id trS2 (inc y) (multTwoSouth y)) north south (merid y) (apInc S2 north south (merid x)) (incSouthPath x)
+
+multTwo : S2 -> S2 -> trS2
+multTwo = hsplit (\_ -> S2 -> trS2) with
+  north   -> inc
+  south   -> multTwoSouth
+  merid x -> funExt S2 (\_ -> trS2) inc multTwoSouth (multTwoMerid x)
+
+lemPropS2 : (P:S2 -> U) (pP:(x:S2) -> prop (P x)) -> P north -> (x:S2) -> P x
+lemPropS2 P pP pN = hsplit P with
+  north -> pN
+  south -> subst S2 P north south (merid base) pN
+  merid x -> rem1
+   where
+    pS : S1 -> P south
+    pS x = subst S2 P north south (merid x) pN
+
+    rem : (p: P south) -> IdS S2 P north south (merid x) pN p
+    rem p = idSIntro S2 P north south (merid x) pN p (pP south (pS x) p)
+
+    rem1 : IdS S2 P north south (merid x) pN (pS base)
+    rem1 = rem (pS base)
+
+multTwoTilde : S2 -> trS2 -> trS2
+multTwoTilde x = truncRec three S2 trS2 trS2Trunc (multTwo x)
+
+multTwoTildeEquiv : (x : S2) -> isEquiv trS2 trS2 (multTwoTilde x)
+multTwoTildeEquiv = 
+  lemPropS2 (\x -> isEquiv trS2 trS2 (multTwoTilde x)) (\x -> propIsEquiv trS2 trS2 (multTwoTilde x))
+    multEquivNorth
+  where multNorthEqId : Id (trS2 -> trS2) (\x -> x) (multTwoTilde north)
+        multNorthEqId = funExt trS2 (\_ -> trS2) (\x -> x) (multTwoTilde north)
+                          (lem3Trunc S2 trS2 three trS2Trunc (\x -> x) (multTwoTilde north)
+                            (\a -> refl trS2 (inc a)))
+        multEquivNorth : isEquiv trS2 trS2 (multTwoTilde north)
+        multEquivNorth = subst (trS2 -> trS2) (isEquiv trS2 trS2) (\x -> x)
+                           (multTwoTilde north) multNorthEqId (idIsEquiv trS2)
+
+
+tHopf3 : S3 -> U
+tHopf3 = hsplit (\_ -> U) with
+  north   -> trS2
+  south   -> trS2
+  merid x -> isEquivEq trS2 trS2 (multTwoTilde x) (multTwoTildeEquiv x)
+
+tHopf3Omega2 : (itOmega two ptS3).1 -> U
+tHopf3Omega2 = itFibOmega two ptS3 tHopf3 (inc north)
+
+-- e_3 from 10.2
+pi3S3 : (itOmega three ptS3).1 -> (itOmega two (trS2,inc north)).1
+pi3S3 p = subst (itOmega two ptS3).1 tHopf3Omega2 point point p
+   (refl (Id trS2 (inc north) (inc north)) (refl trS2 (inc north)))
+  where point : (itOmega two ptS3).1
+        point = pt (itOmega two ptS3)

examples/univalence.cub

@@ -35,9 +35,9 @@ corUnivAx A B = isEquivEq (Id U A B) (Equiv A B) (IdToEquiv A B) (univAx A B)
 
 -- a simple application
 
-idPropIsProp : (A B : U) -> prop A -> prop B -> prop (Id U A B)
-idPropIsProp A B pA pB = substInv U prop (Id U A B) (Equiv A B) (corUnivAx A B) rem
- where
-  rem : prop (Equiv A B)
-  rem = sigIsProp (A->B) (isEquiv A B) (propIsEquiv A B) (isPropProd A (\ _ -> B) (\ _ -> pB))
+-- idPropIsProp : (A B : U) -> prop A -> prop B -> prop (Id U A B)
+-- idPropIsProp A B pA pB = substInv U prop (Id U A B) (Equiv A B) (corUnivAx A B) rem
+--  where
+--   rem : prop (Equiv A B)
+--   rem = sigIsProp (A->B) (isEquiv A B) (propIsEquiv A B) (isPropProd A (\ _ -> B) (\ _ -> pB))