define equivalence using Id and prove univalence with Id everywhere

diff --git a/examples/idtypes.ctt b/examples/idtypes.ctt
index b82050b6cc52616a95c5d93797352244823fff44..d0705ddf549acb664a1acb8ec546e74020ca83db 100644 (file)
--- a/examples/idtypes.ctt
+++ b/examples/idtypes.ctt
@@ -1,5 +1,6 @@
 module idtypes where
 
+import sigma
 import univalence
 
 refId (A : U) (a : A) : Id A a a =
@@ -70,7 +71,7 @@ PathIdPath (A B : U) : Path U (Id U A B) (Path U A B) =
             (\(p : Id U A B) -> <i> idToPathToId U A B p @ - i)
 
 -- A few different versions of univalence for Id:
-IdUnivalence1 (A B : U) : Path U (Id U A B) (equiv A B) = 
+IdUnivalence1 (A B : U) : Path U (Id U A B) (equiv A B) =
   compPath U (Id U A B) (Path U A B) (equiv A B) (PathIdPath A B) (corrUniv A B)
 
 IdUnivalence2 (A B : U) : equiv (Id U A B) (equiv A B) =
@@ -79,7 +80,97 @@ IdUnivalence2 (A B : U) : equiv (Id U A B) (equiv A B) =
 IdUnivalence3 (A B : U) : Id U (Id U A B) (equiv A B) =
   pathToId U (Id U A B) (equiv A B) (IdUnivalence1 A B)
 
