From: Anders <mortberg@chalmers.se>
Date: Fri, 27 Mar 2015 16:53:07 +0000 (+0100)
Subject: Examples
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d130265253b40a7c15a63eca74fc83e5c752c215;p=cubicaltt.git

Examples
---

diff --git a/examples/integer.ctt b/examples/integer.ctt
index 2f08c7b..e8b6ba9 100644
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -37,3 +37,6 @@ predsucZ : (n : Z) -> Id Z (predZ (sucZ n)) n = split
       suc n -> refl Z (negZ (suc n))
 
 sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ
+
+sucIdZ2 : Id U Z Z = compId U Z Z Z sucIdZ sucIdZ
+test : Z = predZ (transport sucIdZ2 zeroZ)
\ No newline at end of file
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index c3bd9f6..1566339 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -49,11 +49,12 @@ isoId (A B : U) (f : A -> B) (g : B -> A)
       <i> glue B [ (i = 0) -> (A,f,g,s,t) ]
 
 --         u
---    a0 ----- a1
---    |        |
--- r0 |        | r1
---    |        |
---    b0 ----- b1
+--    a0 -----> a1
+--    |         |
+-- r0 |         | r1
+--    |         |
+--    V         V
+--    b0 -----> b1
 --         v
 
 Square (A : U) (a0 a1 : A) (u : Id A a0 a1)