From: Simon Huber <hubsim@gmail.com>
Date: Tue, 24 Mar 2015 17:19:51 +0000 (+0100)
Subject: examples
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4dfc94192396c19e683e5fac8d006fdf66dda110;p=cubicaltt.git

examples
---

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 82792ea..7fe411e 100644
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -70,5 +70,25 @@ test4 : Id U bool bool = <i> negNegEq @ i
 kanBool : Id U bool bool =
   kan U bool bool bool bool negEq negEq negEq
 
--- > negNegEq 
--- EVAL: <?0> glue (sum bool) [ (?0 = 0) -> ((sum bool),(((split bool_L7_C1),(((split bool_L7_C1),(((split bool_L11_C1),(split bool_L11_C1)))))))) ]
+-- connectSquare (A : U) (a0 a1 : A) (u : Id A a0 a1)
+--               (b0 b1 : A) (v : Id A b0 b1)
+--               (r0 : Id A a0 b0) (r1 : Id A a1 b1) : Square A a0 a1 u b0 b1 v r0 r1= 
+
+squareBoolF2 : Square U bool bool (refl U bool) bool F2
+                  boolEqF2 (refl U bool)  boolEqF2 =
+  <i j> boolEqF2 @ i /\ j
+
+test5 : IdP boolEqF2 true one = 
+  <i> transport (<j> boolEqF2 @ i /\ j) true
+
+test6 : Id bool true true =
+  <i> transport (<j> F2EqBool @ i \/ j) (test5 @ - i)
+
+test7 : Id U F2 F2 =
+  subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 negNegEq
+
+test8 : Id U F2 F2 =
+  subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 (refl U bool)
+
+test9 : Id U F2 F2 =
+  transport (<i> Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool)
\ No newline at end of file
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 67db0e4..b3818a7 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -40,3 +40,17 @@ isoId (A B : U) (f : A -> B) (g : B -> A)
       (s : (y:B) -> Id B (f (g y)) y)
       (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
       <i> glue B [ (i = 0) -> (A,f,g,s,t) ]
+
+
+--         u
+--    a0 ----- a1
+--    |        |
+-- r0 |        | r1
+--    |        |
+--    b0 ----- b1
+--         v
+
+Square (A : U) (a0 a1 : A) (u : Id A a0 a1)
+               (b0 b1 : A) (v : Id A b0 b1)
+               (r0 : Id A a0 b0) (r1 : Id A a1 b1) : U
+  = IdP (<i> (IdP (<j> A) (u @ i) (v @ i))) r0 r1