+++ /dev/null
-module add where
-
-import nat
-
-add (a : nat) : nat -> nat = split
- zero -> a
- suc n -> suc (add a n)
-
-add_zero : (n : nat) -> Id nat (add zero n) n = split
- zero -> <i> zero
- suc n -> <i> suc (add_zero n @ i)
-
-add_suc (a:nat) : (n : nat) -> Id nat (add (suc a) n) (suc (add a n)) = split
- zero -> <i> suc a
- suc m -> <i> suc (add_suc a m @ i)
-
-add_comm (a : nat) : (n : nat) -> Id nat (add a n) (add n a) = split
- zero -> <i> add_zero a @ -i
- suc m -> <i> comp nat (suc (add_comm a m @ i)) [ (i = 0) -> <j> suc (add a m),
- (i = 1) -> <j> add_suc m a @ -j]
-
-assocAdd (a b:nat) : (c:nat) -> Id nat (add a (add b c)) (add (add a b) c) = split
- zero -> <i>add a b
- suc c1 -> <i>suc (assocAdd a b c1@i)
-
-
--- test (A:U) (a b c d e : A) (p:Id A a b) (q:Id A b c) (r:Id A c d) (s:Id A d e) : Id A a e =
--- <i>comp A (p@i) [ (i=1) -> <i>comp A (q@i) [ (i=1) -> <i>comp A (r@i) [ (i=1) -> s]]]
-
--- data tree = leaf | bin (t0 t1:tree)
-
--- swap : tree -> tree = split
--- leaf -> leaf
--- bin t0 t1 -> bin (swap t1) (swap t0)
-
--- lem : (t:tree) -> Id tree (swap (swap t)) t = split
--- leaf -> <i>leaf
--- bin t0 t1 -> <i>bin (lem t0@i) (lem t1@i)
-
--- pred : nat -> nat = split
--- zero -> zero
--- suc n -> n
-
--- simplAdd (b c :nat) : (a : nat) -> Id nat (add b a) (add c a) -> Id nat b c = split
--- zero -> \ (h:Id nat b c) -> h
--- suc a1 -> \ (h : Id nat (suc (add b a1)) (suc (add c a1))) -> simplAdd b c a1 (<i>pred (h@i))
-
--- corSimplAdd (b c a :nat) (h: Id nat (add a b) (add a c)) : Id nat b c = simplAdd b c a rem
--- where rem : Id nat (add b a) (add c a) =
--- <i>comp nat ((add_comm b a)@i) [(i=1) -> <i>comp nat (h@i) [(i=1) -> add_comm a c]]
-
-
--- leq (b c:nat) : U = (a : nat) * Id nat (add a b) c
\ No newline at end of file
module bool where
-import prelude
+import gradLemma
data bool = false | true
negBoolEq : Id U bool bool =
isoId bool bool negBool negBool negBoolK negBoolK
-test : bool = trans bool bool negBoolEq true
+testFalse : bool = transport negBoolEq true
data F2 = zeroF2 | oneF2
kanBool : Id U bool bool =
kan U bool bool bool bool negBoolEq negBoolEq negBoolEq
-squareBoolF2 : Square U bool bool (refl U bool) bool F2
- boolEqF2 (refl U bool) boolEqF2 =
+squareBoolF2 : Square U bool bool bool F2 (refl U bool)
+ boolEqF2 (refl U bool) boolEqF2 =
<i j> boolEqF2 @ i /\ j
test5 : IdP boolEqF2 true oneF2 =
\r
import prelude\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
+fiber (A B : U) (f : A -> B) (y : B) : U =\r
+ (x : A) * Id B (f x) y\r
+\r
+isEquiv (A B : U) (f : A -> B) : U =\r
+ (s : (y : B) -> fiber A B f y)\r
+ * ((y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w)\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) = lemProp (isEquiv A B f) lem\r
+ where\r
+ isEqf : U = isEquiv A B f\r
+ fibf : (y : B) -> U = fiber A B f\r
+ center : U = (y : B) -> fibf y\r
+ isCenter (s : center) : U = (y : B) (w : fibf y) -> Id (fibf y) (s y) w\r
+ lem (fe : isEqf) : prop isEqf = propSig center isCenter pc pisc\r
+ where\r
+ fibprop (y : B) (u v : fibf y) : Id (fibf y) u v =\r
+ compId (fibf y) u (fe.1 y) v (<i> fe.2 y u @ -i) (fe.2 y v)\r
+ pc : prop center = propPi B fibf fibprop\r
+ pisc (s : center) (g h : isCenter s) : Id (isCenter s) g h =\r
+ <i> \ (y : B) (w : fibf y) ->\r
+ propSet (fibf y) (fibprop y) (s y) w (g y w) (h y w) @ i\r
+\r
+\r
+-- The identity function is an equivalence\r
+idCenter (A : U) (y : A) : fiber A A (idfun A) y = (y, refl A y)\r
+\r
+-- TODO: redifine fiber so this gets nicer?\r
+idIsCenter (A : U) (y : A) (w : fiber A A (idfun A) y)\r
+ : Id (fiber A A (idfun A) y) (idCenter A y) w =\r
+ <i> (w.2 @ -i, <j> w.2 @ j \/ -i)\r
+\r
+idIsEquiv (A : U) : isEquiv A A (idfun A) = (idCenter A,idIsCenter A)\r
+\r
+idEquiv (A : U) : equiv A A = (idfun A, idIsEquiv A)\r
+\r
+-- Transport is an equivalence\r
+-- NB: The proof is taken from the output of a comp U\r
+trans (A B : U) (p : Id U A B) (a : A) : B = transport p a\r
+\r
+transCenter (A B : U) (p : Id U A B) (y : B) : fiber A B (trans A B p) y =\r
+ (comp (<i0> p @ -i0) y []\r
+ ,<i0> comp p (comp (<i0> p @ -i0) y [])\r
+ [ (i0 = 0) -> <i1> comp (<i2> p @ (i1 /\ i2)) (comp (<i0> p @ -i0) y [])\r
+ [ (i1 = 0) -> <i2> comp (<i0> p @ -i0) y [] ]\r
+ , (i0 = 1) -> <i1> comp (<i2> p @ (i1 \/ -i2)) y [ (i1 = 1) -> <i2> y ] ])\r
+\r
+transIsCenter (A B : U) (p : Id U A B) (y : B) (w : fiber A B (trans A B p) y)\r
+ : Id (fiber A B (trans A B p) y) (transCenter A B p y) w\r
+ = <i0>\r
+ ( comp (<i1> p @ -i1) (w.2 @ -i0)\r
+ [ (i0 = 0) -> <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]\r
+ , (i0 = 1) -> <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1) [ (i1 = 1) -> <i2> w.1 ] ]\r
+ , <i1> comp (<i2> p @ i2)\r
+ (comp (<i2> p @ -i2) (w.2 @ (-i0 \/ i1))\r
+ [ (i0 = 0) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ]\r
+ , (i0 = 1)(i1 = 0) ->\r
+ <i2> comp (<i3> p @ (-i2 /\ i3)) (w.1)\r
+ [ (i2 = 1) -> <i3> w.1 ]\r
+ , (i1 = 1) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ] ])\r
+ [ (i0 = 0) -> <i2> comp (<i3> p @ (i2 /\ i3))\r
+ (comp (<i0> p @ -i0) y [ ])\r
+ [ (i1 = 0) ->\r
+ <i3> comp (<i4> p @ (i2 /\ i3 /\ i4))\r
+ (comp (<i0> p @ -i0) y [ ])\r
+ [ (i2 = 0) -> <i4> comp (<i0> p @ -i0) y [ ]\r
+ , (i3 = 0) -> <i4> comp (<i0> p @ -i0) y [ ] ]\r
+ , (i1 = 1) ->\r
+ <i3> comp (<i4> p @ ((i2 /\ i3) \/ -i4)) y\r
+ [ (i2 = 1)(i3 = 1) -> <i4> y ]\r
+ , (i2 = 0) -> <i3> comp (<i0> p @ -i0) y [ ] ]\r
+ , (i0 = 1) ->\r
+ <i2> comp (<i3> p @ (i2 \/ -i3)) (w.2 @ i1)\r
+ [ (i1 = 0) ->\r
+ <i3> comp (<i4> p @ ((i2 /\ i4) \/ (-i3 /\ i4))) (w.1)\r
+ [ (i2 = 0)(i3 = 1) -> <i4> w.1 ]\r
+ , (i1 = 1) ->\r
+ <i3> comp (<i4> p @ (i2 \/ -i3 \/ -i4)) y\r
+ [ (i2 = 1) -> <i4> y, (i3 = 0) -> <i4> y ]\r
+ , (i2 = 1) -> <i3> w.2 @ i1 ]\r
+ , (i1 = 0) ->\r
+ <i2> comp (<i3> p @ (i2 /\ i3))\r
+ (comp (<i1> p @ -i1) (w.2 @ -i0)\r
+ [ (i0 = 0) ->\r
+ <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]\r
+ , (i0 = 1) ->\r
+ <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)\r
+ [ (i1 = 1) -> <i2> w.1 ]\r
+ ])\r
+ [ (i2 = 0) ->\r
+ <i3> comp (<i1> p @ -i1) (w.2 @ -i0)\r
+ [ (i0 = 0) ->\r
+ <i1> comp (<i2> p @ (-i1 \/ -i2)) y\r
+ [ (i1 = 0) -> <i2> y ]\r
+ , (i0 = 1) ->\r
+ <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)\r
+ [ (i1 = 1) -> <i2> w.1 ]\r
+ ]\r
+ ]\r
+ , (i1 = 1) -> <i2> comp (<i3> p @ (i2 \/ -i3)) y [ (i2 = 1) -> <i3> y ] ]\r
+ )\r
+\r
+transIsEquiv (A B : U) (p : Id U A B) : isEquiv A B (trans A B p) =\r
+ (transCenter A B p,transIsCenter A B p)\r
+\r
+transEquiv (A B : U) (p : Id U A B) : equiv A B =\r
+ (trans A B p,transIsEquiv A B p)\r
+\r
+transDelta (A : U) : equiv A A = transEquiv A A (<_> A)\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+-- Alternative definitions:\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
-\r
--- a general lemma about equivalence and fibrations\r
-\r
-Sigma (A:U) (F:A->U) : U = (x:A) * F x\r
-\r
-lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x)\r
- (h : isEquiv (Sigma A F) (Sigma A G) (\ (xp : Sigma A F) -> (xp.1,f xp.1 xp.2))) (x:A) (v:G x) : \r
- isContr (fiber (F x) (G x) (f x) v) = (rem7,psi (rem1.2))\r
- where\r
- AF : U = Sigma A F\r
- AG : U = Sigma A G\r
- g (xp : AF) : AG = (xp.1,f xp.1 xp.2)\r
- rem1 : isContr (fiber AF AG g (x,v)) = h (x,v)\r
- phi (z:fiber (F x) (G x) (f x) v) : fiber AF AG g (x,v) = ((x,z.1),<i>(x,(z.2)@ i))\r
- psi (z:fiber AF AG g (x,v)) : fiber (F x) (G x) (f x) v = transport (<i> (u : F (p@-i)) * IdP (<j>G (p@-i /\ j)) v (f (p@-i) u)) (w,q)\r
- where yu : AF = z.1\r
- y : A = yu.1\r
- w : F y = yu.2\r
- 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
+-- 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
+\r
+-- -- a general lemma about equivalence and fibrations\r
+\r
+-- Sigma (A:U) (F:A->U) : U = (x:A) * F x\r
+\r
+-- lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x)\r
+-- (h : isEquiv (Sigma A F) (Sigma A G) (\ (xp : Sigma A F) -> (xp.1,f xp.1 xp.2))) (x:A) (v:G x) : \r
+-- isContr (fiber (F x) (G x) (f x) v) = (rem7,psi (rem1.2))\r
+-- where\r
+-- AF : U = Sigma A F\r
+-- AG : U = Sigma A G\r
+-- g (xp : AF) : AG = (xp.1,f xp.1 xp.2)\r
+-- rem1 : isContr (fiber AF AG g (x,v)) = h (x,v)\r
+-- phi (z:fiber (F x) (G x) (f x) v) : fiber AF AG g (x,v) = ((x,z.1),<i>(x,(z.2)@ i))\r
+-- psi (z:fiber AF AG g (x,v)) : fiber (F x) (G x) (f x) v = transport (<i> (u : F (p@-i)) * IdP (<j>G (p@-i /\ j)) v (f (p@-i) u)) (w,q)\r
+-- where yu : AF = z.1\r
+-- y : A = yu.1\r
+-- w : F y = yu.2\r
+-- 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
module gradLemma where
-import prelude
+import equiv
+
+-- Gradlemma:
lemIso (A B : U) (f : A -> B) (g : B -> A)
- (s : (y:B) -> Id B (f (g y)) y)
- (t : (x:A) -> Id A (g (f x)) x)
- (y:B) (x0 x1:A) (p0 : Id B y (f x0)) (p1 : Id B y (f x1)) :
- Id ((x:A) * Id B y (f x)) (x0,p0) (x1,p1) = <i> (p @ i, sq1 @ i)
- where
- rem0 : Id A (g y) x0 =
- <i> comp (<_> A) (g (p0 @ i)) [ (i = 0) -> <_> g y, (i = 1) -> t x0 ]
- rem1 : Id A (g y) x1 =
- <i> comp (<_> A) (g (p1 @ i)) [ (i = 0) -> <_> g y, (i = 1) -> t x1 ]
- p : Id A x0 x1 = <i> comp (<_> A) (g y) [ (i = 0) -> rem0, (i = 1) -> rem1 ]
-
- fill0 : Square A (g y) (g (f x0)) (<i> g (p0 @ i)) (g y) x0 rem0 (<i> g y) (t x0) =
- <i j> comp (<_> A) (g (p0@i)) [ (i = 0) -> <_> g y
- , (i = 1) -> <k> t x0 @ j /\ k
- , (j = 0) -> <_> g (p0 @ i) ]
-
- fill1 : Square A (g y) (g (f x1)) (<i> g (p1 @ i)) (g y) x1 rem1 (<i> g y) (t x1) =
- <i j> comp (<_> A) (g (p1@i)) [ (i = 0) -> <_> g y
- , (i = 1) -> <k> t x1 @ j /\ k
- , (j = 0) -> <_> g (p1 @ i) ]
-
- fill2 : Square A (g y) (g y) (<_> g y) x0 x1 p rem0 rem1 =
- <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
- , (i = 1) -> <k> rem1 @ j /\ k
- , (j = 0) -> <_> g y ]
-
- sq : Square A (g y) (g y) (<_> g y) (g (f x0)) (g (f x1)) (<i> g (f (p @ i)))
- (<i> g (p0 @ i)) (<i> g (p1 @ i)) =
- <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
- , (i = 1) -> <k> fill1 @ j @ -k
- , (j = 0) -> <_> g y
- , (j = 1) -> <k> t (p @ i) @ -k ]
-
- sq1 : Square B y y (<_> y) (f x0) (f x1) (<i> f (p @ i)) p0 p1 =
- <i j> comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j)
- , (i = 1) -> s (p1 @ j)
- , (j = 0) -> s y
- , (j = 1) -> s (f (p @ i)) ]
+ (s : (y : B) -> Id B (f (g y)) y)
+ (t : (x : A) -> Id A (g (f x)) x)
+ (y : B) (x0 x1 : A) (p0 : Id B (f x0) y) (p1 : Id B (f x1) y) :
+ Id (fiber A B f y) (x0,p0) (x1,p1) = <i> (p @ i,sq1 @ i)
+ where
+ rem0 : Id A x0 (g y) =
+ <i> comp (<_> A) (g (p0 @ i)) [ (i = 0) -> t x0, (i = 1) -> <_> g y ]
+
+ rem1 : Id A x1 (g y) =
+ <i> comp (<_> A) (g (p1 @ i)) [ (i = 0) -> t x1, (i = 1) -> <_> g y ]
+
+ p : Id A x0 x1 =
+ <i> comp (<_> A) (g y) [ (i = 0) -> <j> rem0 @ -j
+ , (i = 1) -> <j> rem1 @ -j ]
+
+
+ fill0 : Square A (g (f x0)) (g y) x0 (g y)
+ (<i> g (p0 @ i)) rem0 (t x0) (<i> g y) =
+ <i j> comp (<_> A) (g (p0 @ i)) [ (i = 0) -> <k> t x0 @ j /\ k
+ , (i = 1) -> <_> g y
+ , (j = 0) -> <_> g (p0 @ i) ]
+
+ fill1 : Square A (g (f x1)) (g y) x1 (g y)
+ (<i> g (p1 @ i)) rem1 (t x1) (<i> g y) =
+ <i j> comp (<_> A) (g (p1 @ i)) [ (i = 0) -> <k> t x1 @ j /\ k
+ , (i = 1) -> <_> g y
+ , (j = 0) -> <_> g (p1 @ i) ]
+
+ fill2 : Square A x0 x1 (g y) (g y)
+ p (<_> g y) rem0 rem1 =
+ <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j \/ -k
+ , (i = 1) -> <k> rem1 @ j \/ -k
+ , (j = 1) -> <_> g y ]
+
+ sq : Square A (g (f x0)) (g (f x1)) (g y) (g y)
+ (<i> g (f (p @ i))) (<i> g y)
+ (<j> g (p0 @ j)) (<j> g (p1 @ j)) =
+ <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
+ , (i = 1) -> <k> fill1 @ j @ -k
+ , (j = 1) -> <_> g y
+ , (j = 0) -> <k> t (p @ i) @ -k ]
+
+ sq1 : Square B (f x0) (f x1) y y
+ (<i> f (p @ i)) (<_> y) p0 p1 =
+ <i j> comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j)
+ , (i = 1) -> s (p1 @ j)
+ , (j = 0) -> s (f (p @ i))
+ , (j = 1) -> s y ]
+
+gradLemma (A B : U) (f : A -> B) (g : B -> A)
+ (s : (y : B) -> Id B (f (g y)) y)
+ (t : (x : A) -> Id A (g (f x)) x) : isEquiv A B f = (fCenter,fIsCenter)
+ where
+ fCenter (y : B) : fiber A B f y = (g y,s y)
+ fIsCenter (y : B) (w : fiber A B f y) : Id (fiber A B f y) (fCenter y) w =
+ lemIso A B f g s t y (fCenter y).1 w.1 (fCenter y).2 w.2
+
+-- Using gradLemma we get that any isomorphism gives a line in the universe
+isoId (A B : U) (f : A -> B) (g : B -> A)
+ (s : (y : B) -> Id B (f (g y)) y)
+ (t : (x : A) -> Id A (g (f x)) x) : Id U A B =
+ <i> glue B [ (i = 0) -> (A,f,gradLemma A B f g s t)
+ , (i = 1) -> (B,transDelta B) ]
+
+
+
+
+-- OLD CODE:
+-- lemIso with equalities on other direction:
-- lemIso (A B : U) (f : A -> B) (g : B -> A)
-- (s : (y:B) -> Id B (f (g y)) y)
-- (t : (x:A) -> Id A (g (f x)) x)
-- (y:B) (x0 x1:A) (p0 : Id B y (f x0)) (p1 : Id B y (f x1)) :
--- Id ((x:A) * Id B y (f x)) (x0,p0) (x1,p1) = <i>(p@i,sq1@i)
+-- Id ((x:A) * Id B y (f x)) (x0,p0) (x1,p1) = <i> (p @ i, sq1 @ i)
-- where
--- rem0 : Id A (g y) x0 = <i> comp A (g (p0 @ i)) [(i=1) -> t x0]
--- rem1 : Id A (g y) x1 = <i> comp A (g (p1 @ i)) [(i=1) -> t x1]
--- fill0 : Square A (g y) (g (f x0)) (<i>g (p0 @ i)) (g y) x0 rem0 (<i>(g y)) (t x0) =
--- <i j>comp A (g (p0@i)) [(i=1) -> <k>(t x0)@k/\j ]
--- fill1 : Square A (g y) (g (f x1)) (<i>g (p1 @ i)) (g y) x1 rem1 (<i>(g y)) (t x1) =
--- <i j>comp A (g (p1@i)) [(i=1) -> <k>(t x1)@k/\j ]
--- p : Id A x0 x1 = <i> comp A (g y) [(i=0) -> rem0, (i=1) -> rem1]
--- fill : Square A (g y) (g y) (refl A (g y)) x0 x1 p rem0 rem1 =
--- <i j> comp A (g y) [(i=0) -> <k>(rem0@j/\k), (i=1) -> <k>(rem1@j/\k)]
--- sq : Square A (g y) (g y) (refl A (g y)) (g (f x0)) (g (f x1)) (<i>(g (f (p@i))))
--- (<i>g (p0@i)) (<i>g (p1@i)) =
--- <i j>comp A ((fill@i)@j) [(i=0) -> <k>((fill0@j)@-k), (i=1)-><k>((fill1@j)@-k),(j=1) -> <k>(t (p@i))@-k]
--- sq1 : Square B y y (refl B y) (f x0) (f x1) (<i>f (p@i)) p0 p1 =
--- <i j>comp B (f ((sq@i)@j)) [(i=0) -> s (p0@j),(i=1) -> s (p1@j),(j=0) -> s y,(j=1)-> s (f (p@i))]
-
--- special case
-
-corrIso (A B : U) (f : A -> B) (g : B -> A)
- (s : (y:B) -> Id B (f (g y)) y)
- (t : (x:A) -> Id A (g (f x)) x)
- (x0:A) :
- Id ((x:A) * Id B (f x0) (f x)) (x0,refl B (f x0)) (g (f x0),<i>((s (f x0))@-i)) =
- lemIso A B f g s t (f x0) x0 (g (f x0)) (refl B (f x0)) (<i>((s (f x0))@-i))
+-- rem0 : Id A (g y) x0 =
+-- <i> comp (<_> A) (g (p0 @ i)) [ (i = 0) -> <_> g y, (i = 1) -> t x0 ]
+-- rem1 : Id A (g y) x1 =
+-- <i> comp (<_> A) (g (p1 @ i)) [ (i = 0) -> <_> g y, (i = 1) -> t x1 ]
+-- p : Id A x0 x1 = <i> comp (<_> A) (g y) [ (i = 0) -> rem0, (i = 1) -> rem1 ]
+
+-- fill0 : Square A (g y) (g (f x0)) (<i> g (p0 @ i)) (g y) x0 rem0 (<i> g y) (t x0) =
+-- <i j> comp (<_> A) (g (p0@i)) [ (i = 0) -> <_> g y
+-- , (i = 1) -> <k> t x0 @ j /\ k
+-- , (j = 0) -> <_> g (p0 @ i) ]
+
+-- fill1 : Square A (g y) (g (f x1)) (<i> g (p1 @ i)) (g y) x1 rem1 (<i> g y) (t x1) =
+-- <i j> comp (<_> A) (g (p1@i)) [ (i = 0) -> <_> g y
+-- , (i = 1) -> <k> t x1 @ j /\ k
+-- , (j = 0) -> <_> g (p1 @ i) ]
+
+-- fill2 : Square A (g y) (g y) (<_> g y) x0 x1 p rem0 rem1 =
+-- <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
+-- , (i = 1) -> <k> rem1 @ j /\ k
+-- , (j = 0) -> <_> g y ]
+
+-- sq : Square A (g y) (g y) (<_> g y) (g (f x0)) (g (f x1)) (<i> g (f (p @ i)))
+-- (<i> g (p0 @ i)) (<i> g (p1 @ i)) =
+-- <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
+-- , (i = 1) -> <k> fill1 @ j @ -k
+-- , (j = 0) -> <_> g y
+-- , (j = 1) -> <k> t (p @ i) @ -k ]
+
+-- sq1 : Square B y y (<_> y) (f x0) (f x1) (<i> f (p @ i)) p0 p1 =
+-- <i j> comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j)
+-- , (i = 1) -> s (p1 @ j)
+-- , (j = 0) -> s y
+-- , (j = 1) -> s (f (p @ i)) ]
+
+-- -- special case
+
+-- corrIso (A B : U) (f : A -> B) (g : B -> A)
+-- (s : (y:B) -> Id B (f (g y)) y)
+-- (t : (x:A) -> Id A (g (f x)) x)
+-- (x0:A) :
+-- Id ((x:A) * Id B (f x0) (f x)) (x0,refl B (f x0)) (g (f x0),<i>((s (f x0))@-i)) =
+-- lemIso A B f g s t (f x0) x0 (g (f x0)) (refl B (f x0)) (<i>((s (f x0))@-i))
\r
import prelude\r
\r
-hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) :\r
- (b : A) (p : Id A a b) ->\r
- Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) =\r
- J A a (\ (b:A) (p:Id A a b) -> Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p))\r
- (refl (Id A a a) (f a a (refl A a)))\r
+hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :\r
+ Square A a a a b (refl A a) p (f a (refl A a)) (f b p) = \r
+ comp (<i> Square A a a a (p @ i) (<_> a) (<j> p @ i /\ j)\r
+ (f a (<_> a)) (f (p @ i) (<j> p @ i /\ j)))\r
+ (<i> f a (<_> a)) []\r
\r
-hedberg (A : U) (h : discrete A) : set A = \(a b : A) (p q : Id A a b) ->\r
- let rem1 (x y : A) : exConst (Id A x y) = decConst (Id A x y) (h x y)\r
+hedbergStable (A : U) (a b : A) (h : (x : A) -> stable (Id A a x))\r
+ (p q : Id A a b) : Id (Id A a b) p q =\r
+ <j i> comp (<_> A) a [ (j = 0) -> rem2 @ i\r
+ , (j = 1) -> rem3 @ i\r
+ , (i = 0) -> r\r
+ , (i = 1) -> rem4 @ j]\r
+ where \r
+ ra : Id A a a = <_> a \r
+ rem1 (x : A) : exConst (Id A a x) = stableConst (Id A a x) (h x)\r
+ f (x : A) : Id A a x -> Id A a x = (rem1 x).1\r
+ fIsConst (x : A) : const (Id A a x) (f x) = (rem1 x).2\r
+ rem4 : Square A a a b b ra (refl A b) (f b p) (f b q) = fIsConst b p q\r
+ r : Id A a a = f a ra\r
+ rem2 : Square A a a a b ra p r (f b p) = hedbergLemma A a b f p\r
+ rem3 : Square A a a a b ra q r (f b q) = hedbergLemma A a b f q\r
\r
- f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1\r
+hedbergS (A:U) (h : (a x:A) -> stable (Id A a x)) : set A =\r
+ \(a b : A) -> hedbergStable A a b (h a)\r
\r
- fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2\r
+hedberg (A : U) (h : discrete A) : set A =\r
+ \(a b : A) -> hedbergStable A a b (\(b : A) -> decStable (Id A a b) (h a b))\r
\r
- r : Id A a a = f a a (refl A a)\r
\r
- rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p\r
\r
- rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q\r
\r
- rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q\r
+-- Alternative version:\r
\r
- rem5 : Id (Id A a b) (compId A a a b r p) (compId A a a b r q) =\r
- compDown (Id A a b) (compId A a a b r p) (f a b p) (compId A a a b r q)\r
- (f a b q) rem2 rem3 rem4\r
- in lemSimpl A a a b r p q rem5\r
+-- hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) :\r
+-- (b : A) (p : Id A a b) ->\r
+-- Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) =\r
+-- J A a (\ (b:A) (p:Id A a b) -> Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p))\r
+-- (refl (Id A a a) (f a a (refl A a)))\r
+\r
+-- hedberg (A : U) (h : discrete A) : set A = \(a b : A) (p q : Id A a b) ->\r
+-- let rem1 (x y : A) : exConst (Id A x y) = decConst (Id A x y) (h x y)\r
+\r
+-- f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1\r
+\r
+-- fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2\r
+\r
+-- r : Id A a a = f a a (refl A a)\r
+\r
+-- rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p\r
+\r
+-- rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q\r
+\r
+-- rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q\r
+\r
+-- rem5 : Id (Id A a b) (compId A a a b r p) (compId A a a b r q) =\r
+-- compDown (Id A a b) (compId A a a b r p) (f a b p) (compId A a a b r q)\r
+-- (f a b q) rem2 rem3 rem4\r
+-- in lemSimpl A a a b r p q rem5\r
\r
import nat\r
import discor\r
+import gradLemma\r
\r
-- inl = neg, inr = pos\r
Z : U = or nat nat\r
\r
sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ\r
\r
-ZSet : set Z = corrhedberg Z (orDisc nat nat natDec natDec)
\ No newline at end of file
+ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)
\ No newline at end of file
module interval where
-import prelude
+import gradLemma
data I = zero | one | seg <i> [(i = 0) -> zero, (i = 1) -> one]
module nat where
-import prelude
-import newhedberg
+import hedberg
data nat = zero | suc (n : nat)
zero -> m
suc n -> suc (add m n)
+add_zero : (n : nat) -> Id nat (add zero n) n = split
+ zero -> <i> zero
+ suc n -> <i> suc (add_zero n @ i)
+
+add_suc (a:nat) : (n : nat) -> Id nat (add (suc a) n) (suc (add a n)) = split
+ zero -> <i> suc a
+ suc m -> <i> suc (add_suc a m @ i)
+
+add_comm (a : nat) : (n : nat) -> Id nat (add a n) (add n a) = split
+ zero -> <i> add_zero a @ -i
+ suc m -> <i> comp (<_> nat) (suc (add_comm a m @ i))
+ [ (i = 0) -> <j> suc (add a m)
+ , (i = 1) -> <j> add_suc m a @ -j ]
+
+assocAdd (a b:nat) : (c:nat) -> Id nat (add a (add b c)) (add (add a b) c) = split
+ zero -> <i>add a b
+ suc c1 -> <i>suc (assocAdd a b c1@i)
+
+
add' : nat -> nat -> nat = split
zero -> \(x : nat) -> x
suc n -> \(x : nat) -> suc (add' n x)
(\ (m:nat) -> decEqCong (Id nat n m) (Id nat (suc n) (suc m)) (\ (p:Id nat n m) -> <i> suc (p @ i))
(sucInj n m) (natDec n m))
--- natSet : set nat = hedberg nat natDec
-natSet : set nat = corrhedberg nat natDec
-
+natSet : set nat = hedberg nat natDec
+++ /dev/null
-module newhedberg where\r
-\r
-import prelude\r
-\r
-hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :\r
- Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = \r
- comp (<i> Square A a a (<_> a) a (p @ i) (<j> p @ i /\ j)\r
- (f a (<_> a)) (f (p @ i) (<j> p @ i /\ j)))\r
- (<i> f a (<_> a)) []\r
-\r
-hedberg (A : U) (a b : A) (h : (x : A) -> stable (Id A a x))\r
- (p q : Id A a b) : Id (Id A a b) p q =\r
- <j i> comp (<_> A) a [ (j = 0) -> rem2 @ i\r
- , (j = 1) -> rem3 @ i\r
- , (i = 0) -> r\r
- , (i = 1) -> rem4 @ j]\r
- where \r
- ra : Id A a a = <_> a \r
- rem1 (x : A) : exConst (Id A a x) = stableConst (Id A a x) (h x)\r
- f (x : A) : Id A a x -> Id A a x = (rem1 x).1\r
- fIsConst (x : A) : const (Id A a x) (f x) = (rem1 x).2\r
- rem4 : Square A a a ra b b (refl A b) (f b p) (f b q) = fIsConst b p q\r
- r : Id A a a = f a ra\r
- rem2 : Square A a a ra a b p r (f b p) = hedbergLemma A a b f p\r
- rem3 : Square A a a ra a b q r (f b q) = hedbergLemma A a b f q\r
-\r
-hedbergS (A:U) (h : (a x:A) -> stable (Id A a x)) : set A =\r
- \(a b : A) -> hedberg A a b (h a)\r
-\r
-corrhedberg (A : U) (h : discrete A) : set A =\r
- \(a b : A) -> hedberg A a b (\(b : A) -> decStable (Id A a b) (h a b))
\ No newline at end of file
-- lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p =
-- <j i> comp A (comp A (p @ i) [(i=1) -> <k> q @ (-j /\ k)]) [(i=1) -> <k> q @ (-j /\ - k)]
--- lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p) (refl A b) =
--- <j i> comp A (p @ (-i \/ j)) [(i=1) -> <k> p @ (j \/ k)]
-
+lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p) (refl A b) =
+ <j i> comp (<_>A) (p @ (-i \/ j)) [(i=0) -> <l>b, (j=1) -> <l>b, (i=1) -> <k> p @ (j \/ k)]
+
test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
idfun (A : U) (a : A) : A = a
--- isoId (A B : U) (f : A -> B) (g : B -> A)
--- (s : (y:B) -> Id B (f (g y)) y)
--- (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
--- <i> glue A [ (i=0) -> (A,idfun A,idfun A,refl A,refl A), (i = 1) -> (B,g,f,t,s) ]
-
--- isoId' (A B : U) (f : A -> B) (g : B -> A)
--- (s : (y:B) -> Id B (f (g y)) y)
--- (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
--- <i> glue A
--- [ (i = 1) -> (B,g,f,t,s)
--- , (i = 0) ->
--- (A
--- ,\ (x : A) -> comp (<_> A) x [ ]
--- ,\ (y : A) -> comp (<_> A) y [ ]
--- ,\ (y : A) -> <i> comp (<_> A) (comp (<_> A) y [ ])
--- [ (i = 0) -> <j> comp (<_> A) (comp (<_> A) y [ ])
--- [ (j = 0) -> <_> comp (<_> A) y [ ] ]
--- , (i = 1) -> <j> comp (<_> A) y [ (j = 1) -> <_> y ]
--- ]
--- ,\ (x : A) -> <i> comp (<_> A) (comp (<_> A) x [ ])
--- [ (i = 0) -> <j> comp (<_> A) (comp (<_> A) x [ ])
--- [ (j = 0) -> <_> comp (<_> A) x [ ] ]
--- , (i = 1) -> <j> comp (<_> A) x [ (j = 1) -> <_> x ] ])
--- ]
-
--- isoIdRef (A : U) :
--- Id (Id U A A) (refl U A) (isoId A A (idfun A) (idfun A) (refl A) (refl A)) =
--- <i j> glueLine j i A
-
-- u
-- a0 -----> a1
-- | |
-- V V
-- b0 -----> b1
-- v
-
-Square (A : U) (a0 a1 : A) (u : Id A a0 a1)
- (b0 b1 : A) (v : Id A b0 b1)
+Square (A : U) (a0 a1 b0 b1 : A)
+ (u : Id A a0 a1) (v : Id A b0 b1)
(r0 : Id A a0 b0) (r1 : Id A a1 b1) : U
= IdP (<i> (IdP (<j> A) (u @ i) (v @ i))) r0 r1
-constSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p =
+constSquare (A : U) (a : A) (p : Id A a a) : Square A a a a a p p p p =
<i j> comp (<_>A) a
[(i = 0) -> <k> p @ (j \/ - k),
(i = 1) -> <k> p @ (j /\ k),
setIsProp (A : U) (f g : set A) : Id (set A) f g =
<i> \(a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i
-propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x))
- (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1
- = <i> \ (x:A) -> (h x (f0 x) (f1 x)) @ i
-
IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U =
IdP (<i> P (p @ i)) u0 u1
+lemProp (A : U) (h : A -> prop A) : prop A = \ (a : A) -> h a a
+
+propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x))
+ (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1
+ = <i> \ (x:A) -> (h x (f0 x) (f1 x)) @ i
lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a :A) :
(a1 : A) (p : Id A a a1) (b0 : P a) (b1 : P a1) -> IdP (<i>P (p@i)) b0 b1 =
J A a (\ (a1 : A) (p : Id A a a1) -> (b0 : P a) (b1 : P a1) -> IdP (<i>P (p@i)) b0 b1) rem
where rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a
-
--- 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) : IdS A P a0 a1 p b0 b1 =
--- <i> (pP (p @ i) (comp (<j> P (p @ i /\ j)) b0 [ ])
--- (comp (<j> P (p @ i \/ -j)) 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)
+
+isContr (A : U) : U = (x : A) * ((y : A) -> Id A x y)
+
+propIsContr (A : U) : prop (isContr A) = lemProp (isContr A) rem
+ where
+ rem (t : isContr A) : prop (isContr A) = propSig A T pA pB
+ where
+ T (x : A) : U = (y : A) -> Id A x y
+ pA (x y : A) : Id A x y = compId A x t.1 y (<i> t.2 x @ -i) (t.2 y)
+ pB (x : A) : prop (T x) =
+ propPi A (\ (y : A) -> Id A x y) (propSet A pA x)
-- Basic data types
(x y : A) (q: Id B (f x) (f y)) : Id A x y = \r
compUp A (g (f x)) x (g (f y)) y (rfg x) (rfg y) (<i> (g (q @ i)))\r
\r
-lemRSquare (A B : U) (f : A -> B) (g : B -> A) (rfg: retract A B f g)(x y:A) (p : Id A x y) :\r
- Square A (g (f x)) (g (f y)) (<i> g (f (p @ i))) x y\r
- (retractInv A B f g rfg x y (<i> f (p@ i))) (rfg x) (rfg y) =\r
- <j i> comp A (g (f (p @ j))) [(j=0) -> <l> (rfg x) @ (i/\l), (j=1) -> <l> (rfg y) @ (i/\l)]\r
-\r
-retractId (A B : U)(f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y :A) (p:Id A x y) :\r
- Id (Id A x y) (retractInv A B f g rfg x y (<i> f (p@ i))) p =\r
- <i j> comp A (g (f (p @ j))) [(j=0) -> rfg x,(j=1) -> rfg y,\r
- (i=0) -> (lemRSquare A B f g rfg x y p) @ j,(i=1) -> rfg (p @ j)]\r
-\r
-retractSet (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g)\r
- (sB : set B) (x y : A) : prop (Id A x y) =\r
- retractProp (Id A x y) (Id B (f x) (f y)) (mapOnPath A B f x y)\r
- (retractInv A B f g rfg x y) (retractId A B f g rfg x y) (sB (f x) (f y))\r
+-- lemRSquare (A B : U) (f : A -> B) (g : B -> A) (rfg: retract A B f g)(x y:A) (p : Id A x y) :\r
+-- Square A (g (f x)) (g (f y)) (<i> g (f (p @ i))) x y\r
+-- (retractInv A B f g rfg x y (<i> f (p@ i))) (rfg x) (rfg y) =\r
+-- <j i> comp A (g (f (p @ j))) [(j=0) -> <l> (rfg x) @ (i/\l), (j=1) -> <l> (rfg y) @ (i/\l)]\r
+\r
+-- retractId (A B : U)(f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y :A) (p:Id A x y) :\r
+-- Id (Id A x y) (retractInv A B f g rfg x y (<i> f (p@ i))) p =\r
+-- <i j> comp A (g (f (p @ j))) [(j=0) -> rfg x,(j=1) -> rfg y,\r
+-- (i=0) -> (lemRSquare A B f g rfg x y p) @ j,(i=1) -> rfg (p @ j)]\r
+\r
+-- retractSet (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g)\r
+-- (sB : set B) (x y : A) : prop (Id A x y) =\r
+-- retractProp (Id A x y) (Id B (f x) (f y)) (mapOnPath A B f x y)\r
+-- (retractInv A B f g rfg x y) (retractId A B f g rfg x y) (sB (f x) (f y))\r
\r
+++ /dev/null
-module univ where
-
--- Some things from the prelude
-
-Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
-
-refl (A : U) (a : A) : Id A a a = <i> a
-
-mapOnPath (A B : U) (f : A -> B) (a b : A)
- (p : Id A a b) : Id B (f a) (f b) = <i> f (p @ i)
-
-funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
- (p : (x : A) -> Id (B x) (f x) (g x)) :
- Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i
-
-subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
- comp (mapOnPath A U P a b p) e []
-
-singl (A : U) (a : A) : U = (x : A) * Id A a x
-
-contrSingl (A : U) (a b : A) (p : Id A a b) :
- Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i/\j)
-
-J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
- (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p =
- subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d
- where T (z : singl A a) : U = C (z.1) (z.2)
-
-compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
- <i> comp (<_>A) (p @ i) [ (i = 1) -> q, (i=0) -> <_> a ]
-
-prop (A : U) : U = (a b : A) -> Id A a b
-
-lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a :A) :
- (a1 : A) (p : Id A a a1) (b0 : P a) (b1 : P a1) -> IdP (<i>P (p@i)) b0 b1 =
- J A a (\ (a1 : A) (p : Id A a a1) -> (b0 : P a) (b1 : P a1) -> IdP (<i>P (p@i)) b0 b1) rem
- where rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a
-
-lemProp (A : U) (h : A -> prop A) : prop A = \ (a : A) -> h a a
-
-propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x))
- (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1
- = <i> \ (x:A) -> (h x (f0 x) (f1 x)) @ 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)
-
-propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q =
- <j i> comp (<_> A) a [ (i = 0) -> h a a
- , (i = 1) -> h a b
- , (j = 0) -> h a (p @ i)
- , (j = 1) -> h a (q @ i)]
-
-isContr (A : U) : U = (x : A) * ((y : A) -> Id A x y)
-
-propIsContr (A : U) : prop (isContr A) = lemProp (isContr A) rem
- where
- rem (t : isContr A) : prop (isContr A) = propSig A T pA pB
- where
- T (x : A) : U = (y : A) -> Id A x y
- pA (x y : A) : Id A x y = compId A x t.1 y (<i> t.2 x @ -i) (t.2 y)
- pB (x : A) : prop (T x) =
- propPi A (\ (y : A) -> Id A x y) (propSet A pA x)
-
-----------------------------------------------------------------------
-
-fiber (A B : U) (f : A -> B) (y : B) : U =
- (x : A) * Id B (f x) y
-
-isEquiv (A B : U) (f : A -> B) : U =
- (s : (y : B) -> fiber A B f y)
- * ((y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w)
-
-equiv (A B : U) : U = (f : A -> B) * isEquiv A B f
-
--- Gradlemma:
-
--- u
--- a0 -----> a1
--- | |
--- r0 | | r1
--- | |
--- V V
--- b0 -----> b1
--- v
-Square (A : U) (a0 a1 b0 b1 : A)
- (u : Id A a0 a1) (v : Id A b0 b1)
- (r0 : Id A a0 b0) (r1 : Id A a1 b1) : U
- = IdP (<i> (IdP (<j> A) (u @ i) (v @ i))) r0 r1
-
-lemIso (A B : U) (f : A -> B) (g : B -> A)
- (s : (y : B) -> Id B (f (g y)) y)
- (t : (x : A) -> Id A (g (f x)) x)
- (y : B) (x0 x1 : A) (p0 : Id B (f x0) y) (p1 : Id B (f x1) y) :
- Id (fiber A B f y) (x0,p0) (x1,p1) = <i> (p @ i,sq1 @ i)
- where
- rem0 : Id A x0 (g y) =
- <i> comp (<_> A) (g (p0 @ i)) [ (i = 0) -> t x0, (i = 1) -> <_> g y ]
-
- rem1 : Id A x1 (g y) =
- <i> comp (<_> A) (g (p1 @ i)) [ (i = 0) -> t x1, (i = 1) -> <_> g y ]
-
- p : Id A x0 x1 =
- <i> comp (<_> A) (g y) [ (i = 0) -> <j> rem0 @ -j
- , (i = 1) -> <j> rem1 @ -j ]
-
-
- fill0 : Square A (g (f x0)) (g y) x0 (g y)
- (<i> g (p0 @ i)) rem0 (t x0) (<i> g y) =
- <i j> comp (<_> A) (g (p0 @ i)) [ (i = 0) -> <k> t x0 @ j /\ k
- , (i = 1) -> <_> g y
- , (j = 0) -> <_> g (p0 @ i) ]
-
- fill1 : Square A (g (f x1)) (g y) x1 (g y)
- (<i> g (p1 @ i)) rem1 (t x1) (<i> g y) =
- <i j> comp (<_> A) (g (p1 @ i)) [ (i = 0) -> <k> t x1 @ j /\ k
- , (i = 1) -> <_> g y
- , (j = 0) -> <_> g (p1 @ i) ]
-
- fill2 : Square A x0 x1 (g y) (g y)
- p (<_> g y) rem0 rem1 =
- <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j \/ -k
- , (i = 1) -> <k> rem1 @ j \/ -k
- , (j = 1) -> <_> g y ]
-
- sq : Square A (g (f x0)) (g (f x1)) (g y) (g y)
- (<i> g (f (p @ i))) (<i> g y)
- (<j> g (p0 @ j)) (<j> g (p1 @ j)) =
- <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
- , (i = 1) -> <k> fill1 @ j @ -k
- , (j = 1) -> <_> g y
- , (j = 0) -> <k> t (p @ i) @ -k ]
-
- sq1 : Square B (f x0) (f x1) y y
- (<i> f (p @ i)) (<_> y) p0 p1 =
- <i j> comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j)
- , (i = 1) -> s (p1 @ j)
- , (j = 0) -> s (f (p @ i))
- , (j = 1) -> s y ]
-
-gradLemma (A B : U) (f : A -> B) (g : B -> A)
- (s : (y : B) -> Id B (f (g y)) y)
- (t : (x : A) -> Id A (g (f x)) x) : isEquiv A B f = (fCenter,fIsCenter)
- where
- fCenter (y : B) : fiber A B f y = (g y,s y)
- fIsCenter (y : B) (w : fiber A B f y) : Id (fiber A B f y) (fCenter y) w =
- lemIso A B f g s t y (fCenter y).1 w.1 (fCenter y).2 w.2
-
-
--- The identity function is an equivalence
-idFun (A : U) (a : A) : A = a
-
-idCenter (A : U) (y : A) : fiber A A (idFun A) y = (y, refl A y)
-
--- TODO: redifine fiber so this gets nicer?
-idIsCenter (A : U) (y : A) (w : fiber A A (idFun A) y)
- : Id (fiber A A (idFun A) y) (idCenter A y) w =
- <i> (w.2 @ -i, <j> w.2 @ j \/ -i)
-
-idIsEquiv (A : U) : isEquiv A A (idFun A) = (idCenter A,idIsCenter A)
-
-idEquiv (A : U) : equiv A A = (idFun A, idIsEquiv A)
-
-
--- Transport is an equivalence
--- NB: The proof is taken from the output of a comp U
-trans (A B : U) (p : Id U A B) (a : A) : B = comp p a []
-
-transCenter (A B : U) (p : Id U A B) (y : B) : fiber A B (trans A B p) y =
- (comp (<i0> p @ -i0) y []
- ,<i0> comp p (comp (<i0> p @ -i0) y [])
- [ (i0 = 0) -> <i1> comp (<i2> p @ (i1 /\ i2)) (comp (<i0> p @ -i0) y [])
- [ (i1 = 0) -> <i2> comp (<i0> p @ -i0) y [] ]
- , (i0 = 1) -> <i1> comp (<i2> p @ (i1 \/ -i2)) y [ (i1 = 1) -> <i2> y ] ])
-
-transIsCenter (A B : U) (p : Id U A B) (y : B) (w : fiber A B (trans A B p) y)
- : Id (fiber A B (trans A B p) y) (transCenter A B p y) w
- = <i0>
- ( comp (<i1> p @ -i1) (w.2 @ -i0)
- [ (i0 = 0) -> <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]
- , (i0 = 1) -> <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1) [ (i1 = 1) -> <i2> w.1 ] ]
- , <i1> comp (<i2> p @ i2)
- (comp (<i2> p @ -i2) (w.2 @ (-i0 \/ i1))
- [ (i0 = 0) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ]
- , (i0 = 1)(i1 = 0) ->
- <i2> comp (<i3> p @ (-i2 /\ i3)) (w.1)
- [ (i2 = 1) -> <i3> w.1 ]
- , (i1 = 1) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ] ])
- [ (i0 = 0) -> <i2> comp (<i3> p @ (i2 /\ i3))
- (comp (<i0> p @ -i0) y [ ])
- [ (i1 = 0) ->
- <i3> comp (<i4> p @ (i2 /\ i3 /\ i4))
- (comp (<i0> p @ -i0) y [ ])
- [ (i2 = 0) -> <i4> comp (<i0> p @ -i0) y [ ]
- , (i3 = 0) -> <i4> comp (<i0> p @ -i0) y [ ] ]
- , (i1 = 1) ->
- <i3> comp (<i4> p @ ((i2 /\ i3) \/ -i4)) y
- [ (i2 = 1)(i3 = 1) -> <i4> y ]
- , (i2 = 0) -> <i3> comp (<i0> p @ -i0) y [ ] ]
- , (i0 = 1) ->
- <i2> comp (<i3> p @ (i2 \/ -i3)) (w.2 @ i1)
- [ (i1 = 0) ->
- <i3> comp (<i4> p @ ((i2 /\ i4) \/ (-i3 /\ i4))) (w.1)
- [ (i2 = 0)(i3 = 1) -> <i4> w.1 ]
- , (i1 = 1) ->
- <i3> comp (<i4> p @ (i2 \/ -i3 \/ -i4)) y
- [ (i2 = 1) -> <i4> y, (i3 = 0) -> <i4> y ]
- , (i2 = 1) -> <i3> w.2 @ i1 ]
- , (i1 = 0) ->
- <i2> comp (<i3> p @ (i2 /\ i3))
- (comp (<i1> p @ -i1) (w.2 @ -i0)
- [ (i0 = 0) ->
- <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]
- , (i0 = 1) ->
- <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)
- [ (i1 = 1) -> <i2> w.1 ]
- ])
- [ (i2 = 0) ->
- <i3> comp (<i1> p @ -i1) (w.2 @ -i0)
- [ (i0 = 0) ->
- <i1> comp (<i2> p @ (-i1 \/ -i2)) y
- [ (i1 = 0) -> <i2> y ]
- , (i0 = 1) ->
- <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)
- [ (i1 = 1) -> <i2> w.1 ]
- ]
- ]
- , (i1 = 1) -> <i2> comp (<i3> p @ (i2 \/ -i3)) y [ (i2 = 1) -> <i3> y ] ]
- )
-
-transIsEquiv (A B : U) (p : Id U A B) : isEquiv A B (trans A B p) =
- (transCenter A B p,transIsCenter A B p)
-
-transEquiv (A B : U) (p : Id U A B) : equiv A B =
- (trans A B p,transIsEquiv A B p)
-
-transDelta (A : U) : equiv A A = transEquiv A A (<_> A)
-
-transEquivToId (A B : U) (w : equiv A B) : Id U A B =
- <i> glue B [ (i=1) -> (B,transDelta B), (i=0) -> (A,w) ]
-
-eqToEq (A B : U) (p : Id U A B)
- : Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p
- = <j i> glue B
- [ (i=0) -> (A,transEquiv A B p)
- , (i=1) -> (B,transEquiv B B (<_> B))
- , (j=1) -> (p@i,transEquiv (p@i) B (<k> p @ (i \/ k)))]
-
-eqToEq' (A : U) : (B : U) (p : Id U A B)
- -> Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p
- = J U A
- (\ (B : U) (p : Id U A B) ->
- Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p)
- (<j i> glue A
- [ (i=0) -> (A,transDelta A)
- , (i=1) -> (A,transDelta A)
- , (j=1) -> (A,transDelta A)])
-
-transIdFun (A B : U) (w : equiv A B)
- : Id (A -> B) (trans A B (transEquivToId A B w)) w.1 =
- <i> \(a : A) -> let b : B = w.1 a
- in addf (f (f (f b))) b (addf (f (f b)) b (addf (f b) b (trf b))) @ i
- where f (b : B) : B = comp (<_> B) b []
- trf (b : B) : Id B (f b) b =
- <i> fill (<_> B) b [] @ -i
- addf (b b' : B) : Id B b b' -> Id B (f b) b' =
- compId B (f b) b b' (trf b)
-
-
-propIsEquiv (A B : U) (f : A -> B)
- : prop (isEquiv A B f) = lemProp (isEquiv A B f) lem
- where
- isEqf : U = isEquiv A B f
- fibf : (y : B) -> U = fiber A B f
- center : U = (y : B) -> fibf y
- isCenter (s : center) : U = (y : B) (w : fibf y) -> Id (fibf y) (s y) w
- lem (fe : isEqf) : prop isEqf = propSig center isCenter pc pisc
- where
- fibprop (y : B) (u v : fibf y) : Id (fibf y) u v =
- compId (fibf y) u (fe.1 y) v (<i> fe.2 y u @ -i) (fe.2 y v)
- pc : prop center = propPi B fibf fibprop
- pisc (s : center) (g h : isCenter s) : Id (isCenter s) g h =
- <i> \ (y : B) (w : fibf y) ->
- propSet (fibf y) (fibprop y) (s y) w (g y w) (h y w) @ i
-
-idToId (A B : U) (w : equiv A B)
- : Id (equiv A B) (transEquiv A B (transEquivToId A B w)) w
- = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)
- (transEquiv A B (transEquivToId A B w)) w
- (transIdFun A B w)
-
-univAx (A B : U) : isEquiv (Id U A B) (equiv A B) (transEquiv A B) =
- gradLemma (Id U A B) (equiv A B) (transEquiv A B) (transEquivToId A B)
- (idToId A B) (eqToEq A B)
-
-
--- Any equality defines an equivalence
-idToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B =
- J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A)
-
-equivId
- (A B : U)
- (f : A -> B)
- (s : (y : B) -> fiber A B f y)
- (t : (y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w)
- : Id U A B =
- <i> glue B
- [ (i=1) -> (B,idEquiv B)
- , (i=0) -> (A,f,s,t)]
-
-equivToId (A B : U) (w : equiv A B) : Id U A B =
- <i> glue B [ (i=1) -> (B,idEquiv B), (i=0) -> (A,w) ]
-
-
-foo (A B : U) (w : equiv A B) (a : A) : B = (idToEquiv A B (equivToId A B w)).1 a
-
-testfun (A B : U) (w : equiv A B)
- : Id (A -> B) (idToEquiv A B (equivToId A B w)).1 w.1 =
- <i> \(a : A) -> let b : B = w.1 (fill (<_> A) a [] @ -i)
- in (addf (f (f b)) b (addf (f b) b (trf b))) @ i
- where p : A -> B = (idToEquiv A B (equivToId A B w)).1
- f (b : B) : B = comp (<_> B) b []
- trf (b : B) : Id B (f b) b =
- <i> fill (<_> B) b [] @ -i
- addf (b b' : B) : Id B b b' -> Id B (f b) b' =
- compId B (f b) b b' (trf b)
-
-test (A B : U) (w : equiv A B) : Id (equiv A B) (idToEquiv A B (equivToId A B w)) w =
- lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)
- (idToEquiv A B (equivToId A B w)) w
- (testfun A B w)
-
-test2 (A : U) : Id (equiv A A) (idToEquiv A A (equivToId A A (idEquiv A))) (idEquiv A) =
- test A A (idEquiv A)
-
-{-
-equivToId (A B : U) (w : equiv A B) : Id U A B =
- <i> glue B [ (i=1) -> (B,idEquiv B), (i=0) -> (A,w) ]
- --equivId A B w.1 w.2.1 w.2.2
-
-test (A : U) : Id U A A = (equivToId A A (idToEquiv A A (refl U A)))
-
-test2 (A : U) (a : A) : A = comp (test A) a []
-
-want (A : U) : Id (Id U A A) (test A) (equivToId A A (idEquiv A)) = undefined
-
-test3 (A : U) (a : A) : A = comp (equivToId A A (idEquiv A)) a []
-
-test4 (A B : U) (w : equiv A B) (a : A) : B = comp (equivToId A B w) a []
-
-test4nf (A B : U) (w : equiv A B) (a : A) : B =
- comp (<i0> B) (comp (<i0> B) (comp (<i0> B) (w.1 a) [ ]) [ ]) [ ]
-
-
-ormaybe (A A : U) : Id (equiv A A) (idEquiv A) (idToEquiv A A (refl U A)) =
- undefined
-
--- eqToEq (A : U)
--- : (B : U) (p : Id U A B) ->
--- Id (Id U A B) (equivToId A B (idToEquiv A B p)) p =
--- J U A
--- (\ (B : U) (p : Id U A B) ->
--- Id (Id U A B) (equivToId A B (idToEquiv A B p)) p)
--- ?
--- -- (<j i> glue A
--- -- [ (i=0) -> (A,idFun A,idCenter A,idIsCenter A)
--- -- , (i=1) -> (A,idFun A,idCenter A,idIsCenter A)
--- -- , (j=1) -> (A,idFun A,idCenter A,idIsCenter A)])
-
-
-
--}
\ No newline at end of file
module univalence where
-import retract
-import equiv
+import gradLemma
--- we do something simpler than univalence
+transEquivToId (A B : U) (w : equiv A B) : Id U A B =
+ <i> glue B [ (i=1) -> (B,transDelta B), (i=0) -> (A,w) ]
-transpIsEquiv (A B:U) (p:Id U A B) : isEquiv A B (\ (x:A) -> transport p x) =
- transport (<i>isEquiv A (p@i) (\ (x:A) -> transport (<j>p@i/\j) x)) (idIsEquiv A)
+eqToEq (A B : U) (p : Id U A B)
+ : Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p
+ = <j i> glue B
+ [ (i=0) -> (A,transEquiv A B p)
+ , (i=1) -> (B,transDelta B)
+ , (j=1) -> (p@i,transEquiv (p@i) B (<k> p @ (i \/ k)))]
-IdToEquiv (A B:U) (p: Id U A B) : Equiv A B = (\ (x:A) -> transport p x, transpIsEquiv A B p)
+-- The normal form of this is much bigger than the normal form of eqToEq
+eqToEq' (A : U) : (B : U) (p : Id U A B)
+ -> Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p
+ = J U A
+ (\ (B : U) (p : Id U A B) ->
+ Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p)
+ (<j i> glue A
+ [ (i=0) -> (A,transDelta A)
+ , (i=1) -> (A,transDelta A)
+ , (j=1) -> (A,transDelta A)])
-EquivToId (A B:U) (z:Equiv A B) : Id U A B = isEquivEq A B z.1 z.2
+transIdFun (A B : U) (w : equiv A B)
+ : Id (A -> B) (trans A B (transEquivToId A B w)) w.1 =
+ <i> \(a : A) -> let b : B = w.1 a
+ in addf (f (f (f b))) b (addf (f (f b)) b (addf (f b) b (trf b))) @ i
+ where f (b : B) : B = comp (<_> B) b []
+ trf (b : B) : Id B (f b) b =
+ <i> fill (<_> B) b [] @ -i
+ addf (b b' : B) : Id B b b' -> Id B (f b) b' =
+ compId B (f b) b b' (trf b)
-secIdEquiv (A B :U) (p : Id U A B) : Id (Id U A B) (EquivToId A B (IdToEquiv A B p)) p =
- transport (<i>Id (Id U A (p@i)) (EquivToId A (p@i) (IdToEquiv A (p@i) (<j>p@i/\j))) (<j>p@i/\j))
- (<i>isoIdRef A@-i)
+idToId (A B : U) (w : equiv A B)
+ : Id (equiv A B) (transEquiv A B (transEquivToId A B w)) w
+ = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)
+ (transEquiv A B (transEquivToId A B w)) w
+ (transIdFun A B w)
+
+univAx (A B : U) : isEquiv (Id U A B) (equiv A B) (transEquiv A B) =
+ gradLemma (Id U A B) (equiv A B) (transEquiv A B) (transEquivToId A B)
+ (idToId A B) (eqToEq A B)
+
+
+-- Alternative definition:
+
+-- Any equality defines an equivalence
+idToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B =
+ J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A)
+
+equivId (A B : U) (f : A -> B) (s : (y : B) -> fiber A B f y)
+ (t : (y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w)
+ : Id U A B = <i> glue B [ (i = 1) -> (B,idEquiv B), (i = 0) -> (A,f,s,t)]
+
+equivToId (A B : U) (w : equiv A B) : Id U A B =
+ <i> glue B [ (i = 1) -> (B,idEquiv B), (i = 0) -> (A,w) ]
+
+idToEquivIdFun (A B : U) (w : equiv A B)
+ : Id (A -> B) (idToEquiv A B (equivToId A B w)).1 w.1 =
+ <i> \(a : A) -> let b : B = w.1 (fill (<_> A) a [] @ -i)
+ in (addf (f (f b)) b (addf (f b) b (trf b))) @ i
+ where p : A -> B = (idToEquiv A B (equivToId A B w)).1
+ f (b : B) : B = comp (<_> B) b []
+ trf (b : B) : Id B (f b) b =
+ <i> fill (<_> B) b [] @ -i
+ addf (b b' : B) : Id B b b' -> Id B (f b) b' =
+ compId B (f b) b b' (trf b)
+
+idToEquivK (A B : U) (w : equiv A B) : Id (equiv A B) (idToEquiv A B (equivToId A B w)) w =
+ lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)
+ (idToEquiv A B (equivToId A B w)) w (idToEquivIdFun A B w)
+
+-- This takes too long to normalize:
+test (A : U) : Id (equiv A A) (idToEquiv A A (equivToId A A (idEquiv A))) (idEquiv A) =
+ idToEquivK A A (idEquiv A)
+
+
+
+
+
+
+
+-- Old code:
+-- -- we do something simpler than univalence
+
+-- transpIsEquiv (A B:U) (p:Id U A B) : isEquiv A B (\ (x:A) -> transport p x) =
+-- transport (<i>isEquiv A (p@i) (\ (x:A) -> transport (<j>p@i/\j) x)) (idIsEquiv A)
+
+-- IdToEquiv (A B:U) (p: Id U A B) : Equiv A B = (\ (x:A) -> transport p x, transpIsEquiv A B p)
+
+-- EquivToId (A B:U) (z:Equiv A B) : Id U A B = isEquivEq A B z.1 z.2
+
+-- secIdEquiv (A B :U) (p : Id U A B) : Id (Id U A B) (EquivToId A B (IdToEquiv A B p)) p =
+-- transport (<i>Id (Id U A (p@i)) (EquivToId A (p@i) (IdToEquiv A (p@i) (<j>p@i/\j))) (<j>p@i/\j))
+-- (<i>isoIdRef A@-i)
projects / cubicaltt.git / commitdiff