alternative definition of equivalences

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 3e5d933f9a4d18fddc1e2041b662da4a12b21ac1..52155a99efeb4a9c65750b1eb0008dc26b81ff98 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -137,9 +137,63 @@ secEq (A B : U) (f: equiv A B) : (x:A) -> Id A (invEq A B f (f.1 x)) x =
  secEquiv A B f.1 f.2\r
 \r
 \r
+-- Alternative definition:\r
+fiber' (A B : U) (f : A -> B) (y : B) : U =\r
+  (x : A) * Id B y (f x)\r
 \r
+isContr (A:U) : U = (a:A) * ((x:A) -> Id A a x)\r
 \r
--- Alternative definitions:\r
+propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 =\r
+ <j>(p0 a1@j,\r
+     \ (x:A) -> \r
+        <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),\r
+                                      (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>p1 x@i ])\r
+ where\r
+  a0 : A = z0.1\r
+  p0 : (x:A) -> Id A a0 x = z0.2\r
+  a1 : A = z1.1\r
+  p1 : (x:A) -> Id A a1 x = z1.2\r
+  lem1 (x:A) : IdP (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> p0 (p1 x@i) @ j\r
+ \r
+isEquiv' (A B : U) (f : A -> B) : U = (y:B) -> isContr (fiber' A B f y)\r
+\r
+equiv' (A B : U) : U = (f : A -> B) * isEquiv' A B f\r
+\r
+propIsEquiv' (A B : U) (f : A -> B)\r
+  : prop (isEquiv' A B f) = \ (u0 u1:isEquiv' A B f) -> <i> \ (y:B) -> propIsContr (fiber' A B f y) (u0 y) (u1 y) @ i\r
+\r
+-- lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 :A) \r
+--          (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdP (<i>P (p@i)) b0 b1 =\r
+--  <i>pP (p@i) (comp (<j>P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (<j>P (p@i\/-j)) b1 [(i=1) -> <_>b1])@i\r
+\r
+-- lemSig (A : U) (B : A -> U) (pB : (x : A) -> prop (B x))\r
+--        (u v : (x:A) * B x) (p : Id A u.1 v.1) :\r
+--        Id ((x:A) * B x) u v =\r
+--   <i> (p@i,(lemPropF A B pB u.1 v.1 p u.2 v.2)@i)\r
+\r
+-- propSig (A : U) (B : A -> U) (pA : prop A)\r
+--         (pB : (x : A) -> prop (B x)) (t u : (x:A) * B x) :\r
+--         Id ((x:A) * B x) t u =\r
+--   lemSig A B pB t u (pA t.1 u.1)\r
+\r
+equivLemma' (A B : U)\r
+  : (v w : equiv' A B) -> Id (A -> B) v.1 w.1 -> Id (equiv' A B) v w\r
+  = lemSig (A -> B) (isEquiv' A B) (propIsEquiv' A B)\r
+\r
+-- for univalence\r
+\r
+invEq' (A B:U) (w:equiv' A B) (y:B) : A = (w.2 y).1.1\r
+\r
+retEq' (A B:U) (w:equiv' A B) (y:B) : Id B (w.1 (invEq' A B w y)) y =\r
+ <i>(w.2 y).1.2@-i\r
+\r
+secEq' (A B:U) (w:equiv' A B) (x:A) : Id A (invEq' A B w (w.1 x)) x =\r
+ <i> ((w.2 (w.1 x)).2 (x,<j>w.1 x)@i).1\r
+\r
+\r
+\r
+\r
+-- Another alternative definitions:\r
 \r
 -- isContr (A : U) : U = and (prop A) A\r
 \r
@@ -205,3 +259,4 @@ secEq (A B : U) (f: equiv A B) : (x:A) -> Id A (invEq A B f (f.1 x)) x =
 --             p : Id A x y = <i>(z.2 @ i).1\r
 --             q : IdP (<j>G (p@j)) v (f y w) = <i>((z.2) @ i).2\r
 --    rem7 (z0 z1 : fiber (F x) (G x) (f x) v) : Id (fiber (F x) (G x) (f x) v) z0 z1 = <i>psi ((rem1.1 (phi z0) (phi z1))@i)\r
+\r