From 84b57eb06f65b4d02d05858d0a81202135acbb21 Mon Sep 17 00:00:00 2001
From: Simon Huber <hubsim@gmail.com>
Date: Fri, 11 Sep 2015 22:18:54 +0200
Subject: [PATCH] Another formulation of univalence

---
 examples/equiv.ctt      |  4 ++++
 examples/univalence.ctt | 43 +++++++++++++++++++++++++++++++++++++----
 2 files changed, 43 insertions(+), 4 deletions(-)

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index e3edaed..3e5d933 100644
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -27,6 +27,10 @@ propIsEquiv (A B : U) (f : A -> B)
           <i> \ (y : B) (w : fibf y) ->
                  propSet (fibf y) (fibprop y) (s y) w (g y w) (h y w) @ i
 
+equivLemma (A B : U)
+  : (v w : equiv A B) -> Id (A -> B) v.1 w.1 -> Id (equiv A B) v w
+  = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)
+
 
 -- The identity function is an equivalence
 idCenter (A : U) (y : A) : fiber A A (idfun A) y = (y, refl A y)
diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 73ead54..ac236fa 100644
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -30,13 +30,16 @@ transIdFun (A B : U) (w : equiv A B)
 
 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
+  = equivLemma A B (transEquiv A B (transEquivToId A B w)) w
       (transIdFun A B w)
 
+transEquivIsEquiv (A B : U)
+  : isEquiv (Id U A B) (equiv A B) (transEquiv A B)
+  = gradLemma (Id U A B) (equiv A B) (transEquiv A B)
+      (transEquivToId A B) (idToId A B) (eqToEq A B)
+
 univalence (A B : U) : equiv (Id U A B) (equiv A B) =
-  (transEquiv A B,gradLemma (Id U A B) (equiv A B) (transEquiv A B)
-                            (transEquivToId A B) (idToId A B) (eqToEq A B))
+  (transEquiv A B,transEquivIsEquiv A B)
 
 univalence1 (A B:U) : Id U (Id U A B) (equiv A B) = 
  isoId (Id U A B) (equiv A B) (transEquiv A B) (transEquivToId A B) (idToId A B) (eqToEq A B)
@@ -47,3 +50,35 @@ test (A : U) : Id (equiv A A) (transEquiv A A (transEquivToId A A (idEquiv A)))
   idToId A A (idEquiv A)
 
 
+-- The canonical map defined using J
+canIdToEquiv (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)
+
+canDiagTrans (A : U) : Id (A -> A) (canIdToEquiv A A (<_> A)).1 (idfun A) =
+  <i> fill (<_> A -> A) (idfun A) [] @ -i
+
+transDiagTrans (A : U) : Id (A -> A) (idfun A) (trans A A (<_> A)) =
+  <i> \ (a : A) -> fill (<_> A) a [] @ i
+
+canIdToEquivLem (A : U) : (B : U) (p : Id U A B) ->
+  Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1
+  = J U A
+      (\ (B : U) (p : Id U A B) ->
+        Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1)
+      (compId (A -> A)
+        (canIdToEquiv A A (<_> A)).1 (idfun A) (trans A A (<_> A))
+        (canDiagTrans A) (transDiagTrans A))
+
+canIdToEquivIsTransEquiv (A B : U) :
+  Id (Id U A B -> equiv A B) (canIdToEquiv A B) (transEquiv A B) =
+  <i> \ (p : Id U A B) ->
+        equivLemma A B (canIdToEquiv A B p) (transEquiv A B p)
+          (canIdToEquivLem A B p) @ i
+
+-- The canonical map is an equivalence
+univalence2 (A B : U) : isEquiv (Id U A B) (equiv A B) (canIdToEquiv A B) =
+  substInv (Id U A B -> equiv A B)
+    (isEquiv (Id U A B) (equiv A B))
+     (canIdToEquiv A B) (transEquiv A B)
+     (canIdToEquivIsTransEquiv A B)
+     (transEquivIsEquiv A B)
\ No newline at end of file
-- 
2.34.1