Move lemma to equivalence-module

src/Cat/Categories/Sets.agda

@@ -106,59 +106,6 @@ module _ (ℓ : Level) where
         iso : (p ≡ q) ≈ (fst p ≡ fst q)
         iso = f , g , inv
 
-      lem3 : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)}
-        → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q
-      lem3 {Q = Q} eA = res
-        where
-        f : Σ A P → Σ A Q
-        f (a , pA) = a , fst (eA a) pA
-        g : Σ A Q → Σ A P
-        g (a , qA) = a , g' qA
-          where
-          k : TypeIsomorphism _
-          k = toIso _ _ (snd (eA a))
-          open Σ k renaming (fst to g')
-        ve-re : (x : Σ A P) → (g ∘ f) x ≡ x
-        ve-re x i = fst x , eq i
-          where
-          eq : snd ((g ∘ f) x) ≡ snd x
-          eq = begin
-            snd ((g ∘ f) x) ≡⟨⟩
-            snd (g (f (a , pA))) ≡⟨⟩
-            g' (fst (eA a) pA) ≡⟨ lem ⟩
-            pA ∎
-            where
-            open Σ x renaming (fst to a ; snd to pA)
-            k : TypeIsomorphism _
-            k = toIso _ _ (snd (eA a))
-            open Σ k renaming (fst to g' ; snd to inv)
-            module A = AreInverses inv
-            -- anti-funExt
-            lem : (g' ∘ (fst (eA a))) pA ≡ pA
-            lem i = A.verso-recto i pA
-        re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
-        re-ve x i = fst x , eq i
-          where
-          open Σ x renaming (fst to a ; snd to qA)
-          eq = begin
-            snd ((f ∘ g) x)                 ≡⟨⟩
-            fst (eA a) (g' qA)            ≡⟨ (λ i → A.recto-verso i qA) ⟩
-            qA                                ∎
-            where
-            k : TypeIsomorphism _
-            k = toIso _ _ (snd (eA a))
-            open Σ k renaming (fst to g' ; snd to inv)
-            module A = AreInverses inv
-        inv : AreInverses f g
-        inv = record
-          { verso-recto = funExt ve-re
-          ; recto-verso = funExt re-ve
-          }
-        iso : Σ A P ≈ Σ A Q
-        iso = f , g , inv
-        res : Σ A P ≃ Σ A Q
-        res = fromIsomorphism _ _ iso
-
     module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
       lem4 : isSet A → isSet B → (f : A → B)
         → isEquiv A B f ≃ isIso f
@@ -186,7 +133,7 @@ module _ (ℓ : Level) where
 
       -- lem3 and the equivalence from lem4
       step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B)
-      step0 = lem3 {ℓc = lzero} (λ f → sym≃ (lem4 sA sB f))
+      step0 = equivSig (λ f → sym≃ (lem4 sA sB f))
 
       -- univalence
       step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B)
@@ -219,7 +166,7 @@ module _ (ℓ : Level) where
       open Σ hA renaming (fst to A)
 
       eq1 : (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB)
-      eq1 = ua (lem3 (\ hB → univ≃))
+      eq1 = ua (equivSig (\ hB → univ≃))
 
       univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB)
       univalent[Contr] = subst {P = isContr} (sym eq1) tres

src/Cat/Category.agda

@@ -147,8 +147,11 @@ 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)
+
         aux : isContr (Σ[ B ∈ Object ] A ≡ B)
-        aux = {!!}
+        aux = {!Σ Object (A ≡_)!}
 
         step : isContr (Σ Object (A ≅_))
         step = {!subst {P = isContr} {!!} aux!}

src/Cat/Category/Product.agda

@@ -172,32 +172,15 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
     open IsPreCategory isPreCat
 
     univalent : Univalent
-    univalent {(X , xa , xb)} {(Y , ya , yb)} = univalenceFromIsomorphism res
+    univalent {(X , xa , xb)} {(Y , ya , yb)} = {!!}
-      where
-      open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≈_)
-      -- open import Relation.Binary.PreorderReasoning (Cat.Equivalence.preorder≅ {!!}) using ()
-      --   renaming
-      --     ( _∼⟨_⟩_ to _≈⟨_⟩_
-      --     ; begin_ to begin!_
-      --     ; _∎ to _∎! )
-      -- lawl
-      --   : ((X , xa , xb) ≡ (Y , ya , yb))
-      --   ≈ (Σ[ iso ∈ (X ℂ.≅ Y) ] let p = ℂ.isoToId iso in (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
-      -- lawl = {!begin! ? ≈⟨ ? ⟩ ? ∎!!}
-      -- Problem with the above approach: Preorders only work for heterogeneous equaluties.
 
-      -- (X , xa , xb) ≡ (Y , ya , yb)
+    -- module _ {(X , xa , xb) : Object} {(Y , ya , yb) : Object} where
-      -- ≅
+    module _ (𝕏 𝕐 : Object) where
-      -- Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)
+      open Σ 𝕏 renaming (fst to X ; snd to x)
-      -- ≅
+      open Σ x renaming (fst to xa ; snd to xb)
-      -- Σ (X ℂ.≅ Y) (λ iso
+      open Σ 𝕐 renaming (fst to Y ; snd to y)
-      --   → let p = ℂ.isoToId iso
+      open Σ y renaming (fst to ya ; snd to yb)
-      --   in
+      open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≈_)
-      --   ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
-      --   × PathP (λ i → ℂ.Arrow (p i) B) xb yb
-      --   )
-      -- ≅
-      -- (X , xa , xb) ≅ (Y , ya , yb)
       step0
         : ((X , xa , xb) ≡ (Y , ya , yb))
         ≈ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
