From f66d180ec301cbe1313e1720c4d2a54a6e6b8b57 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 4 Apr 2018 11:27:03 +0200
Subject: [PATCH] [WIP] Stronger lemma for univalence

---
 src/Cat/Category.agda         | 52 +++++++++++++++++++++++++++++++++--
 src/Cat/Category/Product.agda | 27 ++++++++++++++----
 2 files changed, 72 insertions(+), 7 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 0ee54dd..cb0340c 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -131,6 +131,55 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     Univalent[Contr] : Set _
     Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
 
+    private
+      module _ (A : Object) where
+        postulate
+          -- It may be that we need something weaker than this, in that there
+          -- may be some other lemmas available to us.
+          -- For instance, `need0` should be available to us when we prove `need1`.
+          need0 : ∀ Y → A ≡ Y
+          need1 : (f : Arrow A A) → identity ≡ f
+
+        c : Σ Object (A ≅_)
+        c = A , idIso A
+
+        module _ (y : Σ Object (A ≅_)) where
+          open Σ y renaming (proj₁ to Y ; proj₂ to isoY)
+          q : A ≡ Y
+          q = need0 Y
+
+          -- Some error with primComp
+          isoAY : A ≅ Y
+          isoAY = {!id-to-iso A Y q!}
+
+          lem : PathP (λ i → A ≅ q i) (idIso A) isoY
+          lem = d* isoAY
+            where
+            D  : (Y : Object) → (A ≡ Y) → Set _
+            D Y p = (A≅Y : A ≅ Y) → PathP (λ i → A ≅ p i) (idIso A) A≅Y
+            d  : D A refl
+            d A≅Y i = a0 i , a1 i , a2 i
+              where
+              open Σ A≅Y   renaming (proj₁ to f  ; proj₂ to iso-f)
+              open Σ iso-f renaming (proj₁ to f~ ; proj₂ to areInv)
+              a0 : identity ≡ f
+              a0 = need1 f
+              a1 : identity ≡ f~
+              a1 = need1 f~
+              -- we do have this!
+              postulate
+                prop : ∀ {A B} (fg : Arrow A B × Arrow B A) → isProp (IsInverseOf (fst fg) (snd fg))
+              a2 : PathP (λ i → IsInverseOf (a0 i) (a1 i)) isIdentity areInv
+              a2 = lemPropF prop λ i → a0 i , a1 i
+            d* : D Y q
+            d* = pathJ D d Y q
+
+          p : (A , idIso A) ≡ (Y , isoY)
+          p i = need0 Y i , lem i
+
+        univ-lem : isContr (Σ Object (A ≅_))
+        univ-lem = c , p
+
     -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
     -- Date: Wed, Mar 21, 2018 at 3:12 PM
     --
@@ -312,7 +361,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
         res i = fp i , cp i
 
     propInitial : isProp Initial
-    propInitial Xi Yi = {!!}
+    propInitial Xi Yi = res
       where
       open Σ Xi renaming (proj₁ to X ; proj₂ to Xii)
       open Σ Yi renaming (proj₁ to Y ; proj₂ to Yii)
@@ -342,7 +391,6 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
       res : Xi ≡ Yi
       res i = p0 i , p1 i
 
-
 -- | Propositionality of being a category
 module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 0e25ba2..a811ecd 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -172,16 +172,33 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       open import Cubical.Univalence
       module _ (c : (X , x) ≅ (Y , y)) where
       -- module _ (c : _ ≅ _) where
+        open Σ c renaming (proj₁ to f_c ; proj₂ to inv_c)
+        open Σ inv_c renaming (proj₁ to g_c ; proj₂ to ainv_c)
+        open Σ ainv_c renaming (proj₁ to left ; proj₂ to right)
         c0 : X ℂ.≅ Y
-        c0 = {!!}
+        c0 = proj₁ f_c , proj₁ g_c , (λ i → proj₁ (left i)) , (λ i → proj₁ (right i))
         f0 : X ≡ Y
         f0 = ℂ.iso-to-id c0
-        f1 : PathP (λ i → ℂ.Arrow (f0 i) A × ℂ.Arrow (f0 i) B) x y
-        f1 = {!!}
+        module _ {A : ℂ.Object} (α : ℂ.Arrow X A) where
+          coedom : ℂ.Arrow Y A
+          coedom = coe (λ i → ℂ.Arrow (f0 i) A) α
+        coex : ℂ.Arrow Y A × ℂ.Arrow Y B
+        coex = coe (λ i → ℂ.Arrow (f0 i) A × ℂ.Arrow (f0 i) B) x
+        f1 : PathP (λ i → ℂ.Arrow (f0 i) A × ℂ.Arrow (f0 i) B) x coex
+        f1 = {!sym!}
+        f2 : coex ≡ y
+        f2 = {!!}
         f : (X , x) ≡ (Y , y)
-        f i = f0 i , f1 i
+        f i = f0 i , {!f1 i!}
+      prp : isSet (ℂ.Object × ℂ.Arrow Y A × ℂ.Arrow Y B)
+      prp = setSig {sA = {!!}} {(λ _ → setSig {sA = ℂ.arrowsAreSets} {λ _ → ℂ.arrowsAreSets})}
+      ve-re : (p : (X , x) ≡ (Y , y)) → f (id-to-iso _ _ p) ≡ p
+      -- ve-re p i j = {!ℂ.arrowsAreSets!} , ℂ.arrowsAreSets _ _ (let k = proj₁ (proj₂ (p i)) in {!!}) {!!} {!!} {!!} , {!!}
+      ve-re p = let k = prp {!!} {!!} {!!} {!p!} in {!!}
+      re-ve : (iso : (X , x) ≅ (Y , y)) → id-to-iso _ _ (f iso) ≡ iso
+      re-ve = {!!}
       iso : E.Isomorphism (id-to-iso (X , x) (Y , y))
-      iso = f , record { verso-recto = {!!} ; recto-verso = {!!} }
+      iso = f , record { verso-recto = funExt ve-re ; recto-verso = funExt re-ve }
       res : isEquiv ((X , x) ≡ (Y , y)) ((X , x) ≅ (Y , y)) (id-to-iso (X , x) (Y , y))
       res = Equiv≃.fromIso _ _ iso