a lot of comments

diff --git a/examples/discor.ctt b/examples/discor.ctt
index 5b39f91c23313dbf341e3f1f7e33a4d2a535db2f..068a46d619d29b38cab9bd9ba56a04c2ba3f27e3 100644 (file)
--- a/examples/discor.ctt
+++ b/examples/discor.ctt
@@ -1,3 +1,4 @@
+-- or A B is discrete if A and B are\r
 module discor where\r
 \r
 import prelude\r

diff --git a/examples/groupoidTrunc.ctt b/examples/groupoidTrunc.ctt
index e3149bf2b4759f55d9096c43a2b5bbdd19c33313..827e4dd5801e29977ab096168362f75ee8d0e899 100644 (file)
--- 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 9a57b92f8eb37146e5732a670e8be0e5f23b0fe6..e438e62f672c45665a3a2c78e23f1438c0002a8b 100644 (file)
--- a/examples/hedberg.ctt
+++ b/examples/hedberg.ctt
@@ -1,3 +1,4 @@
+-- Hedbergs lemma: a type with decidable equality is a set\r
 module hedberg where\r
 \r
 import prelude\r

diff --git a/examples/helix.ctt b/examples/helix.ctt
index 5e0e4be34a929e4040a201096a1ca05d8fc8989d..31b387511ba17bc7957da700b5c9cf84a15c605f 100644 (file)
--- 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 723de51d5adecba8e65d35a4012ad4af1186372a..2834ed5b2c1c4d6c2d91529a64cb110b16dea2e5 100644 (file)
--- 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 d0705ddf549acb664a1acb8ec546e74020ca83db..d2bb65e207a3590b5273065bc207cb35ca296054 100644 (file)
--- 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 1bd689198ac64d5cd8cf2395f3e5502eb9987322..391db88982b9915152bf6e9889395c60d83a8e82 100644 (file)
--- 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\r
 testNOneZ : Z = transport (<i> sucPathZ @ - i) zeroZ\r
 \r
+\r
+\r
 ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)\r