From 7786ab9f5814ecf53c418805fd0cd55c47698268 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Thu, 9 Apr 2015 13:16:33 +0200 Subject: [PATCH] funext from interval --- examples/interval.ctt | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 examples/interval.ctt 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 ( seg{I} @ i) + where htpy (x : A) : I -> B = split + zero -> f x + one -> g x + seg @ i -> (p x) @ i -- 2.34.1