Fix uafunext2

diff --git a/examples/uafunext2.ctt b/examples/uafunext2.ctt
index 0ae4e8217603347177b7ee18c58cbeb57fa02977..a92fe5a0c7b191c46caecbd0c28e4b0a1092bb4c 100644 (file)
--- a/examples/uafunext2.ctt
+++ b/examples/uafunext2.ctt
@@ -3,51 +3,51 @@ module uafunext2 where
 import retract\r
 import equiv\r
 \r
-lem1 (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : Id U ((x:A)*P x) A = isoId T A f g t s\r
+lem1 (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : Id U ((x:A)*P x) A = isoId T A f g t s\r
  where\r
    T : U = (x:A) * P x\r
    f (z:T) : A = z.1\r
-   g (x:A) : T = (x,(cA x).1)\r
-   s (z:T) : Id T (g (f z)) z = <i>(z.1,((cA z.1).2 (cA z.1).1 z.2)@ i)\r
+   g (x:A) : T = (x,(cA x).2)\r
+   s (z:T) : Id T (g (f z)) z = <i>(z.1,((cA z.1).1 (cA z.1).2 z.2)@ i)\r
    t (x:A) : Id A (f (g x)) x = refl A x\r
 \r
-lem2 (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : Id U (A -> (x:A)*P x) (A->A) = \r
+lem2 (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : Id U (A -> (x:A)*P x) (A->A) =\r
  <i> A -> (lem1 A P cA)@ i\r
 \r
-alpha (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (u:A -> (x:A)*P x) : A -> A =\r
+alpha (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) (u:A -> (x:A)*P x) : A -> A =\r
  transport (lem2 A P cA) u\r
 \r
-test (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (u : A -> (x:A)*P x) (x:A) :\r
+test (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) (u : A -> (x:A)*P x) (x:A) :\r
  Id A (alpha A P cA u x) (u x).1 = refl A (u x).1\r
 \r
-\r
 lemTransFib (A:U) : (B:U) (E:Id U A B) (b:B) -> prop (fiber A B (\ (x:A) -> transport E x) b) =\r
  J U A (\ (B:U) (E:Id U A B) -> (b:B) -> prop (fiber A B (\ (x:A) -> transport E x) b)) (lemIdFib A)\r
-        \r
-fibId (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : U = fiber (A -> (x:A)*P x) (A -> A) (alpha A P cA) (idfun A)\r
 \r
-corr1 (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : prop (fibId A P cA) = \r
+fibId (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : U = fiber (A -> (x:A)*P x) (A -> A) (alpha A P cA) (idfun A)\r
+\r
+corr1 (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : prop (fibId A P cA) =\r
  lemTransFib (A -> (x:A)*P x) (A -> A) (lem2 A P cA) (idfun A)\r
 \r
-phi (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (f:(x:A) -> P x) : fibId A P cA =\r
+phi (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) (f:(x:A) -> P x) : fibId A P cA =\r
  (\ (x:A) -> (x,f x),refl (A->A) (idfun A))\r
- \r
-psi (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (up : fibId A P cA) (x:A) : P x = \r
+\r
+psi (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) (up : fibId A P cA) (x:A) : P x =\r
  subst (A -> A) (\ (g:A->A) -> P (g x)) (alpha A P cA u) (idfun A) (<i>p@-i) (u x).2\r
  where u : A -> (y:A) * P y = up.1\r
        p : Id (A -> A) (idfun A) (alpha A P cA u) = up.2\r
 \r
-retPhiPsi (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) (f : (x:A) -> P x) :\r
+retPhiPsi (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) (f : (x:A) -> P x) :\r
  Id ((x:A) -> P x) (psi A P cA (phi A P cA f)) f = refl ((x:A) -> P x) f\r
 \r
-thm (A:U) (P:A-> U) (cA:(x:A) -> contr (P x)) : prop ((x:A) -> P x) =\r
+thm (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : prop ((x:A) -> P x) =\r
  retractProp ((x:A) -> P x) (fibId A P cA) (phi A P cA) (psi A P cA) (retPhiPsi A P cA) (corr1 A P cA)\r
 \r
 sumF  (A B:U) (f:A -> B) : U = (g:A->B) * (x:A) -> Id B (f x) (g x)\r
 prodF (A B:U) (f:A -> B) : U = (x:A) -> (y:B) * Id B (f x) y\r
 \r
-lemProdF (A B:U) (f:A -> B) : prop (prodF A B f) = \r
- thm A (\ (x:A) -> (y:B) * Id B (f x) y) (\ (x:A) -> ((f x,refl B (f x)),lemIdFib B (f x)))\r
+lemProdF (A B:U) (f:A -> B) : prop (prodF A B f) = thm A P cA\r
+ where P (x:A) : U =  (y:B) * Id B (f x) y\r
+       cA (x:A) : isContr (P x) = (lemIdFib B (f x),(f x,refl B (f x)))\r
 \r
 sumToProd (A B:U) (f:A -> B) (gp : sumF A B f) : prodF A B f = \ (x:A) -> (gp.1 x,gp.2 x)\r
 prodToSum (A B:U) (f:A -> B) (h : prodF A B f) : sumF A B f = (\ (x:A) -> (h x).1,\ (x:A) -> (h x).2)\r
@@ -60,6 +60,3 @@ corr2 (A B:U) (f:A->B) : prop (sumF A B f) =
 \r
 funext (A B:U) (f g:A -> B) (h:(x:A) -> Id B (f x) (g x)) : Id (A->B) f g = <i> \ (x:A) -> (rem@i).1 x\r
  where rem : Id (sumF A B f) (f,\ (x:A) -> refl B (f x)) (g,h) = corr2 A B f (f,\ (x:A) -> refl B (f x)) (g,h)\r
-\r
-\r
-\r