From: Simon Huber <hubsim@gmail.com>
Date: Thu, 9 Apr 2015 11:16:33 +0000 (+0200)
Subject: funext from interval
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7786ab9f5814ecf53c418805fd0cd55c47698268;p=cubicaltt.git

funext from interval
---

diff --git a/examples/interval.ctt b/examples/interval.ctt
new file mode 100644
index 0000000..01c49e6
--- /dev/null
+++ b/examples/interval.ctt
@@ -0,0 +1,13 @@
+module interval where
+
+import prelude
+
+data I = zero | one | seg @ zero ~ one
+
+fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) :
+     Id (A -> B) f g = mapOnPath I (A -> B) (\(i : I) (x : A) -> htpy x i)
+                          zero one (<i> seg{I} @ i)
+  where htpy (x : A) : I -> B = split
+          zero    -> f x
+          one     -> g x
+          seg @ i -> (p x) @ i