--- /dev/null
+module testContr where
+
+import prelude
+
+retIsContr (A B :U) (f:A->B) (g:B->A) (h : (x:A) -> Id A (g (f x)) x) (v:isContr B)
+ : isContr A = (g b,p)
+ where
+ b : B = v.1
+ q : (y:B) -> Id B b y = v.2
+ p (x:A) : Id A (g b) x = <i>comp (<j>A) (g (q (f x)@i)) [(i=0) -> <j>g b,(i=1) -> h x]
+
+sigIsContr (A:U) (B:A->U) (u:isContr A) (q:(x:A) -> isContr (B x))
+ : isContr ((x:A)*B x) = ((a,g a),r)
+ where
+ a : A = u.1
+ p : (x:A) -> Id A a x = u.2
+ g (x:A) : B x = (q x).1
+ h (x:A) : (y:B x) -> Id (B x) (g x) y = (q x).2
+ C : U = (x:A) * B x
+ r (z:C) : Id C (a,g a) z =
+ <i>(p z.1@i,h (p z.1@i) (comp (<j>B (p z.1@i\/-j)) z.2 [(i=1)-><j>z.2])@i)
+
+isPathContr (A:U) (cA:isContr A) (x y:A) : isContr (Id A x y) = (p0,q)
+ where
+ a : A = cA.1
+ f : (x:A) -> Id A a x = cA.2
+ p0 : Id A x y = <i>comp (<j>A) a [(i=0) -> f x,(i=1) -> f y]
+ q (p:Id A x y) : Id (Id A x y) p0 p =
+ <j i>comp (<k>A) a [(i=0) -> f x,(i=1) -> f y,
+ (j=0) -> <k>comp (<l>A) a [(k=0) -> <l>a,(i=0) -> <l>f x@k/\l,(i=1) -> <l>f y@k/\l],
+ (j=1) -> f (p@i)]
+
+fiber (A B : U) (f : A -> B) (y : B) : U =
+ (x : A) * Id B y (f x)
+
+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
+
+isEquivContr (A B:U) (cA:isContr A) (cB:isContr B) (f:A->B) : isEquiv A B f =
+ \ (y:B) -> sigIsContr A (\ (x:A) -> Id B y (f x)) cA (\ (x:A) -> isPathContr B cB y (f x))
+
+sig (A:U) (B:A->U) : U = (x:A) * B x
+
+totalFun (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (w:sig A B) : sig A C =
+ (w.1,f (w.1) (w.2))
+
+funFib1 (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) :
+ fiber (sig A B) (sig A C) (totalFun A B C f) (x0,z0) = ((x0,u.1),<i>(x0,u.2@i))
+
+funFib2 (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0)
+ (w : fiber (sig A B) (sig A C) (totalFun A B C f) (x0,z0)) : fiber (B x0) (C x0) (f x0) z0 = (b0,s)
+ where
+ x : A = w.1.1
+ b : B x = w.1.2
+ p : Id A x0 x = <i>(w.2@i).1
+ q : IdP (<i>C (p@i)) z0 (f x b) = <i>(w.2@i).2
+ b0 : B x0 = comp (<i>B (p@-i)) b []
+ r : IdP (<i>B (p@-i)) b b0 = <i>comp (<j>B (p@-j\/-i)) b [(i=0) -> <k>b]
+ s : Id (C x0) z0 (f x0 b0) = <i>comp (<j>C (p@(i/\-j))) (q@i) [(i=0) -> <k>z0,(i=1) -> <k>f (p@-k) (r@k)]
+
+compFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) :
+ fiber (B x0) (C x0) (f x0) z0 = funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u)
+
+retFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) :
+ Id (fiber (B x0) (C x0) (f x0) z0) (funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u)) u =
+ <l> (comp (<i> B x0) u.1 [(l=1) -> <j>u.1],
+ <i> comp (<j> C x0) (u.2 @ i) [ (l=1) -> <j> u.2 @ i,
+ (i = 0) -> <j> z0,
+ (i = 1) -> <j> f x0 (comp (<k> B x0) u.1 [ (j = 0) -> <k> u.1, (l=1) -> <k>u.1 ]) ])
+
+equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B)) (cC : isContr (sig A C)) (x:A)
+ : isEquiv (B x) (C x) (f x) =
+ \ (z:C x) -> retIsContr (fiber (B x) (C x) (f x) z) (fiber (sig A B) (sig A C) (totalFun A B C f) (x,z))
+ (funFib1 A B C f x z)
+ (funFib2 A B C f x z)
+ (retFunFib A B C f x z)
+ (isEquivContr (sig A B) (sig A C) cB cC (totalFun A B C f) (x,z))
+
+
+lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A a x) =
+ ((a,refl A a),\ (z:(x:A) * Id A a x) -> contrSingl A a z.1 z.2)
+
+idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A)
+
+lem1 (B:U) : isContr ((X:U) * equiv X B) =
+ ((B,idEquiv B)
+ ,\(w : (X : U) * equiv X B)
+ -> <i> let glueB : U = glue B [(i=0) -> (B,idEquiv B), (i=1) -> w]
+ unglueElemB : glueB -> B
+ = \(g : glueB)
+ -> unglueElem g [(i=0) -> (B,idEquiv B)
+ ,(i=1) -> w]
+ in (glueB
+ ,unglueElemB
+ ,\(b : B)
+ -> let center : fiber glueB B unglueElemB b
+ = (glueElem (comp (<_> B) b [(i=0) -> <_> b
+ ,(i=1) -> (w.2.2 b).1.2])
+ [(i=0) -> b
+ ,(i=1) -> (w.2.2 b).1.1]
+ ,fill (<_> B) b [(i=0) -> <_> b
+ ,(i=1) -> (w.2.2 b).1.2])
+ contr (v : fiber glueB B unglueElemB b)
+ : Id (fiber glueB B unglueElemB b) center v
+ = <j> (glueElem (comp (<_> B) b [(i=0) -> <k> v.2 @ (j /\ k)
+ ,(i=1) -> ((w.2.2 b).2 v @ j).2
+ ,(j=0) -> fill (<_> B) b [(i=0) -> <_> b
+ ,(i=1) -> (w.2.2 b).1.2]
+ ,(j=1) -> v.2])
+ [(i=0) -> v.2 @ j
+ ,(i=1) -> ((w.2.2 b).2 v @ j).1]
+ ,fill (<_> B) b [(i=0) -> <l> v.2 @ (j /\ l)
+ ,(i=1) -> ((w.2.2 b).2 v @ j).2
+ ,(j=0) -> fill (<_> B) b [(i=0) -> <_> b
+ ,(i=1) -> (w.2.2 b).1.2]
+ ,(j=1) -> v.2])
+ in (center,contr)))
+
+contrSingl (A : U) (a b : A) (p : Id A a b) :
+ Id ((x:A) * Id A x b) (b,refl A b) (a,p) = <i> (p @ -i,<j> p @ -i\/j)
+
+lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A x a) =
+ ((a,refl A a),\ (z:(x:A) * Id A x a) -> contrSingl A z.1 a z.2)
+
+thmUniv (t : (A X:U) -> Id U X A -> equiv X A) (A:U) : (X:U) -> isEquiv (Id U X A) (equiv X A) (t A X) =
+ equivFunFib U (\ (X:U) -> Id U X A) (\ (X:U) -> equiv X A) (t A) (lemSinglContr U A) (lem1 A)
+
+-- thmUniv (lem1 : (A:U) -> isContr ((X:U) * equiv A X)) (t : (A X:U) -> Id U A X -> equiv A X) (A:U)
+-- : (X:U) -> isEquiv (Id U A X) (equiv A X) (t A X) =
+-- equivFunFib U (\ (X:U) -> Id U A X) (equiv A) (t A) (lemSinglContr U A) (lem1 A)
projects / cubicaltt.git / commitdiff