From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 14 Apr 2016 18:13:02 +0000 (-0400)
Subject: Finish binnat example and add elimination principles for equivalences and isomorphisms
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=51d1d2943b57c868ec0e46325514d8fc58dd0919;p=cubicaltt.git

Finish binnat example and add elimination principles for equivalences and isomorphisms
---

diff --git a/examples/binnat.ctt b/examples/binnat.ctt
index 90c2a7d..5f0818d 100644
--- a/examples/binnat.ctt
+++ b/examples/binnat.ctt
@@ -1,10 +1,7 @@
 module binnat where
 
--- import function
-import hedberg
-import equiv
+import univalence
 import nat
--- import elimEquiv
 
 -- Positive binary numbers like in Coq
 data pos = pos1
@@ -64,198 +61,164 @@ NtoPosSuc : (n : nat) -> neg (Id nat zero n) -> Id pos (NtoPos (suc n)) (sucPos
   zero -> \(p : neg (Id nat zero zero)) -> efq (Id pos (NtoPos (suc zero)) (sucPos (NtoPos zero))) (p (<_> zero))
   suc n -> \(_ : neg (Id nat zero (suc n))) -> <_> (sucPos (NtoPos' n))
 
--- NtoPosK : retract pos N PosToN NtoPos
--- NtoPosK p = posInd (\p -> Id pos (NtoPos (PosToN p)) p) (refl pos pos1) hS p
---  where
---   hS : (p : pos) ->
---        Id pos (NtoPos (PosToN p)) p ->
---        Id pos (NtoPos (PosToN (sucPos p))) (sucPos p)
---   hS p hp =
---     let H1 : Id pos (NtoPos (PosToN (sucPos p))) (NtoPos (suc (PosToN p)))
---         H1 = mapOnPath N pos NtoPos (PosToN (sucPos p)) (suc (PosToN p)) (sucPosSuc p)
 
---         H2 : Id pos (NtoPos (suc (PosToN p))) (sucPos (NtoPos (PosToN p)))
---         H2 = NtoPosSuc (PosToN p) (zeronPosToN p)
+NtoPosK (p:pos) : Id pos (NtoPos (PosToN p)) p
+ = posInd (\(p:pos) -> Id pos (NtoPos (PosToN p)) p) (refl pos pos1) hS p
+ where
+  hS (p : pos) (hp: Id pos (NtoPos (PosToN p)) p) :  Id pos (NtoPos (PosToN (sucPos p))) (sucPos p)
+   =
+    let H1 : Id pos (NtoPos (PosToN (sucPos p))) (NtoPos (suc (PosToN p)))
+         = mapOnPath nat pos NtoPos (PosToN (sucPos p)) (suc (PosToN p)) (sucPosSuc p)
 
---         H3 : Id pos (sucPos (NtoPos (PosToN p))) (sucPos p)
---         H3 = mapOnPath pos pos sucPos (NtoPos (PosToN p)) p hp
---     in comp pos (NtoPos (PosToN (sucPos p))) (sucPos (NtoPos (PosToN p))) (sucPos p)
---          (comp pos (NtoPos (PosToN (sucPos p))) (NtoPos (suc (PosToN p))) (sucPos (NtoPos (PosToN p))) H1 H2)
---          H3
-
--- posToNinj : injective pos N PosToN
--- posToNinj = retractInj pos N PosToN NtoPos NtoPosK
-
--- -- Binary natural numbers
--- binN : U
--- data binN = binN0 | binNpos (p : pos)
-
--- NtoBinN : N -> binN
--- NtoBinN = split
---   zero  -> binN0
---   suc n -> binNpos (NtoPos (suc n))
-
--- BinNtoN : binN -> N
--- BinNtoN = split
---   binN0     -> zero
---   binNpos p -> PosToN p
-
--- NtoBinNK : section binN N BinNtoN NtoBinN
--- NtoBinNK = split
---   zero  -> refl N zero
---   suc n -> PosToNK n
+        H2 : Id pos (NtoPos (suc (PosToN p))) (sucPos (NtoPos (PosToN p)))
+         = NtoPosSuc (PosToN p) (zeronPosToN p)
 
--- rem : (p : pos) -> Id binN (NtoBinN (PosToN (sucPos p))) (binNpos (sucPos p))
--- rem p = comp binN (NtoBinN (PosToN (sucPos p))) (binNpos (NtoPos (suc (PosToN p))))
---                  (binNpos (sucPos p)) rem1 rem2
---      where
---       rem1 : Id binN (NtoBinN (PosToN (sucPos p))) (binNpos (NtoPos (suc (PosToN p))))
---       rem1 = mapOnPath N binN NtoBinN (PosToN (sucPos p)) (suc (PosToN p)) (sucPosSuc p)
-
---       rem2 : Id binN (binNpos (NtoPos (suc (PosToN p)))) (binNpos (sucPos p))
---       rem2 = mapOnPath pos binN binNpos (NtoPos (suc (PosToN p))) (sucPos p)
---                 (comp pos (NtoPos (suc (PosToN p))) (sucPos (NtoPos (PosToN p))) (sucPos p)
---                 (NtoPosSuc (PosToN p) (zeronPosToN p))
---                 (mapOnPath pos pos sucPos (NtoPos (PosToN p)) p (NtoPosK p)))
-
--- lem1 : (p : pos) -> Id binN (NtoBinN (PosToN p)) (binNpos p)
--- lem1 p = posInd (\p -> Id binN (NtoBinN (PosToN p)) (binNpos p)) (refl binN (binNpos pos1))
---                 (\p _ -> rem p) p
-
--- BinNtoNK : retract binN N BinNtoN NtoBinN
--- BinNtoNK = split
---   binN0     -> refl binN binN0
---   binNpos p -> lem1 p
-
--- IdbinNN : Id U binN N
--- IdbinNN = isoId binN N BinNtoN NtoBinN NtoBinNK BinNtoNK
-
--- binNMonoid : Monoid binN
--- binNMonoid = transMonoidInv binN N IdbinNN monoidAddN
-
--- zeroBinN : binN
--- zeroBinN = zm binN binNMonoid
-
--- addBinN : binN -> binN -> binN
--- addBinN = opm binN binNMonoid
-
--- addBinNA : (a b c : binN) ->
---            Id binN (addBinN a (addBinN b c)) (addBinN (addBinN a b) c)
--- addBinNA = opmA binN binNMonoid
-
--- test : binN
--- test = addBinN (binNpos (x1 (x1 (x0 pos1)))) (binNpos (x0 (x0 (x0 (x1 pos1)))))
-
--- -- Doubling
-
--- one : N
--- one = suc zero
-
--- two : N
--- two = suc one
-
--- three : N
--- three = suc two
-
--- four : N
--- four = suc three
-
--- five : N
--- five = suc four
-
--- -- doublesN n m = 2^n * m
--- doublesN : N -> N -> N
--- doublesN = split
---   zero  -> \m -> m
---   suc n -> \m -> doublesN n (doubleN m)
-
--- n1024 : N
--- n1024 = doublesN (addN four four) four
-
--- doubleBinN : binN -> binN
--- doubleBinN = split
---   binN0     -> binN0
---   binNpos p -> binNpos (x0 p)
-
--- doublesBinN : N -> binN -> binN
--- doublesBinN = split
---   zero  -> \m -> m
---   suc n -> \m -> doublesBinN n (doubleBinN m)
-
--- -- Doubling structure
--- Double : U
--- data Double =
---   D (A : U) -- carrier
---     (double : A -> A) -- doubling function computing 2 * x
---     (elt : A) -- element to double
-
--- carrier : Double -> U
--- carrier = split D c _ _ -> c
-
--- double : (D : Double) -> (carrier D -> carrier D)
--- double = split D _ op _ -> op
-
--- elt : (D : Double) -> carrier D
--- elt = split D _ _ e -> e
-
--- DoubleN : Double
--- DoubleN = D N doubleN n1024
-
--- DoubleBinN : Double
--- DoubleBinN = D binN doubleBinN (NtoBinN n1024)
-
--- -- iterate
--- iter : (A : U) -> N -> (A -> A) -> A -> A
--- iter A = split
---   zero  -> \_ z -> z
---   suc n -> \f z -> f (iter A n f z)
+        H3 : Id pos (sucPos (NtoPos (PosToN p))) (sucPos p)
+         = mapOnPath pos pos sucPos (NtoPos (PosToN p)) p hp
+    in compId pos (NtoPos (PosToN (sucPos p))) (sucPos (NtoPos (PosToN p))) (sucPos p)
+         (compId pos (NtoPos (PosToN (sucPos p))) (NtoPos (suc (PosToN p))) (sucPos (NtoPos (PosToN p))) H1 H2)
+         H3
 
--- -- 2^10 * e = 2^5 * (2^5 * e)
--- propDouble : (D : Double) -> U
--- propDouble D = Id (carrier D) (iter (carrier D) (doubleN five) (double D) (elt D))
---                               (iter (carrier D) five (double D) (iter (carrier D) five (double D) (elt D)))
+posToNinj : injective pos nat PosToN
+ = \ (p0 p1:pos) (h:Id nat (PosToN p0) (PosToN p1)) ->
+       <i> comp (<_>pos) (NtoPos (h@i)) [(i=0) -> NtoPosK p0,(i=1) -> NtoPosK p1]
 
--- -- The property we want to prove that takes long to typecheck:
--- -- 2^10 * 1024 = 2^5 * (2^5 * 1024)
--- -- propN : propDouble DoubleN
--- -- propN = refl N (doublesN (addN five five) n1024)
+-- Binary natural numbers
+data binN = binN0 | binNpos (p : pos)
 
--- -- With binary numbers it is instant
--- propBin : propDouble DoubleBinN
--- propBin = refl binN (doublesBinN (addN five five) (elt DoubleBinN))
+NtoBinN : nat -> binN = split
+  zero  -> binN0
+  suc n -> binNpos (NtoPos (suc n))
 
--- -- Define intermediate structure:
--- doubleBinN' : binN -> binN
--- doubleBinN' b = NtoBinN (doubleN (BinNtoN b))
+BinNtoN : binN -> nat = split
+  binN0     -> zero
+  binNpos p -> PosToN p
 
--- DoubleBinN' : Double
--- DoubleBinN' = D binN doubleBinN' (NtoBinN n1024)
+NtoBinNK : (n:nat) -> Id nat (BinNtoN (NtoBinN n)) n = split
+  zero  -> refl nat zero
+  suc n -> PosToNK n
 
--- eqDouble1 : Id Double DoubleN DoubleBinN'
--- eqDouble1 = elimIsIso N (\B f g -> Id Double DoubleN (D B (\b -> f (doubleN (g b))) (f n1024)))
---                         (refl Double DoubleN) binN NtoBinN BinNtoN BinNtoNK NtoBinNK
+rem (p : pos) : Id binN (NtoBinN (PosToN (sucPos p))) (binNpos (sucPos p)) =
+ compId binN (NtoBinN (PosToN (sucPos p))) (binNpos (NtoPos (suc (PosToN p))))
+                 (binNpos (sucPos p)) rem1 rem2
+     where
+      rem1 : Id binN (NtoBinN (PosToN (sucPos p))) (binNpos (NtoPos (suc (PosToN p))))
+           = mapOnPath nat binN NtoBinN (PosToN (sucPos p)) (suc (PosToN p)) (sucPosSuc p)
 
--- eqDouble2 : Id Double DoubleBinN' DoubleBinN
--- eqDouble2 = mapOnPath (binN -> binN) Double F doubleBinN' doubleBinN rem
---  where
---   F : (binN -> binN) -> Double
---   F d = D binN d (NtoBinN n1024)
+      rem2 : Id binN (binNpos (NtoPos (suc (PosToN p)))) (binNpos (sucPos p))
+           = <i>binNpos 
+                (compId pos (NtoPos (suc (PosToN p))) (sucPos (NtoPos (PosToN p))) (sucPos p)
+                (NtoPosSuc (PosToN p) (zeronPosToN p))
+                (mapOnPath pos pos sucPos (NtoPos (PosToN p)) p (NtoPosK p))@i)
+
+lem1 (p : pos) : Id binN (NtoBinN (PosToN p)) (binNpos p)
+       = posInd (\ (p:pos) -> Id binN (NtoBinN (PosToN p)) (binNpos p)) (refl binN (binNpos pos1))
+                (\ (p:pos) (_:Id binN (NtoBinN (PosToN p)) (binNpos p)) -> rem p) p
+
+BinNtoNK : (b:binN) -> Id binN (NtoBinN (BinNtoN b)) b = split --  retract binN N BinNtoN NtoBinN = split
+  binN0     -> refl binN binN0
+  binNpos p -> lem1 p
+
+IdbinNN : Id U binN nat
+ = isoId binN nat BinNtoN NtoBinN NtoBinNK BinNtoNK
+
+-- Doubling
+
+one : nat   = suc zero
+two : nat   = suc one
+three : nat = suc two
+four : nat  = suc three
+five : nat  = suc four
+
+-- doublesN n m = 2^n * m
+doublesN : nat -> nat -> nat = split
+  zero  -> \(m:nat) -> m
+  suc n -> \(m:nat) -> doublesN n (doubleN m)
+
+addN (n:nat) : nat -> nat = split
+ zero -> n
+ suc m -> suc (addN n m)
+
+n1024 : nat = doublesN (addN four four) four
+
+doubleBinN : binN -> binN = split
+  binN0     -> binN0
+  binNpos p -> binNpos (x0 p)
+
+doublesBinN : nat -> binN -> binN = split
+  zero  -> \(m:binN) -> m
+  suc n -> \(m:binN) -> doublesBinN n (doubleBinN m)
+
+-- Doubling structure
+data Double =
+  D (A : U) -- carrier
+    (double : A -> A) -- doubling function computing 2 * x
+    (elt : A) -- element to double
+
+carrier : Double -> U 
+ = split D c _ _ -> c
+
+double : (D : Double) -> (carrier D -> carrier D)
+ = split D _ op _ -> op
+
+elt : (D : Double) -> carrier D
+ = split D _ _ e -> e
+
+DoubleN : Double = D nat doubleN n1024
+
+DoubleBinN : Double = D binN doubleBinN (NtoBinN n1024)
+
+-- iterate
+iter (A : U) : nat -> (A -> A) -> A -> A = split
+  zero  -> \(f:A->A) (z:A) -> z
+  suc n -> \(f:A->A) (z:A) -> f (iter A n f z)
+
+-- 2^10 * e = 2^5 * (2^5 * e)
+propDouble (D : Double) : U
+ = Id (carrier D) (iter (carrier D) (doubleN five) (double D) (elt D))
+                              (iter (carrier D) five (double D) (iter (carrier D) five (double D) (elt D)))
+
+-- The property we want to prove that takes long to typecheck:
+-- 2^10 * 1024 = 2^5 * (2^5 * 1024)
+-- propN : propDouble DoubleN
+-- propN = refl N (doublesN (addN five five) n1024)
+
+-- With binary numbers it is instant
+propBin : propDouble DoubleBinN
+ = refl binN (doublesBinN (addN five five) (elt DoubleBinN))
+
+-- Define intermediate structure:
+doubleBinN' (b:binN) : binN
+ = NtoBinN (doubleN (BinNtoN b))
+
+DoubleBinN' : Double
+ = D binN doubleBinN' (NtoBinN n1024)
+
+eqDouble1 : Id Double DoubleN DoubleBinN'
+ = elimIsIso nat (\(B : U) (f : nat -> B) (g : B -> nat) -> Id Double DoubleN (D B (\(b : B) -> f (doubleN (g b))) (f n1024)))
+             (refl Double DoubleN) binN NtoBinN BinNtoN BinNtoNK NtoBinNK
+
+eqDouble2 : Id Double DoubleBinN' DoubleBinN
+ = mapOnPath (binN -> binN) Double F doubleBinN' doubleBinN rem
+  where
+   F (d:binN -> binN) : Double
+    = D binN d (NtoBinN n1024)
 
---   rem : Id (binN -> binN) doubleBinN' doubleBinN
---   rem = funExt binN (\_ -> binN) doubleBinN' doubleBinN rem1
---    where
---     rem1 : (n : binN) -> Id binN (doubleBinN' n) (doubleBinN n)
---     rem1 = split
---       binN0     -> refl binN binN0
---       binNpos p ->
---         let p1 : Id binN (NtoBinN (doubleN (PosToN p))) (NtoBinN (PosToN (x0 p)))
---             p1 = mapOnPath N binN NtoBinN (doubleN (PosToN p)) (PosToN (x0 p)) (refl N (doubleN (PosToN p)))
---         in comp binN (NtoBinN (doubleN (PosToN p))) (NtoBinN (PosToN (x0 p))) (binNpos (x0 p)) p1 (lem1 (x0 p))
-
--- eqDouble : Id Double DoubleN DoubleBinN
--- eqDouble = comp Double DoubleN DoubleBinN' DoubleBinN eqDouble1 eqDouble2
+   rem : Id (binN -> binN) doubleBinN' doubleBinN
+    = funExt binN (\(x:binN) -> binN) doubleBinN' doubleBinN rem1
+    where
+     rem1 : (n : binN) -> Id binN (doubleBinN' n) (doubleBinN n)
+      = split
+      binN0     -> refl binN binN0
+      binNpos p ->
+        let p1 : Id binN (NtoBinN (doubleN (PosToN p))) (NtoBinN (PosToN (x0 p)))
+             = mapOnPath nat binN NtoBinN (doubleN (PosToN p)) (PosToN (x0 p)) (refl nat (doubleN (PosToN p)))
+        in compId binN (NtoBinN (doubleN (PosToN p))) (NtoBinN (PosToN (x0 p))) (binNpos (x0 p)) p1 (lem1 (x0 p))
+
+eqDouble : Id Double DoubleN DoubleBinN
+ = compId Double DoubleN DoubleBinN' DoubleBinN eqDouble1 eqDouble2
 
 -- opaque doubleN
 
--- -- goal : propDouble DoubleN
--- -- goal = substInv Double propDouble DoubleN DoubleBinN eqDouble propBin
\ No newline at end of file
+-- goal : propDouble DoubleN = substInv Double propDouble DoubleN DoubleBinN eqDouble propBin
+
diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 2ed8ee2..95d71e0 100644
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -5,6 +5,7 @@
 -- and don't terminate in reasonable time.
 module univalence where
 
+import retract
 import equiv
 
 ------------------------------------------------------------------------------
@@ -201,4 +202,45 @@ slowtest (A : U) : Id (equiv A A)
 -- --     (isEquiv (Id U A B) (equiv A B))
 -- --      (canIdToEquiv A B) (transEquiv A B)
 -- --      (canIdToEquivIsTransEquiv A B)
--- --      (transEquivIsEquiv A B)
\ No newline at end of file
+-- --      (transEquivIsEquiv A B)
+
+
+
+------------------------------------------------------------------------------
+-- Elimination principle for equivalences and isomorphisms
+
+isContrProp (A : U) (h : isContr A) : prop A = p
+  where
+  p (a b : A) : Id A a b = <i> comp (<_> A) h.1 [ (i = 0) -> h.2 a, (i = 1) -> h.2 b ]
+
+idEquiv (A : U) : equiv A A = (idfun A,idIsEquiv A)
+
+contrSinglEquiv (A B : U) (f : equiv A B) :
+  Id ((X : U) * equiv X B) (B,idEquiv B) (A,f) = rem
+  where
+  rem1 : prop ((X : U) * equiv X B) = isContrProp ((X : U) * equiv X B) (lem1 B)
+  rem : Id ((X : U) * equiv X B) (B,idEquiv B) (A,f) = rem1 (B,idEquiv B) (A,f)
+
+elimEquiv (B : U) (P : (A : U) -> (A -> B) -> U) (d : P B (idfun B))
+            (A : U) (f : equiv A B) : P A f.1 = rem
+  where
+  T (z : (X : U) * equiv X B) : U = P z.1 z.2.1
+  rem1 : Id ((X : U) * equiv X B) (B,idEquiv B) (A,f) = contrSinglEquiv A B f
+  rem : P A f.1 = subst ((X : U) * equiv X B) T (B,idEquiv B) (A,f) rem1 d
+
+elimIso (B : U) (Q : (A : U) -> (A -> B) -> (B -> A) -> U)
+        (h1 : Q B (idfun B) (idfun B)) (A : U) (f : A -> B) : (g : B -> A) ->
+        section A B f g -> retract A B f g -> Q A f g = rem1 A f
+ where
+   P (A : U) (f : A -> B) : U = (g : B -> A) -> section A B f g -> retract A B f g -> Q A f g
+
+   rem : P B (idfun B) = \(g : B -> B) (sg : section B B (idfun B) g) (rg : retract B B (idfun B) g) ->
+     substInv (B -> B) (Q B (idfun B)) g (idfun B) (<i> \(b : B) -> (sg b) @ i) h1
+
+   rem1 (A : U) (f : A -> B) : P A f = \(g : B -> A) (sg : section A B f g) (rg : retract A B f g) -> 
+          elimEquiv B P rem A (f,gradLemma A B f g sg rg) g sg rg
+
+elimIsIso (A : U) (Q : (B : U) -> (A -> B) -> (B -> A) -> U)
+         (d : Q A (idfun A) (idfun A)) (B : U) (f : A -> B) (g : B -> A)
+         (sg : section A B f g) (rg : retract A B f g) : Q B f g =
+  elimIso A (\(B : U) (f : B -> A) (g : A -> B) -> Q B g f) d B g f rg sg