From: coquand <coquand@chalmers.se>
Date: Tue, 14 Apr 2015 06:19:50 +0000 (+0200)
Subject: one example with constant functions
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f98077706d02d431dd125f4132d100d48adf54c2;p=cubicaltt.git

one example with constant functions
---

diff --git a/examples/ex1.ctt b/examples/ex1.ctt
new file mode 100644
index 0000000..c3fba31
--- /dev/null
+++ b/examples/ex1.ctt
@@ -0,0 +1,29 @@
+module ex1 where
+
+import prelude
+
+constant (A B:U) (f:A->B) : U = (x y:A) -> Id B (f x) (f y)
+
+data S (X:U) = inc (x:X) | path (x y:X) @ (inc x) ~ (inc y)
+
+phi (X A:U) (fc : (f:X->A) * constant X A f) : S X -> A = split
+  inc x -> fc.1 x
+  path x y @ i -> (fc.2 x y) @ i
+
+psi (X A:U) (f:S X -> A) : (f:X->A) * constant X A f = 
+ (\ (x:X) -> f (inc x), \ (x y:X) -> <i>(f (path{S X} x y)@i))
+
+lem (X A:U) (f : S X -> A) : Id (S X -> A) (phi X A (psi X A f)) f = 
+ <i> \ (x:S X) -> (rem x) @ i
+ where rem : (u : S X) -> Id A (phi X A (psi X A f) u) (f u) = split
+         inc x -> refl A (f (inc x))
+         path x y @ i -> <j>f (path{S X} x y)@ i
+
+thm (X A:U) : Id U ((f:X->A) * constant X A f) (S X -> A) = isoId T0 T1 f g t s
+ where T0 : U = (f:X->A) * constant X A f
+       T1 : U = S X -> A
+       f : T0 -> T1 = phi X A
+       g : T1 -> T0 = psi X A
+       s (x:T0) : Id T0 (g (f x)) x = refl T0 x
+       t : (y:T1) -> Id T1 (f (g y)) y = lem X A
+