@@ -287,7 +270,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
           let
             iso : X ℂ.≅ Y
             iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
-            helper : PathP (λ i → ℂ.Arrow (ℂ.isoToId ? i) A) xa ya
+            helper : PathP (λ i → ℂ.Arrow (ℂ.isoToId {!!} i) A) xa ya
             helper = {!!}
           in iso , helper , {!!}})
         , record
@@ -315,12 +298,13 @@ 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 = {!!}
 
-      res : TypeIsomorphism (idToIso (X , xa , xb) (Y , ya , yb))
+    univalent' : Univalent
-      res = {!snd equiv1!}
+    univalent' = from[Andrea] equiv4reel
-
-    univalent2 : ∀ X Y → (X ≅ Y) ≃ (X ≡ Y)
-    univalent2 = {!!}
 
     isCat : IsCategory raw
     IsCategory.isPreCategory isCat = isPreCat

src/Cat/Equivalence.agda

@@ -445,3 +445,57 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
           ; recto-verso = funExt ve-re
           }
     in fromIsomorphism _ _ iso
+
+module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
+  equivSig : {ℓc : Level} {Q : A → Set ℓc}
+    → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q
+  equivSig {Q = Q} eA = res
+    where
+    f : Σ A P → Σ A Q
+    f (a , pA) = a , fst (eA a) pA
+    g : Σ A Q → Σ A P
+    g (a , qA) = a , g' qA
+      where
+      k : Isomorphism _
+      k = toIso _ _ (snd (eA a))
+      open Σ k renaming (fst to g')
+    ve-re : (x : Σ A P) → (g ∘ f) x ≡ x
+    ve-re x i = fst x , eq i
+      where
+      eq : snd ((g ∘ f) x) ≡ snd x
+      eq = begin
+        snd ((g ∘ f) x) ≡⟨⟩
+        snd (g (f (a , pA))) ≡⟨⟩
+        g' (fst (eA a) pA) ≡⟨ lem ⟩
+        pA ∎
+        where
+        open Σ x renaming (fst to a ; snd to pA)
+        k : Isomorphism _
+        k = toIso _ _ (snd (eA a))
+        open Σ k renaming (fst to g' ; snd to inv)
+        module A = AreInverses inv
+        -- anti-funExt
+        lem : (g' ∘ (fst (eA a))) pA ≡ pA
+        lem i = A.verso-recto i pA
+    re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
+    re-ve x i = fst x , eq i
+      where
+      open Σ x renaming (fst to a ; snd to qA)
+      eq = begin
+        snd ((f ∘ g) x)                 ≡⟨⟩
+        fst (eA a) (g' qA)            ≡⟨ (λ i → A.recto-verso i qA) ⟩
+        qA                                ∎
+        where
+        k : Isomorphism _
+        k = toIso _ _ (snd (eA a))
+        open Σ k renaming (fst to g' ; snd to inv)
+        module A = AreInverses inv
+    inv : AreInverses f g
+    inv = record
+      { verso-recto = funExt ve-re
+      ; recto-verso = funExt re-ve
+      }
+    iso : Σ A P ≅ Σ A Q
+    iso = f , g , inv
+    res : Σ A P ≃ Σ A Q
+    res = fromIsomorphism _ _ iso