Examples

diff --git a/examples/integer.ctt b/examples/integer.ctt
index 2f08c7b2b44e38bd6aaa06ed19ffa6e38bf70676..e8b6ba9e10f80ae817362f243131f7659ffec1ed 100644 (file)
--- 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 c3bd9f6ec42bb499760bd9556a7513faac75c7d1..15663399f37506e9dafbffe92fe3ee136ad3f7ff 100644 (file)
--- 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)