From 66ab7138a63a643f5bc24ed845bc7249f7ee9822 Mon Sep 17 00:00:00 2001
From: Andrea Vezzosi <sanzhiyan@gmail.com>
Date: Thu, 22 Mar 2018 10:41:38 +0000
Subject: [PATCH] generalized lem3 and made progress for Sets univalence

---
 src/Cat/Categories/Sets.agda | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index b96822b..14be2a4 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -138,14 +138,10 @@ module _ (ℓ : Level) where
         iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q)
         iso = f , g , inv
 
-      lem3 : {Q : A → Set ℓb}
+      lem3 : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)}
         → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q
-      lem3 {Q} eA = res
+      lem3 {Q = Q} eA = res
         where
-        P→Q : ∀ {a} → P a ≡ Q a
-        P→Q = ua (eA _)
-        Q→P : ∀ {a} → Q a ≡ P a
-        Q→P = sym P→Q
         f : Σ A P → Σ A Q
         f (a , pA) = a , _≃_.eqv (eA a) pA
         g : Σ A Q → Σ A P
@@ -226,7 +222,7 @@ module _ (ℓ : Level) where
 
       -- lem3 and the equivalence from lem4
       step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B)
-      step0 = lem3 (λ f → sym≃ (lem4 sA sB f))
+      step0 = lem3 {ℓc = lzero} (λ f → sym≃ (lem4 sA sB f))
       -- univalence
       step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B)
       step1 = hh ⊙ h
@@ -297,8 +293,11 @@ module _ (ℓ : Level) where
       --
       -- is contractible, which implies univalence.
 
+    eq1 : ∀ hA → (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB)
+    eq1 hA = (ua (lem3 (\ hB → sym≃ thr)))
+
     univalent[Contr] : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB)
-    univalent[Contr] hA = {!!} , {!!}
+    univalent[Contr] hA = subst {P = isContr} (sym (eq1 hA)) {!!}
 
     univalent : Univalent
     univalent = from[Contr] univalent[Contr]