From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Fri, 21 Oct 2016 18:04:31 +0000 (-0400)
Subject: comments
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=c7f0f1c07a7cbe81bfe53a7eb91ad34197f917ab;p=cubicaltt.git

comments
---

diff --git a/examples/helix.ctt b/examples/helix.ctt
index 31b3875..d7e75c1 100644
--- a/examples/helix.ctt
+++ b/examples/helix.ctt
@@ -306,7 +306,8 @@ invMult (x y:S1) : S1 = (multIsEquiv x y).1.1
 
 invS1 (x:S1) : S1 = invMult x base
 
-lemInvS1 : Path S1 (invS1 base) base = <i> comp (<_>S1) (comp (<_>S1) base [(i=1) -> refl S1 base]) [(i=1) -> refl S1 base]
+lemInvS1 : Path S1 (invS1 base) base = 
+  <i> comp (<_>S1) (comp (<_>S1) base [(i=1) -> refl S1 base]) [(i=1) -> refl S1 base]
 
 loopInvS1 : U = Path S1 (invS1 base) (invS1 base)
 
diff --git a/examples/injective.ctt b/examples/injective.ctt
index bd339d4..f6be07f 100644
--- a/examples/injective.ctt
+++ b/examples/injective.ctt
@@ -1,6 +1,8 @@
+-- Two definitions of injectivity and proof that they can be
+-- identified
 module injective where
 
-import prop
+import equiv
 
 -- First definition of injectivity, informally: if two elements f a0, f a1 are
 -- equal in B, then a0, a1 must be equal in A.
@@ -99,4 +101,4 @@ injPath (A B : U) (f : A -> B) (sA : set A) (sB : set B) :
     Path U (inj0 A B f sA sB) (inj1 A B f sA sB)
   = propPath (inj0 A B f sA sB) (inj1 A B f sA sB)
       (inj01 A B f sA sB) (inj10 A B f sA sB)
-      (prop_inj0 A B f sA sB) (prop_inj1 A B f sA sB)
\ No newline at end of file
+      (prop_inj0 A B f sA sB) (prop_inj1 A B f sA sB)
diff --git a/examples/int.ctt b/examples/int.ctt
index 391db88..0f46117 100644
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -1,3 +1,5 @@
+-- The integers as nat + nat with proof that suc is an iso giving a
+-- non-trivial path from Z to Z
 module int where
 
 import equiv
diff --git a/examples/integer.ctt b/examples/integer.ctt
index 4886fa5..8892377 100644
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -1,3 +1,5 @@
+-- The integers as a HIT (identifying +0 with -0). Proof that this
+-- representation is isomorphic to the one in int.ctt
 module integer where
 
 import int
diff --git a/examples/interval.ctt b/examples/interval.ctt
index a0d3645..29f2549 100644
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -1,10 +1,12 @@
+-- The interval as a HIT. Proof of funtion extensionality from it.
 module interval where
 
-import gradLemma
 import equiv
 
-
-data I = zero | one | seg <i> [(i = 0) -> zero, (i = 1) -> one]
+data I = zero 
+       | one
+       | seg <i> [ (i = 0) -> zero
+                 , (i = 1) -> one ]
 
 -- Proof of funext from the interval
 fext (A B : U) (f g : A -> B) (p : (x : A) -> Path B (f x) (g x)) :
diff --git a/examples/list.ctt b/examples/list.ctt
index 83fdac8..6ad651c 100644
--- a/examples/list.ctt
+++ b/examples/list.ctt
@@ -1,8 +1,10 @@
+-- Lists
 module list where
 
 import prelude
 
-data list (A : U) = nil | cons (a : A) (as : list A)
+data list (A : U) = nil 
+                  | cons (a : A) (as : list A)
 
 append (A : U) : list A -> list A -> list A = split
   nil -> idfun (list A)
diff --git a/examples/nat.ctt b/examples/nat.ctt
index 10baab4..47eee38 100644
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -1,3 +1,4 @@
+-- Natural numbers
 module nat where
 
 import bool
diff --git a/examples/ordinal.ctt b/examples/ordinal.ctt
index a5fe863..f1fb72d 100644
--- a/examples/ordinal.ctt
+++ b/examples/ordinal.ctt
@@ -1,3 +1,4 @@
+-- Ordinals
 module ordinal where
 
 import prelude
diff --git a/examples/pi.ctt b/examples/pi.ctt
index 99aa68e..3f180ce 100644
--- a/examples/pi.ctt
+++ b/examples/pi.ctt
@@ -1,3 +1,4 @@
+-- Characterization of equality in pi types.
 module pi where
 
 import equiv
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index ce9a07b..0c8a77d 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -1,3 +1,6 @@
+-- The prelude. Definition of Path types and basic operations on them
+-- (refl, mapOnPath, funExt...). Definition of prop, set and
+-- groupoid. Some basic data types (empty, unit, or, and).
 module prelude where
 
 -- Identity types
diff --git a/examples/propTrunc.ctt b/examples/propTrunc.ctt
index 146c165..a4b33fe 100644
--- a/examples/propTrunc.ctt
+++ b/examples/propTrunc.ctt
@@ -1,3 +1,4 @@
+-- Propositional truncation as a HIT. (WARNING: not working correctly)
 module propTrunc where
 
 import prelude
