Add equiv and uafunext2

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
new file mode 100644 (file)
index 0000000..5e32517
--- /dev/null
+++ b/examples/equiv.ctt
@@ -0,0 +1,51 @@
+module equiv where\r
+\r
+import prelude\r
+\r
+and (A B:U) :U = (_:A) * B\r
+\r
+contr (A:U) : U = (_:A) * prop A\r
+\r
+isContr (A : U) : U = and (prop A) A\r
+\r
+fiber (A B:U) (f:A->B) (b:B) : U = (x:A) * Id B b (f x)\r
+\r
+lemIdFib (A:U) (a:A) : prop (fiber A A (\ (x:A) -> x) a) = rem\r
+ where F : U = fiber A A (\ (x:A) -> x) a\r
+       rem (u v:F) : Id F u v = <i>(rem1 @ i,rem2 @ i)\r
+         where x : A = u.1\r
+               p : Id A a x = u.2\r
+               y : A = v.1\r
+               q : Id A a y = v.2\r
+               rem1 : Id A x y = <i>comp A a [(i=0) -> p,(i=1) -> q]\r
+               rem2 : IdP (<i>Id A a (rem1@i)) p q = <i j>comp A a [(i=0) -> <l>p@(j/\l),(i=1) -> <l>q@(j/\l)]\r
+\r
+lemPropAnd (A B :U) (pA: prop A) (pB: A -> prop B) : prop (and A B) = \r
+ \ (u v:and A B) -> <i>((pA u.1 v.1)@i, (pB u.1 u.2 v.2)@i)\r
+\r
+isContrProp (A:U) : prop (isContr A) = \r
+ lemPropAnd (prop A) A (propIsProp A) (\ (h:prop A) -> h)\r
+\r
+isEquiv (A B:U) (f:A->B) : U = (y:B) -> isContr (fiber A B f y)\r
+\r
+idIsEquiv (A:U) : isEquiv A A (idfun A) = \ (a:A) -> (lemIdFib A a,(a,refl A a))\r
+\r
+propIsEquiv (A B : U) (f : A -> B) : prop (isEquiv A B f)\r
+ = propPi B (\ (y:B) -> isContr (fiber A B f y)) (\ (y:B) -> isContrProp (fiber A B f y))\r
+\r
+isEquivEq (A B : U) (f : A -> B) (is:isEquiv A B f) : Id U A B = \r
+ isoId A B f g (\ (y:B) -> <i>(s y)@-i) t\r
+ where\r
+   rem1 (y:B) : prop (fiber A B f y) =  (is y).1\r
+   rem2 (y:B) : fiber A B f y        =  (is y).2\r
+   g (y:B) : A = (rem2 y).1\r
+   s (y:B) : Id B y (f (g y)) = (rem2 y).2\r
+   rem3 (x:A) : Id B (f x) (f (g (f x))) = s (f x)\r
+   rem4 (x:A) : Id (fiber A B f (f x)) (g (f x),rem3 x) (x,refl B (f x)) = \r
+     rem1 (f x) (g (f x),rem3 x) (x,refl B (f x))\r
+   t (x:A) : Id A (g (f x)) x = <i> ((rem4 x)@i).1\r
+    \r
+Equiv (A B : U) : U = (f : A -> B) * isEquiv A B f\r
+\r
+lemIdEquiv (A B:U) (f g : Equiv A B) (h:Id (A->B) f.1 g.1) : Id (Equiv A B) f g\r
+ = <i>(h@i,(lemPropF (A->B) (isEquiv A B) (propIsEquiv A B) f.1 g.1 h f.2 g.2)@i)\r