--- TODO: redefine equiv using Id?
+
+-- Redefine equivalence using Id and prove univalence with this formulation
+
+fiberId (A B : U) (f : A -> B) (y : B) : U =
+  (x : A) * Id B y (f x)
+
+isContrId (A : U) : U = (x : A) * ((y : A) -> Id A x y)
+
+isEquivId (A B : U) (f : A -> B) : U = (y : B) -> isContrId (fiberId A B f y)
+
+equivId (A B : U) : U = (f : A -> B) * isEquivId A B f
+
+fiberToFiberId (A B : U) (f : A -> B) (y : B) :
+  Path U (fiber A B f y) (fiberId A B f y) =
+    isoPath (fiber A B f y) (fiberId A B f y) f1 f2 rem1 rem2
+  where
+  f1 (t : fiber A B f y) : fiberId A B f y = (t.1,pathToId B y (f t.1) t.2)
+  f2 (t : fiberId A B f y) : fiber A B f y = (t.1,idToPath B y (f t.1) t.2)
+  rem1 (x : fiberId A B f y) : Path (fiberId A B f y) (f1 (f2 x)) x =
+    <i> (x.1,idToPathToId B y (f x.1) x.2 @ -i)
+  rem2 (x : fiber A B f y) : Path (fiber A B f y) (f2 (f1 x)) x =
+      <i> (x.1,pathToIdToPath B y (f x.1) x.2 @ -i)
+
+isContrToIsContrId (A : U) (p : isContr A) : isContrId A =
+  (p.1,\(y : A) -> pathToId A p.1 y (p.2 y))
+
+equivToEquivId (A B : U) (e : equiv A B) : equivId A B = (f,rem)
+  where
+  f : A -> B = e.1
+  rem (y : B) : isContrId (fiberId A B f y) =
+    transport (<i> isContrId (fiberToFiberId A B f y @ i))
+              (isContrToIsContrId (fiber A B f y) (e.2 y))
+
+isContrToIsContrIdU (A : U) : Path U (isContr A) (isContrId A) =
+   isoPath (isContr A) (isContrId A) f1 f2 rem1 rem2
+  where
+  f1 : isContr A -> isContrId A = isContrToIsContrId A
+  f2 (p : isContrId A) : isContr A = (p.1,\(y : A) -> idToPath A p.1 y (p.2 y))
+
+  rem1 (x : isContrId A) : Path (isContrId A) (f1 (f2 x)) x =
+    <i> (x.1,\(y : A) -> idToPathToId A x.1 y (x.2 y) @ - i)
+  rem2 (x : isContr A) : Path (isContr A) (f2 (f1 x)) x =
+    <i> (x.1,\(y : A) -> pathToIdToPath A x.1 y (x.2 y) @ - i)
+
+isContrFiberToIsContrFiberId (A B : U) (f : A -> B) (y : B) :
+  Path U (isContr (fiber A B f y)) (isContrId (fiberId A B f y)) = goal
+  where
+  rem1 : Path U (isContr (fiber A B f y)) (isContr (fiberId A B f y)) =
+    <i> isContr (fiberToFiberId A B f y @ i)
+  rem2 : Path U (isContr (fiberId A B f y)) (isContrId (fiberId A B f y)) =
+    isContrToIsContrIdU (fiberId A B f y)
+  goal : Path U (isContr (fiber A B f y)) (isContrId (fiberId A B f y)) =
+    compPath U (isContr (fiber A B f y)) (isContr (fiberId A B f y))
+               (isContrId (fiberId A B f y)) rem1 rem2
+
+opaque isContrFiberToIsContrFiberId
+
+equivEquivIdU (A B : U) : Path U (equiv A B) (equivId A B) =
+  isoPath (equiv A B) (equivId A B) f1 f2 rem1 rem2
+  where
+  f1 (p : equiv A B) : equivId A B =
+    (p.1,\(y : B) -> trans (isContr (fiber A B p.1 y))
+                           (isContrId (fiberId A B p.1 y))
+                           (isContrFiberToIsContrFiberId A B p.1 y) (p.2 y))
+  f2 (p : equivId A B) : equiv A B =
+    (p.1,\(y : B) -> transNeg (isContr (fiber A B p.1 y))
+                              (isContrId (fiberId A B p.1 y))
+                              (isContrFiberToIsContrFiberId A B p.1 y) (p.2 y))
+
+  rem1 (x : equivId A B) : Path (equivId A B) (f1 (f2 x)) x =
+    <i> (x.1,\(y : B) -> transK (isContr (fiber A B x.1 y))
+                                (isContrId (fiberId A B x.1 y))
+                                (isContrFiberToIsContrFiberId A B x.1 y) (x.2 y) @ -i)
+
+  rem2 (x : equiv A B) : Path (equiv A B) (f2 (f1 x)) x =
+    <i> (x.1,\(y : B) -> transNegK (isContr (fiber A B x.1 y))
+                                   (isContrId (fiberId A B x.1 y))
+                                   (isContrFiberToIsContrFiberId A B x.1 y) (x.2 y) @ -i)
+
+transparent isContrFiberToIsContrFiberId
+
+-- Univalence expressed using Id everywhere:
+univalenceId (A B : U) : equivId (Id U A B) (equivId A B) =
+  equivToEquivId (Id U A B) (equivId A B) rem1
+  where
+  rem : Path U (Id U A B) (equivId A B) =
+    compPath U (Id U A B) (equiv A B) (equivId A B)
+             (IdUnivalence1 A B) (equivEquivIdU A B)
+  rem1 : equiv (Id U A B) (equivId A B) =
+    transEquiv' (equivId A B) (Id U A B) rem
+
 
 --------------------------------------------------------------------------------
 -- Some tests

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index f9b0b312342c6ba048dbb5cb7184f914702fb571..ce9a07bb00cc8efbe2c0e8da98f9bb8e0c196ce4 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -17,6 +17,27 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
 
 -- Transport can be defined using comp
 trans (A B : U) (p : Path U A B) (a : A) : B = comp p a []
+transNeg (A B : U) (p : Path U A B) (b : B) : A = comp (<i> p @ - i) b []
+
+transK (A B : U) (p : Path U A B) (y : B) :
+  Path B y (trans A B p (transNeg A B p y)) =
+    <i> comp p (transNeg A B p y) [(i=0) -> rem1
+                                  ,(i=1) -> rem2 (transNeg A B p y)]
+    where
+    rem1 : PathP p (transNeg A B p y) y =
+      <i> comp (<j> p @ (i\/-j)) y [(i=1) -> <j>y]
+    rem2 (x:A) : PathP p x (trans A B p x) =
+      <i> comp (<j> p @ (i/\j)) x [(i=0) -> <j> x]
+
+transNegK (A B : U) (p : Path U A B) (a : A) :
+  Path A a (transNeg A B p (trans A B p a)) =
+    <i> comp (<j> p @ -j) (trans A B p a) [(i=0) -> rem1
+                                         ,(i=1) -> rem2 (trans A B p a) ]
+    where
+    rem1 : PathP (<i> p@-i) (trans A B p a) a = 
+       <i> comp (<j> p @ (-i /\ j)) a [(i=1) -> <j>a]
+    rem2 (b:B) : PathP (<i> p@-i) b (transNeg A B p b) = 
+      <i> comp (<j> p @ (-i \/ -j)) b [(i=0) -> <j> b]
 
 -- subst can be defined using trans:
 substTrans (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b =