--- /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
+
+-- 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)
+
+
+
+-- 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
projects / cubicaltt.git / commitdiff