From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 20 Oct 2016 21:47:04 +0000 (-0400)
Subject: a lot of comments
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9c8123c53fdabcf66d3db7feb4ab192f4b45ce7d;p=cubicaltt.git

a lot of comments
---

diff --git a/examples/discor.ctt b/examples/discor.ctt
index 5b39f91..068a46d 100644
--- a/examples/discor.ctt
+++ b/examples/discor.ctt
@@ -1,3 +1,4 @@
+-- or A B is discrete if A and B are
 module discor where
 
 import prelude
diff --git a/examples/groupoidTrunc.ctt b/examples/groupoidTrunc.ctt
index e3149bf..827e4dd 100644
--- a/examples/groupoidTrunc.ctt
+++ b/examples/groupoidTrunc.ctt
@@ -1,3 +1,4 @@
+-- The groupoid truncation as a HIT
 module groupoidTrunc where
 
 import equiv
diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt
index 9a57b92..e438e62 100644
--- a/examples/hedberg.ctt
+++ b/examples/hedberg.ctt
@@ -1,3 +1,4 @@
+-- Hedbergs lemma: a type with decidable equality is a set
 module hedberg where
 
 import prelude
diff --git a/examples/helix.ctt b/examples/helix.ctt
index 5e0e4be..31b3875 100644
--- a/examples/helix.ctt
+++ b/examples/helix.ctt
@@ -1,3 +1,4 @@
+-- The loop space of the circle is equal to Z
 module helix where
 
 import circle
diff --git a/examples/hnat.ctt b/examples/hnat.ctt
index 723de51..2834ed5 100644
--- a/examples/hnat.ctt
+++ b/examples/hnat.ctt
@@ -1,3 +1,4 @@
+-- Non-standard natural numbers as a HIT without any path constructor
 module hnat where
 
 import nat
diff --git a/examples/idtypes.ctt b/examples/idtypes.ctt
index d0705dd..d2bb65e 100644
--- a/examples/idtypes.ctt
+++ b/examples/idtypes.ctt
@@ -1,3 +1,5 @@
+-- Identity types (variation of Path types with definitional equality
+-- for J). Including a proof univalence expressed only using Id. 
 module idtypes where
 
 import sigma
diff --git a/examples/int.ctt b/examples/int.ctt
index 1bd6891..391db88 100644
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -61,4 +61,6 @@ sucPathZ : Path U Z Z = isoPath Z Z sucZ predZ sucpredZ predsucZ
 testOneZ : Z = transport sucPathZ zeroZ
 testNOneZ : Z = transport (<i> sucPathZ @ - i) zeroZ
 
+
+
 ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)