diff --git a/examples/uafunext2.ctt b/examples/uafunext2.ctt
new file mode 100644 (file)
index 0000000..0ae4e82
--- /dev/null
+++ b/examples/uafunext2.ctt
@@ -0,0 +1,65 @@
+module uafunext2 where\r
+\r
+import retract\r
+import equiv\r
+\r
+lem1 (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : Id U ((x:A)*P x) A = isoId T A f g t s\r
+ where\r
+   T : U = (x:A) * P x\r
+   f (z:T) : A = z.1\r
+   g (x:A) : T = (x,(cA x).1)\r
+   s (z:T) : Id T (g (f z)) z = <i>(z.1,((cA z.1).2 (cA z.1).1 z.2)@ i)\r
+   t (x:A) : Id A (f (g x)) x = refl A x\r
+\r
+lem2 (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : Id U (A -> (x:A)*P x) (A->A) = \r
+ <i> A -> (lem1 A P cA)@ i\r
+\r
+alpha (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (u:A -> (x:A)*P x) : A -> A =\r
+ transport (lem2 A P cA) u\r
+\r
+test (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (u : A -> (x:A)*P x) (x:A) :\r
+ Id A (alpha A P cA u x) (u x).1 = refl A (u x).1\r
+\r
+\r
+lemTransFib (A:U) : (B:U) (E:Id U A B) (b:B) -> prop (fiber A B (\ (x:A) -> transport E x) b) =\r
+ J U A (\ (B:U) (E:Id U A B) -> (b:B) -> prop (fiber A B (\ (x:A) -> transport E x) b)) (lemIdFib A)\r
+        \r
+fibId (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : U = fiber (A -> (x:A)*P x) (A -> A) (alpha A P cA) (idfun A)\r
+\r
+corr1 (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : prop (fibId A P cA) = \r
+ lemTransFib (A -> (x:A)*P x) (A -> A) (lem2 A P cA) (idfun A)\r
+\r
+phi (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (f:(x:A) -> P x) : fibId A P cA =\r
+ (\ (x:A) -> (x,f x),refl (A->A) (idfun A))\r
+ \r
+psi (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (up : fibId A P cA) (x:A) : P x = \r
+ subst (A -> A) (\ (g:A->A) -> P (g x)) (alpha A P cA u) (idfun A) (<i>p@-i) (u x).2\r
+ where u : A -> (y:A) * P y = up.1\r
+       p : Id (A -> A) (idfun A) (alpha A P cA u) = up.2\r
+\r
+retPhiPsi (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (f : (x:A) -> P x) :\r
+ Id ((x:A) -> P x) (psi A P cA (phi A P cA f)) f = refl ((x:A) -> P x) f\r
+\r
+thm (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : prop ((x:A) -> P x) =\r
+ retractProp ((x:A) -> P x) (fibId A P cA) (phi A P cA) (psi A P cA) (retPhiPsi A P cA) (corr1 A P cA)\r
+\r
+sumF  (A B:U) (f:A -> B) : U = (g:A->B) * (x:A) -> Id B (f x) (g x)\r
+prodF (A B:U) (f:A -> B) : U = (x:A) -> (y:B) * Id B (f x) y\r
+\r
+lemProdF (A B:U) (f:A -> B) : prop (prodF A B f) = \r
+ thm A (\ (x:A) -> (y:B) * Id B (f x) y) (\ (x:A) -> ((f x,refl B (f x)),lemIdFib B (f x)))\r
+\r
+sumToProd (A B:U) (f:A -> B) (gp : sumF A B f) : prodF A B f = \ (x:A) -> (gp.1 x,gp.2 x)\r
+prodToSum (A B:U) (f:A -> B) (h : prodF A B f) : sumF A B f = (\ (x:A) -> (h x).1,\ (x:A) -> (h x).2)\r
+\r
+retSP (A B:U) (f:A->B) (gp:sumF A B f) : Id (sumF A B f) (prodToSum A B f (sumToProd A B f gp)) gp =\r
+ refl (sumF A B f) gp\r
+\r
+corr2 (A B:U) (f:A->B) : prop (sumF A B f) =\r
+ retractProp (sumF A B f) (prodF A B f) (sumToProd A B f) (prodToSum A B f) (retSP A B f) (lemProdF A B f)\r
+\r
+funext (A B:U) (f g:A -> B) (h:(x:A) -> Id B (f x) (g x)) : Id (A->B) f g = <i> \ (x:A) -> (rem@i).1 x\r
+ where rem : Id (sumF A B f) (f,\ (x:A) -> refl B (f x)) (g,h) = corr2 A B f (f,\ (x:A) -> refl B (f x)) (g,h)\r
+\r
+\r
+\r