Preunivalence implies strong preunivalence (#1364)

As demonstrated by Evan Cavallo, strong preunivalence follows from
preunivalence + function extensionality.
By an analogous proof, preunivalent categories are strongly
preunivalent.

Author: fredrik-bakke

.vscode/agda.code-snippets

@@ -21,14 +21,19 @@
     "description": "Equational reasoning",
     "prefix": ["equational-reasoning"]
   },
-  "Homotopy-reasoning": {
+  "Homotopy reasoning": {
     "body": ["homotopy-reasoning ? ~ ? by ?"],
-    "description": "Homotopy-reasoning",
+    "description": "Homotopy reasoning",
     "prefix": ["homotopy-reasoning"]
   },
-  "Equivalence-reasoning": {
+  "Equivalence reasoning": {
     "body": ["equivalence-reasoning ? ≃ ? by ?"],
-    "description": "Equivalence-reasoning",
+    "description": "Equivalence reasoning",
     "prefix": ["equivalence-reasoning"]
+  },
+  "Retract reasoning": {
+    "body": ["retract-reasoning ? retract-of ? by ?"],
+    "description": "Retract reasoning",
+    "prefix": ["retract-reasoning"]
   }
 }

src/category-theory/cores-precategories.lagda.md

@@ -121,6 +121,10 @@ module _
     iso-Precategory (core-precategory-Precategory C) x y ≃ iso-Precategory C x y
   inv-compute-iso-core-Precategory =
     inv-compute-iso-Pregroupoid (core-pregroupoid-Precategory C)
+
+  inclusion-iso-core-Precategory :
+    iso-Precategory C x y → iso-Precategory (core-precategory-Precategory C) x y
+  inclusion-iso-core-Precategory = map-equiv compute-iso-core-Precategory
 ```
 
 ### The core is replete

src/category-theory/isomorphisms-in-precategories.lagda.md

@@ -22,6 +22,7 @@ open import foundation.retractions
 open import foundation.sections
 open import foundation.sets
 open import foundation.subtypes
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 
@@ -420,7 +421,7 @@ module _
     is-section-hom-inv-is-iso-Precategory C p
 ```
 
-### Inverses of isomorphisms
+### The inverse operation on isomorphisms
 
 ```agda
 module _
@@ -527,6 +528,49 @@ module _
       ( is-section-hom-inv-iso-Precategory C f)
 ```
 
+### The 3-for-2 property of isomorphisms
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y z : obj-Precategory C}
+  (f : hom-Precategory C x y)
+  (g : hom-Precategory C y z)
+  where
+
+  is-iso-left-factor-Precategory :
+    is-iso-Precategory C f →
+    is-iso-Precategory C (comp-hom-Precategory C g f) →
+    is-iso-Precategory C g
+  is-iso-left-factor-Precategory F GF =
+    tr
+      ( is-iso-Precategory C)
+      ( equational-reasoning
+        ( comp-hom-Precategory C
+          ( comp-hom-Precategory C g f)
+          ( hom-inv-is-iso-Precategory C F))
+        ＝ ( comp-hom-Precategory C
+            ( g)
+            ( comp-hom-Precategory C f ( hom-inv-is-iso-Precategory C F)))
+          by
+          associative-comp-hom-Precategory C
+            ( g)
+            ( f)
+            ( hom-inv-is-iso-Precategory C F)
+        ＝ (comp-hom-Precategory C g (id-hom-Precategory C))
+          by
+            ap
+              ( comp-hom-Precategory C g)
+              ( is-section-hom-inv-is-iso-Precategory C F)
+        ＝ g
+          by right-unit-law-comp-hom-Precategory C g)
+      ( is-iso-comp-is-iso-Precategory C GF (is-iso-inv-is-iso-Precategory C F))
+```
+
+> It remains to formalize the implication
+> `is-iso g → is-iso (g ∘ f) → is-iso f`.
+
 ### The inverse operation is a fibered involution on isomorphisms
 
 ```agda
