From: Simon Huber 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 = negNegEq @ i kanBool : Id U bool bool = kan U bool bool bool bool negEq negEq negEq --- > negNegEq --- EVAL: 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 = + boolEqF2 @ i /\ j + +test5 : IdP boolEqF2 true one = + transport ( boolEqF2 @ i /\ j) true + +test6 : Id bool true true = + transport ( 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 ( 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 = 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 ( (IdP ( A) (u @ i) (v @ i))) r0 r1