From e6a2e3a0f090b9bf2c03e2c1e465d53935cb46ab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 11 Apr 2018 13:18:34 +0200
Subject: [PATCH] Reduce applications of symmetry

---
 src/Cat/Categories/Sets.agda  | 24 ++++++++----------------
 src/Cat/Category.agda         |  8 ++++----
 src/Cat/Category/Product.agda | 12 ++----------
 3 files changed, 14 insertions(+), 30 deletions(-)

diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index be62a35..80b8080 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -132,20 +132,16 @@ module _ (ℓ : Level) where
       open Σ hB renaming (fst to B ; snd to sB)
 
       -- lem3 and the equivalence from lem4
-      step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B)
-      step0 = equivSig (λ f → sym≃ (lem4 sA sB f))
-
-      -- univalence
-      step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B)
-      step1 = sym≃ univalence
+      step0 : Σ (A → B) (isEquiv A B) ≃ Σ (A → B) isIso
+      step0 = equivSig (lem4 sA sB)
 
       -- lem2 with propIsSet
-      step2 : (A ≡ B) ≃ (hA ≡ hB)
-      step2 = sym≃ (lem2 (λ A → isSetIsProp) hA hB)
+      step2 : (hA ≡ hB) ≃ (A ≡ B)
+      step2 = lem2 (λ A → isSetIsProp) hA hB
 
       -- Go from an isomorphism on sets to an isomorphism on homotopic sets
-      trivial? : (hA ≅ hB) ≃ (A ≈ B)
-      trivial? = sym≃ (fromIsomorphism _ _ res)
+      trivial? : (A ≈ B) ≃ (hA ≅ hB)
+      trivial? = fromIsomorphism _ _ res
         where
         fwd : Σ (A → B) isIso → hA ≅ hB
         fwd (f , g , inv) = f , g , inv.toPair
@@ -155,12 +151,8 @@ module _ (ℓ : Level) where
         bwd (f , g , x , y) = f , g , record { verso-recto = x ; recto-verso = y }
         res : Σ (A → B) isIso ≈ (hA ≅ hB)
         res = fwd , bwd , record { verso-recto = refl ; recto-verso = refl }
-
-      conclusion : (hA ≅ hB) ≃ (hA ≡ hB)
-      conclusion = trivial? ⊙ step0 ⊙ step1 ⊙ step2
-
-      univ≃ : (hA ≅ hB) ≃ (hA ≡ hB)
-      univ≃ = trivial? ⊙ step0 ⊙ step1 ⊙ step2
+      univ≃ : (hA ≡ hB) ≃ (hA ≅ hB)
+      univ≃ = step2 ⊙ univalence ⊙ step0 ⊙ trivial?
 
     univalent : Univalent
     univalent = from[Andrea] (λ _ _ → univ≃)
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index a39dd27..d8febb7 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -135,7 +135,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
 
     Univalent[Andrea] : Set _
-    Univalent[Andrea] = ∀ A B → (A ≅ B) ≃ (A ≡ B)
+    Univalent[Andrea] = ∀ A B → (A ≡ B) ≃ (A ≅ B)
 
     -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
     -- Date: Wed, Mar 21, 2018 at 3:12 PM
@@ -147,14 +147,14 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     from[Andrea] = from[Contr] ∘ step
       where
       module _ (f : Univalent[Andrea]) (A : Object) where
-        lem : Σ Object (A ≅_) ≃ Σ Object (A ≡_)
-        lem = equivSig {ℓa} {ℓb} {Object} {A ≅_} {_} {A ≡_} (f A)
+        lem : Σ Object (A ≡_) ≃ Σ Object (A ≅_)
+        lem = equivSig (f A)
 
         aux : isContr (Σ Object (A ≡_))
         aux = (A , refl) , (λ y → contrSingl (snd y))
 
         step : isContr (Σ Object (A ≅_))
-        step = equivPreservesNType {n = ⟨-2⟩} (Equivalence.symmetry lem) aux
+        step = equivPreservesNType {n = ⟨-2⟩} lem aux
 
     propUnivalent : isProp Univalent
     propUnivalent a b i = propPi (λ iso → propIsContr) a b i
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 663503f..0c7170d 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -171,10 +171,6 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
 
     open IsPreCategory isPreCat
 
-    univalent : Univalent
-    univalent {(X , xa , xb)} {(Y , ya , yb)} = {!!}
-
-    -- module _ {(X , xa , xb) : Object} {(Y , ya , yb) : Object} where
     module _ (𝕏 𝕐 : Object) where
       open Σ 𝕏 renaming (fst to X ; snd to x)
       open Σ x renaming (fst to xa ; snd to xb)
@@ -298,13 +294,9 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         : ((X , xa , xb) ≡ (Y , ya , yb))
         ≃ ((X , xa , xb) ≅ (Y , ya , yb))
       equiv1 = _ , fromIso _ _ (snd iso)
-      equiv4reel
-        : ((X , xa , xb) ≅ (Y , ya , yb))
-        ≃ ((X , xa , xb) ≡ (Y , ya , yb))
-      equiv4reel = {!!}
 
-    univalent' : Univalent
-    univalent' = from[Andrea] equiv4reel
+    univalent : Univalent
+    univalent = from[Andrea] equiv1
 
     isCat : IsCategory raw
     IsCategory.isPreCategory isCat = isPreCat