From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Fri, 18 Dec 2015 14:08:27 +0000 (-0500)
Subject: alternative definition of equivalences
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=3435cd4f0b66679b8820be3f12470abf1049ea0f;p=cubicaltt.git

alternative definition of equivalences
---

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 3e5d933..52155a9 100644
--- 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
 
 
+-- Alternative definition:
+fiber' (A B : U) (f : A -> B) (y : B) : U =
+  (x : A) * Id B y (f x)
 
+isContr (A:U) : U = (a:A) * ((x:A) -> Id A a x)
 
--- Alternative definitions:
+propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 =
+ <j>(p0 a1@j,
+     \ (x:A) -> 
+        <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),
+                                      (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>p1 x@i ])
+ where
+  a0 : A = z0.1
+  p0 : (x:A) -> Id A a0 x = z0.2
+  a1 : A = z1.1
+  p1 : (x:A) -> Id A a1 x = z1.2
+  lem1 (x:A) : IdP (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> p0 (p1 x@i) @ j
+ 
+isEquiv' (A B : U) (f : A -> B) : U = (y:B) -> isContr (fiber' A B f y)
+
+equiv' (A B : U) : U = (f : A -> B) * isEquiv' A B f
+
+propIsEquiv' (A B : U) (f : A -> B)
+  : 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
+
+-- lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 :A) 
+--          (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdP (<i>P (p@i)) b0 b1 =
+--  <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
+
+-- lemSig (A : U) (B : A -> U) (pB : (x : A) -> prop (B x))
+--        (u v : (x:A) * B x) (p : Id A u.1 v.1) :
+--        Id ((x:A) * B x) u v =
+--   <i> (p@i,(lemPropF A B pB u.1 v.1 p u.2 v.2)@i)
+
+-- propSig (A : U) (B : A -> U) (pA : prop A)
+--         (pB : (x : A) -> prop (B x)) (t u : (x:A) * B x) :
+--         Id ((x:A) * B x) t u =
+--   lemSig A B pB t u (pA t.1 u.1)
+
+equivLemma' (A B : U)
+  : (v w : equiv' A B) -> Id (A -> B) v.1 w.1 -> Id (equiv' A B) v w
+  = lemSig (A -> B) (isEquiv' A B) (propIsEquiv' A B)
+
+-- for univalence
+
+invEq' (A B:U) (w:equiv' A B) (y:B) : A = (w.2 y).1.1
+
+retEq' (A B:U) (w:equiv' A B) (y:B) : Id B (w.1 (invEq' A B w y)) y =
+ <i>(w.2 y).1.2@-i
+
+secEq' (A B:U) (w:equiv' A B) (x:A) : Id A (invEq' A B w (w.1 x)) x =
+ <i> ((w.2 (w.1 x)).2 (x,<j>w.1 x)@i).1
+
+
+
+
+-- Another alternative definitions:
 
 -- isContr (A : U) : U = and (prop A) A
 
@@ -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
 --             q : IdP (<j>G (p@j)) v (f y w) = <i>((z.2) @ i).2
 --    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)
+