comments

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 5748481ebd28898598796384107c011674e015b3..62544321d16eb0364f97522e7a3e1117a2ab09c8 100644 (file)
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -1,14 +1,12 @@
+-- The circle as a HIT.
 module circle where
 
 import bool
 import int
 
-              ----------------------------------
-              -- Example: The circle as a HIT --
-              ----------------------------------
-
 data S1 = base
-        | loop <i> [(i=0) -> base, (i=1) -> base]
+        | loop <i> [ (i=0) -> base
+                   , (i=1) -> base]
 
 loopS1 : U = Path S1 base base
 

diff --git a/examples/csystem.ctt b/examples/csystem.ctt
index 80ba0a10df0b1f5828ec8d06dab05f0b97e441fa..2158a973dcfe32be227356b15be51ebab75c4ec2 100644 (file)
--- a/examples/csystem.ctt
+++ b/examples/csystem.ctt
@@ -1,5 +1,7 @@
+-- Definition of C-systems and universe categories. Construction of a
+-- C-system from a universe category.
 module csystem where
-import prelude
+
 import sigma
 import equiv
 import nat