From 4e708c67792dfafb3c87699462a8666fc9a40efb Mon Sep 17 00:00:00 2001
From: Anders <mortberg@chalmers.se>
Date: Tue, 14 Apr 2015 16:54:50 +0200
Subject: [PATCH] Update the description in demo.ctt

---
 examples/demo.ctt | 27 ++++++++++++++++++++++++---
 1 file changed, 24 insertions(+), 3 deletions(-)

diff --git a/examples/demo.ctt b/examples/demo.ctt
index e4b6f1b..2375f33 100644
--- a/examples/demo.ctt
+++ b/examples/demo.ctt
@@ -27,12 +27,33 @@ data list (A : U) = nil
                   | cons (a : A) (as : list A)
 
 
--- "IdP P a b" is a built-in notion where P : Id U A B, a : A and b : B
--- "<i>" abstracts the name/color/dimension i.
+{-
+
+An element in ID A0 A1 is a line in the universe connecting A0 and A1:
+
+ |- A0  Type     |- A1  Type
+-----------------------------
+     |- ID A0 A1   Type
+
+
+   |- P : ID A0 A1      |- a0 : A0     |- a1 : A1
+--------------------------------------------------------
+             |- IdP P a0 a1   Type
+
+
+Note: As we have U : U the type ID is not needed in the
+      implementation.
+
+-}
+
+-- The usual identity can be seen a special case of IdP:
 Id (A : U) (a b : A) : U = IdP (<i> A) a b
 
-refl (A : U) (a : A) : Id A a a = <i> a
+-- Here "<i> A" is a constant path in the universe:
+constPath (A : U) : Id U A A = <i> A
 
+-- "<i>" abstracts the name/color/dimension i.
+refl (A : U) (a : A) : Id A a a = <i> a
 
 inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 
-- 
2.34.1