From c7f0f1c07a7cbe81bfe53a7eb91ad34197f917ab Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Fri, 21 Oct 2016 14:04:31 -0400 Subject: [PATCH] comments --- examples/helix.ctt | 3 ++- examples/injective.ctt | 6 ++++-- examples/int.ctt | 2 ++ examples/integer.ctt | 2 ++ examples/interval.ctt | 8 +++++--- examples/list.ctt | 4 +++- examples/nat.ctt | 1 + examples/ordinal.ctt | 1 + examples/pi.ctt | 1 + examples/prelude.ctt | 3 +++ examples/propTrunc.ctt | 1 + examples/retract.ctt | 1 + examples/sigma.ctt | 1 + examples/subset.ctt | 3 ++- examples/susp.ctt | 6 +++++- examples/torsor.ctt | 5 ++--- examples/univalence.ctt | 4 ++-- {examples => experiments}/multS1.ctt | 26 +------------------------- {examples => experiments}/prop.ctt | 0 {examples => experiments}/quotient.ctt | 2 +- 20 files changed, 40 insertions(+), 40 deletions(-) rename {examples => experiments}/multS1.ctt (92%) rename {examples => experiments}/prop.ctt (100%) rename {examples => experiments}/quotient.ctt (96%) 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 = comp (<_>S1) (comp (<_>S1) base [(i=1) -> refl S1 base]) [(i=1) -> refl S1 base] +lemInvS1 : Path S1 (invS1 base) base = + 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 = 0) -> zero, (i = 1) -> one] +data I = zero + | one + | seg [ (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=0) -> north, (i=1) -> south] + | merid (a : A) [ (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 -> 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) = \ (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 -- 2.34.1