@@ -706,6 +750,37 @@ module _
     equiv-precomp-hom-is-iso-Precategory C (is-iso-iso-Precategory C f) z
 ```
 
+```agda
+module _
+  {l1 l2 : Level}
+  (C : Precategory l1 l2)
+  {x y : obj-Precategory C}
+  (f : iso-Precategory C x y)
+  (z : obj-Precategory C)
+  where
+
+  precomp-iso-Precategory : iso-Precategory C y z → iso-Precategory C x z
+  precomp-iso-Precategory g = comp-iso-Precategory C g f
+
+  is-equiv-precomp-iso-Precategory : is-equiv precomp-iso-Precategory
+  is-equiv-precomp-iso-Precategory =
+    is-equiv-subtype-is-equiv
+      ( is-prop-is-iso-Precategory C)
+      ( is-prop-is-iso-Precategory C)
+      ( precomp-hom-Precategory C (hom-iso-Precategory C f) z)
+      ( λ g is-iso-g →
+        is-iso-comp-is-iso-Precategory C is-iso-g (is-iso-iso-Precategory C f))
+      ( is-equiv-precomp-hom-iso-Precategory C f z)
+      ( λ g →
+        is-iso-left-factor-Precategory C (hom-iso-Precategory C f) g
+          ( is-iso-iso-Precategory C f))
+
+  equiv-precomp-iso-Precategory :
+    iso-Precategory C y z ≃ iso-Precategory C x z
+  equiv-precomp-iso-Precategory =
+    ( precomp-iso-Precategory , is-equiv-precomp-iso-Precategory)
+```
+
 ### A morphism `f` is an isomorphism if and only if postcomposition by `f` is an equivalence
 
 **Proof:** If `f` is an isomorphism with inverse `f⁻¹`, then postcomposing with

src/category-theory/strongly-preunivalent-categories.lagda.md

@@ -16,6 +16,9 @@ open import foundation.1-types
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.embeddings
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.fibers-of-maps
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositional-maps
@@ -80,8 +83,8 @@ module _
     is-preunivalent-Precategory 𝒞
   is-preunivalent-is-strongly-preunivalent-Precategory H x y =
     is-emb-is-prop-map
-      ( backward-implication-subuniverse-equality-duality
-        ( is-prop-Prop)
+      ( backward-implication-structured-equality-duality
+        ( is-prop-equiv')
         ( H x)
         ( x)
         ( iso-eq-Precategory 𝒞 x)
@@ -367,6 +370,44 @@ module _
       ( is-1-type-obj-Strongly-Preunivalent-Category 𝒞)
 ```
 
+## Preunivalent categories are strongly preunivalent
+
+```agda
+is-strongly-preunivalent-is-preunivalent-Precategory :
+  {l1 l2 : Level} (𝒞 : Precategory l1 l2) →
+  is-preunivalent-Precategory 𝒞 → is-strongly-preunivalent-Precategory 𝒞
+is-strongly-preunivalent-is-preunivalent-Precategory 𝒞 pua x (y , α) (y' , α') =
+  is-prop-equiv
+    ( equivalence-reasoning
+      ( (y , α) ＝ (y' , α'))
+      ≃ Eq-Σ (y , α) (y' , α') by equiv-pair-eq-Σ (y , α) (y' , α')
+      ≃ fiber
+          ( iso-eq-Precategory 𝒞 y y')
+          ( comp-iso-Precategory 𝒞 α' (inv-iso-Precategory 𝒞 α))
+      by
+        equiv-tot
+        ( λ where
+          refl →
+            equivalence-reasoning
+            (α ＝ α')
+            ≃ ( comp-iso-Precategory 𝒞 α (inv-iso-Precategory 𝒞 α) ＝
+                comp-iso-Precategory 𝒞 α' (inv-iso-Precategory 𝒞 α))
+              by
+                equiv-ap
+                  ( equiv-precomp-iso-Precategory 𝒞 (inv-iso-Precategory 𝒞 α) y)
+                  ( α)
+                  ( α')
+            ≃ ( id-iso-Precategory 𝒞 ＝
+                comp-iso-Precategory 𝒞 α' (inv-iso-Precategory 𝒞 α))
+              by
+              equiv-concat
+                ( inv (right-inverse-law-comp-iso-Precategory 𝒞 α))
+                ( comp-iso-Precategory 𝒞 α' (inv-iso-Precategory 𝒞 α))))
+    ( is-prop-map-is-emb
+      ( pua y y')
+      ( comp-iso-Precategory 𝒞 α' (inv-iso-Precategory 𝒞 α)))
+```
+
 ## See also
 
 - [The strong preunivalence axiom](foundation.strong-preunivalence.md)

src/foundation-core/equality-dependent-pair-types.lagda.md