diff --git a/examples/retract.ctt b/examples/retract.ctt
index 72a11f0..84783b1 100644
--- a/examples/retract.ctt
+++ b/examples/retract.ctt
@@ -1,3 +1,4 @@
+-- Definition of retract and section
 module retract where
 
 import prelude
diff --git a/examples/sigma.ctt b/examples/sigma.ctt
index 9494866..f389439 100644
--- a/examples/sigma.ctt
+++ b/examples/sigma.ctt
@@ -1,3 +1,4 @@
+-- Various results about sigma types.
 module sigma where
 
 import equiv
diff --git a/examples/subset.ctt b/examples/subset.ctt
index 1e279f0..0df6500 100644
--- a/examples/subset.ctt
+++ b/examples/subset.ctt
@@ -1,3 +1,4 @@
+-- Two definitions of a subset and a proof that they are equal.
 module subset where
 
 import injective
@@ -181,4 +182,4 @@ subsetIso1 (A : U) (sA : set A) : (s1 : subset1 A sA) ->
 -- Show that we can identify the two definitions of subsets with each other
 subsetPath (A : U) (sA : set A) : Path U (subset0 A sA) (subset1 A sA)
   = isoPath (subset0 A sA) (subset1 A sA) (subset01 A sA) (subset10 A sA)
-      (subsetIso1 A sA) (subsetIso0 A sA)
\ No newline at end of file
+      (subsetIso1 A sA) (subsetIso0 A sA)
diff --git a/examples/susp.ctt b/examples/susp.ctt
index b051f5b..8a5394a 100644
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -1,10 +1,14 @@
+-- Suspension. Definition of the circle as the suspension of bool and
+-- a proof that this is equal to the standard HIT representation of
+-- the circle.
 module susp where
 
 import circle
 
 data susp (A : U) = north
                   | south
-                  | merid (a:A) <i> [(i=0) -> north, (i=1) -> south]
+                  | merid (a : A) <i> [ (i=0) -> north
+                                      , (i=1) -> south ]
 
 -- n-spheres
 sphere : nat -> U = split
diff --git a/examples/torsor.ctt b/examples/torsor.ctt
index 85b5b0a..c9faa9e 100644
--- a/examples/torsor.ctt
+++ b/examples/torsor.ctt
@@ -1,9 +1,8 @@
+-- Torsors. Proof that S1 is equal to BZ, the classifying space of Z.
 module torsor where
-import prelude
+
 import int
-import circle
 import helix
-import univalence
 
 --
 
diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 6619df2..1046657 100644
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -1,8 +1,8 @@
 -- This file contains two proofs of the univalence axiom. One using
 -- unglue (section 7.2) and a direct one (appendix B of the cubicaltt
 -- paper). The normal form of the first proof can be computed (and
--- typecheck, see nthmUniv) while the second one uses very much memory
--- and don't terminate in reasonable time.
+-- typechecked) while the second one uses very much memory and don't
+-- terminate in reasonable time.
 module univalence where
 
 import retract
diff --git a/examples/multS1.ctt b/experiments/multS1.ctt
similarity index 92%
rename from examples/multS1.ctt
rename to experiments/multS1.ctt
index c6bf3ef..761cc84 100644
--- a/examples/multS1.ctt
+++ b/experiments/multS1.ctt
@@ -1,30 +1,6 @@
 module multS1 where
 
-import circle
-
--- another inverse function
-
--- the multiplication is invertible
-
-lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x = split
- base -> bP
- loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i
-
-idL : (x : S1) -> Path S1 (mult base x) x = split
-       base -> refl S1 base
-       loop @ i -> <j> loop1 @ i
-
-multIsEquiv : (x:S1) -> isEquiv S1 S1 (mult x) =  lemPropFib P pP bP 
- where P (x:S1) : U            = isEquiv S1 S1 (mult x)
-       pP (x:S1) : prop (P x)  = propIsEquiv S1 S1 (mult x)
-       rem : Path (S1 -> S1) (idfun S1) (mult base) = <i>\ (x:S1) -> idL x @ -i
-       bP : P base = subst (S1->S1) (isEquiv S1 S1)  (idfun S1) (mult base) rem (idIsEquiv S1)
-
--- inverse of multiplication by x
-
-invMult (x y:S1) : S1 = (multIsEquiv x y).1.1
-
-invS1 (x:S1) : S1 = invMult x base
+import helix
 
 pt0 : S1 = mapOnPath S1 S1 invS1 base base loop2@0
 test1 : S1 = mapOnPath S1 S1 invS1 base base loop2@1
diff --git a/examples/prop.ctt b/experiments/prop.ctt
similarity index 100%
rename from examples/prop.ctt
rename to experiments/prop.ctt
diff --git a/examples/quotient.ctt b/experiments/quotient.ctt
similarity index 96%
rename from examples/quotient.ctt
rename to experiments/quotient.ctt
index 7669e2d..7b88dae 100644
--- a/examples/quotient.ctt
+++ b/experiments/quotient.ctt
@@ -1,6 +1,6 @@
+-- Experimental implementation of quotient HIT (not finished)
 module quotient where
 
-import prelude
 import circle
 
 -- Quotient A by R