result on equivalence of fibers

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 321efab30c729487f352718b1bf574c5736e354d..4beebb5265d4211d6b799e2346a159529639b601 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -45,3 +45,24 @@ Equiv (A B : U) : U = (f : A -> B) * isEquiv A B f
 \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>(rem3 @ 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