@@ -16,6 +16,7 @@ open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
+open import foundation-core.retracts-of-types
 open import foundation-core.transport-along-identifications
 ```
 
@@ -112,10 +113,12 @@ module _
         ( is-section-pair-eq-Σ s t)
 
   equiv-pair-eq-Σ : (s t : Σ A B) → (s ＝ t) ≃ Eq-Σ s t
-  pr1 (equiv-pair-eq-Σ s t) = pair-eq-Σ
-  pr2 (equiv-pair-eq-Σ s t) = is-equiv-pair-eq-Σ s t
+  equiv-pair-eq-Σ s t = (pair-eq-Σ , is-equiv-pair-eq-Σ s t)
 
-  η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t
+  retract-pair-eq-Σ : (s t : Σ A B) → (s ＝ t) retract-of (Eq-Σ s t)
+  retract-pair-eq-Σ s t = (pair-eq-Σ , eq-pair-Σ' , is-section-pair-eq-Σ s t)
+
+  η-pair : (t : Σ A B) → (pr1 t , pr2 t) ＝ t
   η-pair t = refl
 ```
 

src/foundation-core/identity-types.lagda.md

@@ -240,7 +240,7 @@ module _
 
   assoc :
     {x y z w : A} (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) →
-    ((p ∙ q) ∙ r) ＝ (p ∙ (q ∙ r))
+    (p ∙ q) ∙ r ＝ p ∙ (q ∙ r)
   assoc refl q r = refl
 ```
 
@@ -268,13 +268,13 @@ module _
 
   double-assoc :
     {x y z w v : A} (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) (s : w ＝ v) →
-    (((p ∙ q) ∙ r) ∙ s) ＝ p ∙ (q ∙ (r ∙ s))
+    ((p ∙ q) ∙ r) ∙ s ＝ p ∙ (q ∙ (r ∙ s))
   double-assoc refl q r s = assoc q r s
 
   triple-assoc :
     {x y z w v u : A}
     (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) (s : w ＝ v) (t : v ＝ u) →
-    ((((p ∙ q) ∙ r) ∙ s) ∙ t) ＝ p ∙ (q ∙ (r ∙ (s ∙ t)))
+    (((p ∙ q) ∙ r) ∙ s) ∙ t ＝ p ∙ (q ∙ (r ∙ (s ∙ t)))
   triple-assoc refl q r s t = double-assoc q r s t
 ```
 
@@ -298,7 +298,7 @@ module _
   left-inv : {x y : A} (p : x ＝ y) → inv p ∙ p ＝ refl
   left-inv refl = refl
 
-  right-inv : {x y : A} (p : x ＝ y) → p ∙ (inv p) ＝ refl
+  right-inv : {x y : A} (p : x ＝ y) → p ∙ inv p ＝ refl
   right-inv refl = refl
 ```
 
@@ -355,11 +355,11 @@ module _
   where
 
   is-retraction-inv-concat :
-    {x y z : A} (p : x ＝ y) (q : y ＝ z) → (inv p ∙ (p ∙ q)) ＝ q
+    {x y z : A} (p : x ＝ y) (q : y ＝ z) → inv p ∙ (p ∙ q) ＝ q
   is-retraction-inv-concat refl q = refl
 
   is-section-inv-concat :
-    {x y z : A} (p : x ＝ y) (r : x ＝ z) → (p ∙ (inv p ∙ r)) ＝ r
+    {x y z : A} (p : x ＝ y) (r : x ＝ z) → p ∙ (inv p ∙ r) ＝ r
   is-section-inv-concat refl r = refl
 
   is-retraction-inv-concat' :

src/foundation-core/retracts-of-types.lagda.md

@@ -203,6 +203,37 @@ module _
       ( retraction-retract r')
 ```
 
+## Retract reasoning
+
+Retracts can be constructed by equational reasoning in the following way:
+
+```text
+retract-reasoning
+  X retract-of Y by retract-1
+    retract-of Z by retract-2
+    retract-of V by retract-3
+```
+
+The retract constructed in this way is
+`comp-retract retract-3 (comp-retract retract-2 retract-1)`, i.e., the retract
+is associated fully to the right.
+
+```agda
+infixl 1 retract-reasoning_
+infixl 0 step-retract-reasoning
+
+retract-reasoning_ :
+  {l1 : Level} (X : UU l1) → X retract-of X
+retract-reasoning X = id-retract
+
+step-retract-reasoning :
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
+  (X retract-of Y) → (Z : UU l3) → (Y retract-of Z) → (X retract-of Z)
+step-retract-reasoning e Z f = comp-retract f e
+
+syntax step-retract-reasoning e Z f = e retract-of Z by f
+```
+
 ## See also
 
 - [Retracts of maps](foundation.retracts-of-maps.md)