diff --git a/.vscode/agda.code-snippets b/.vscode/agda.code-snippets
index 1869ef9188..817c4485b2 100644
--- a/.vscode/agda.code-snippets
+++ b/.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"]
   }
 }
diff --git a/src/category-theory/cores-precategories.lagda.md b/src/category-theory/cores-precategories.lagda.md
index 210c08f99c..72d32c1b12 100644
--- a/src/category-theory/cores-precategories.lagda.md
+++ b/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
diff --git a/src/category-theory/isomorphisms-in-precategories.lagda.md b/src/category-theory/isomorphisms-in-precategories.lagda.md
index 31a63e5d4f..6b46d5aa26 100644
--- a/src/category-theory/isomorphisms-in-precategories.lagda.md
+++ b/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,48 @@ 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 other 2 cases of the 3-for-2 property.
+
 ### The inverse operation is a fibered involution on isomorphisms
 
 ```agda
@@ -706,6 +749,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
diff --git a/src/category-theory/strongly-preunivalent-categories.lagda.md b/src/category-theory/strongly-preunivalent-categories.lagda.md
index 8ba02ef3ba..6d85226c73 100644
--- a/src/category-theory/strongly-preunivalent-categories.lagda.md
+++ b/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)
diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md
index bcc2650afd..24d3238eef 100644
--- a/src/foundation-core/equality-dependent-pair-types.lagda.md
+++ b/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
 ```
 
diff --git a/src/foundation-core/identity-types.lagda.md b/src/foundation-core/identity-types.lagda.md
index 1a8a144f36..c62936f746 100644
--- a/src/foundation-core/identity-types.lagda.md
+++ b/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' :
diff --git a/src/foundation-core/retracts-of-types.lagda.md b/src/foundation-core/retracts-of-types.lagda.md
index 43c71c5134..1b18d5e0ce 100644
--- a/src/foundation-core/retracts-of-types.lagda.md
+++ b/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)
diff --git a/src/foundation-core/small-types.lagda.md b/src/foundation-core/small-types.lagda.md
index 96a3cd8d75..838cd07547 100644
--- a/src/foundation-core/small-types.lagda.md
+++ b/src/foundation-core/small-types.lagda.md
@@ -11,6 +11,7 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-dependent-function-types
+open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.mere-equivalences
 open import foundation.propositional-truncations
@@ -25,8 +26,10 @@ open import foundation-core.cartesian-product-types
 open import foundation-core.coherently-invertible-maps
 open import foundation-core.contractible-types
 open import foundation-core.coproduct-types
+open import foundation-core.dependent-identifications
+open import foundation-core.equality-dependent-pair-types
+open import foundation-core.fibers-of-maps
 open import foundation-core.functoriality-dependent-pair-types
-open import foundation-core.identity-types
 open import foundation-core.propositions
 open import foundation-core.retractions
 open import foundation-core.sections
@@ -132,15 +135,14 @@ module _
   is-prop-is-small = is-prop-is-proof-irrelevant is-proof-irrelevant-is-small
 
   is-small-Prop : Prop (lsuc l ⊔ l1)
-  is-small-Prop = is-small l A , is-prop-is-small
+  is-small-Prop = (is-small l A , is-prop-is-small)
 ```
 
 ### Any type in `UU l1` is `l1`-small
 
 ```agda
 is-small' : {l1 : Level} {A : UU l1} → is-small l1 A
-pr1 (is-small' {A = A}) = A
-pr2 is-small' = id-equiv
+is-small' {A = A} = (A , id-equiv)
 ```
 
 ### Every type of universe level `l1` is `(l1 ⊔ l2)`-small
@@ -151,8 +153,7 @@ module _
   where
 
   is-small-lmax : is-small (l1 ⊔ l2) X
-  pr1 is-small-lmax = raise l2 X
-  pr2 is-small-lmax = compute-raise l2 X
+  is-small-lmax = (raise l2 X , compute-raise l2 X)
 
   is-contr-is-small-lmax :
     is-contr (is-small (l1 ⊔ l2) X)
@@ -164,7 +165,7 @@ module _
 
 ```agda
 is-small-lsuc : {l : Level} (X : UU l) → is-small (lsuc l) X
-is-small-lsuc {l} X = is-small-lmax (lsuc l) X
+is-small-lsuc {l} = is-small-lmax (lsuc l)
 ```
 
 ### Small types are closed under equivalences
@@ -173,8 +174,7 @@ is-small-lsuc {l} X = is-small-lmax (lsuc l) X
 is-small-equiv :
   {l1 l2 l3 : Level} {A : UU l1} (B : UU l2) →
   A ≃ B → is-small l3 B → is-small l3 A
-pr1 (is-small-equiv B e (X , h)) = X
-pr2 (is-small-equiv B e (X , h)) = h ∘e e
+is-small-equiv B e (X , h) = (X , h ∘e e)
 
 is-small-equiv' :
   {l1 l2 l3 : Level} (A : UU l1) {B : UU l2} →
@@ -210,13 +210,31 @@ is-small-mere-equiv l e H =
     ( λ e' → is-small-equiv _ e' H)
 ```
 
+### The equality type of the smallness predicate is equivalent to the fiber of `equiv-eq`
+
+This computation uses the function extensionality axiom.
+
+```agda
+compute-eq-is-small :
+  {l1 l2 : Level} {X : UU l1} (α β : is-small l2 X) →
+  (α ＝ β) ≃ fiber equiv-eq (equiv-is-small β ∘e inv-equiv-is-small α)
+compute-eq-is-small {X = X} (Y , α) (Y' , α') =
+  equivalence-reasoning
+  ( (Y , α) ＝ (Y' , α'))
+  ≃ Σ (Y ＝ Y') (λ x → dependent-identification (λ Y → X ≃ Y) x α α')
+    by equiv-pair-eq-Σ (Y , α) (Y' , α')
+  ≃ Σ (Y ＝ Y') (λ x → equiv-eq x ∘e α ＝ α')
+    by equiv-tot (λ p → equiv-concat (tr-equiv-type-right p α) α')
+  ≃ Σ (Y ＝ Y') (λ x → equiv-eq x ＝ α' ∘e inv-equiv α)
+    by equiv-tot (λ p → equiv-right-transpose-equiv-comp α (equiv-eq p) α')
+```
+
 ### Any contractible type is small
 
 ```agda
 is-small-is-contr :
   (l : Level) {l1 : Level} {A : UU l1} → is-contr A → is-small l A
-pr1 (is-small-is-contr l H) = raise-unit l
-pr2 (is-small-is-contr l H) = equiv-is-contr H is-contr-raise-unit
+is-small-is-contr l H = (raise-unit l , equiv-is-contr H is-contr-raise-unit)
 ```
 
 ### The unit type is small with respect to any universe
diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md
index 14919d3b92..2e28767d65 100644
--- a/src/foundation/equivalences.lagda.md
+++ b/src/foundation/equivalences.lagda.md
@@ -492,7 +492,7 @@ module _
 
   distributive-inv-comp-equiv :
     (e : X ≃ Y) (f : Y ≃ Z) →
-    (inv-equiv (f ∘e e)) ＝ ((inv-equiv e) ∘e (inv-equiv f))
+    inv-equiv (f ∘e e) ＝ (inv-equiv e) ∘e (inv-equiv f)
   distributive-inv-comp-equiv e f =
     eq-htpy-equiv
       ( λ x →
@@ -574,6 +574,45 @@ pr1 (equiv-precomp-equiv e C) = _∘e e
 pr2 (equiv-precomp-equiv e C) = is-equiv-precomp-equiv-equiv e
 ```
 
+### Transposing inverses
+
+```agda
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3}
+  (p : X ≃ Y) (q : Y ≃ Z) (r : X ≃ Z)
+  where
+
+  equiv-right-transpose-equiv-comp :
+    (q ∘e p ＝ r) ≃ (q ＝ r ∘e inv-equiv p)
+  equiv-right-transpose-equiv-comp =
+    eq-transpose-equiv (equiv-precomp-equiv p Z) q r
+
+  equiv-left-transpose-equiv-comp :
+    (q ∘e p ＝ r) ≃ (p ＝ inv-equiv q ∘e r)
+  equiv-left-transpose-equiv-comp =
+    eq-transpose-equiv (equiv-postcomp-equiv q X) p r
+
+  right-transpose-equiv-comp :
+    q ∘e p ＝ r → q ＝ r ∘e inv-equiv p
+  right-transpose-equiv-comp s =
+    inv (is-retraction-precomp-equiv-inv-equiv p q) ∙ ap (_∘e inv-equiv p) s
+
+  inv-right-transpose-equiv-comp :
+    q ＝ r ∘e inv-equiv p → q ∘e p ＝ r
+  inv-right-transpose-equiv-comp s =
+    ap (_∘e p) s ∙ is-section-precomp-equiv-inv-equiv p r
+
+  left-transpose-equiv-comp :
+    q ∘e p ＝ r → p ＝ inv-equiv q ∘e r
+  left-transpose-equiv-comp s =
+    inv (is-retraction-postcomp-equiv-inv-equiv q p) ∙ ap (inv-equiv q ∘e_) s
+
+  inv-left-transpose-equiv-comp :
+    p ＝ inv-equiv q ∘e r → q ∘e p ＝ r
+  inv-left-transpose-equiv-comp s =
+    ap (q ∘e_) s ∙ is-section-postcomp-equiv-inv-equiv q r
+```
+
 ### Computing transport in the type of equivalences
 
 ```agda
@@ -585,6 +624,18 @@ module _
     {x y : A} (p : x ＝ y) (e : B x ≃ C x) →
     tr (λ x → B x ≃ C x) p e ＝ equiv-tr C p ∘e e ∘e equiv-tr B (inv p)
   tr-equiv-type refl e = eq-htpy-equiv refl-htpy
+
+module _
+  {l1 l2 : Level} {X : UU l1} {Y Y' : UU l2}
+  where
+
+  tr-equiv-type-right :
+    (p : Y ＝ Y') (α : X ≃ Y) → equiv-tr id p ∘e α ＝ tr (X ≃_) p α
+  tr-equiv-type-right refl = left-unit-law-equiv
+
+  tr-equiv-type-left :
+    (p : Y ＝ Y') (α : Y ≃ X) → α ∘e equiv-tr id (inv p) ＝ tr (_≃ X) p α
+  tr-equiv-type-left refl = right-unit-law-equiv
 ```
 
 ### A cospan in which one of the legs is an equivalence is a pullback if and only if the corresponding map on the cone is an equivalence
diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
index c830446ce5..dd28fcfa22 100644
--- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
+++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
@@ -101,6 +101,7 @@ module _
       is-separated 𝒫 (Σ A B)
     forward-implication-extended-fundamental-theorem-id H K =
       forward-implication-subuniverse-equality-duality 𝒫
+        ( is-in-subuniverse-equiv 𝒫)
         ( λ x f y b →
           apply-universal-property-trunc-Prop
             ( mere-eq-is-0-connected H a x)
@@ -112,7 +113,10 @@ module _
       is-separated 𝒫 (Σ A B) →
       (f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map 𝒫 (f x)
     backward-implication-extended-fundamental-theorem-id K =
-      backward-implication-subuniverse-equality-duality 𝒫 K a
+      backward-implication-subuniverse-equality-duality 𝒫
+        ( is-in-subuniverse-equiv 𝒫)
+        ( K)
+        ( a)
 
   extended-fundamental-theorem-id :
     is-0-connected A →
@@ -120,7 +124,7 @@ module _
     is-separated 𝒫 (Σ A B)
   extended-fundamental-theorem-id H =
     ( forward-implication-extended-fundamental-theorem-id H ,
-    backward-implication-extended-fundamental-theorem-id)
+      backward-implication-extended-fundamental-theorem-id)
 ```
 
 ### The unbased extended fundamental theorem of identity types
diff --git a/src/foundation/strong-preunivalence.lagda.md b/src/foundation/strong-preunivalence.lagda.md
index 051e55fa52..0ef3c70f97 100644
--- a/src/foundation/strong-preunivalence.lagda.md
+++ b/src/foundation/strong-preunivalence.lagda.md
@@ -8,9 +8,12 @@ module foundation.strong-preunivalence where
 
 ```agda
 open import foundation.contractible-types
+open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
 open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
 open import foundation.preunivalence
 open import foundation.propositional-maps
 open import foundation.propositions
@@ -82,8 +85,8 @@ based-preunivalence-instance-strong-preunivalence :
   instance-strong-preunivalence l X → based-preunivalence-axiom X
 based-preunivalence-instance-strong-preunivalence X L Y =
   is-emb-is-prop-map
-    ( backward-implication-subuniverse-equality-duality
-      ( is-prop-Prop)
+    ( backward-implication-structured-equality-duality
+      ( is-prop-equiv')
       ( L)
       ( X)
       ( λ _ → equiv-eq)
@@ -138,6 +141,26 @@ strong-preunivalence : strong-preunivalence-axiom
 strong-preunivalence = strong-preunivalence-axiom-univalence-axiom univalence
 ```
 
+### The preunivalence axiom implies the strong preunivalence axiom
+
+This argument is due to [Evan Cavallo](https://ecavallo.net/). Note that it
+depends on the function extensionality axiom in order to compute the equality
+type of `is-small`.
+
+```agda
+strong-preunivalence-axiom-preunivalence-axiom-Level :
+  {l1 l2 : Level} →
+  preunivalence-axiom-Level l1 → strong-preunivalence-axiom-Level l2 l1
+strong-preunivalence-axiom-preunivalence-axiom-Level pua X (Y , α) (Y' , α') =
+  is-prop-equiv
+    ( compute-eq-is-small (Y , α) (Y' , α'))
+    ( is-prop-map-is-emb (pua Y Y') (α' ∘e inv-equiv α))
+```
+
+See
+[`UF.PreUnivalence`](https://martinescardo.github.io/TypeTopology/UF.PreUnivalence.html)
+at TypeTopology for Cavallo's original formalizations.
+
 ## See also
 
 - [Strongly preunivalent categories](category-theory.strongly-preunivalent-categories.md)
diff --git a/src/foundation/structured-equality-duality.lagda.md b/src/foundation/structured-equality-duality.lagda.md
index 534bf63cd7..be2d518ded 100644
--- a/src/foundation/structured-equality-duality.lagda.md
+++ b/src/foundation/structured-equality-duality.lagda.md
@@ -101,6 +101,9 @@ logically equivalent:
 ```agda
 module _
   {l1 l2 l3 : Level} (𝒫 : subuniverse (l1 ⊔ l2) l3)
+  (tr-𝒫 :
+    {X Y : UU (l1 ⊔ l2)} →
+    X ≃ Y → is-in-subuniverse 𝒫 X → is-in-subuniverse 𝒫 Y)
   {A : UU l1} {B : A → UU l2}
   where
 
@@ -109,23 +112,21 @@ module _
       (y : A) → is-in-subuniverse-map 𝒫 (f y)) →
     is-separated 𝒫 (Σ A B)
   forward-implication-subuniverse-equality-duality =
-    forward-implication-structured-equality-duality
-      ( is-in-subuniverse-equiv 𝒫)
+    forward-implication-structured-equality-duality tr-𝒫
 
   backward-implication-subuniverse-equality-duality :
     is-separated 𝒫 (Σ A B) →
     ( (x : A) (f : (y : A) → (x ＝ y) → B y)
       (y : A) → is-in-subuniverse-map 𝒫 (f y))
   backward-implication-subuniverse-equality-duality =
-    backward-implication-structured-equality-duality
-      ( is-in-subuniverse-equiv 𝒫)
+    backward-implication-structured-equality-duality tr-𝒫
 
   subuniverse-equality-duality :
     ( (x : A) (f : (y : A) → (x ＝ y) → B y)
       (y : A) → is-in-subuniverse-map 𝒫 (f y)) ↔
     is-separated 𝒫 (Σ A B)
   subuniverse-equality-duality =
-    structured-equality-duality (is-in-subuniverse-equiv 𝒫)
+    structured-equality-duality tr-𝒫
 ```
 
 ## See also
diff --git a/src/foundation/transposition-identifications-along-equivalences.lagda.md b/src/foundation/transposition-identifications-along-equivalences.lagda.md
index ef7e0b1cc7..8c97737465 100644
--- a/src/foundation/transposition-identifications-along-equivalences.lagda.md
+++ b/src/foundation/transposition-identifications-along-equivalences.lagda.md
@@ -26,15 +26,15 @@ open import foundation-core.homotopies
 Consider an [equivalence](foundation-core.equivalences.md) `e : A ≃ B` and two
 elements `x : A` and `y : B`. The
 {{#concept "transposition" Disambiguation="identifications along equivalences" Agda=eq-transpose-equiv}}
-is an equivalence
+is an equivalence of [identity types](foundation-core.identity-types.md)
 
 ```text
-  (e x ＝ y) ≃ (x ＝ e⁻¹ y)
+  (e x ＝ y) ≃ (x ＝ e⁻¹ y).
 ```
 
-of [identity types](foundation-core.identity-types.md). There are two ways of
-constructing this equivalence. One way uses the fact that `e⁻¹` is a
-[section](foundation-core.sections.md) of `e`, from which it follows that
+There are two ways of constructing this equivalence. One way uses the fact that
+`e⁻¹` is a [section](foundation-core.sections.md) of `e`, from which it follows
+that
 
 ```text
  (e x ＝ y) ≃ (e x ＝ e e⁻¹ y) ≃ (x ＝ e⁻¹ y).
diff --git a/src/foundation/transposition-identifications-along-retractions.lagda.md b/src/foundation/transposition-identifications-along-retractions.lagda.md
index 2dfe11e3cb..155d68d491 100644
--- a/src/foundation/transposition-identifications-along-retractions.lagda.md
+++ b/src/foundation/transposition-identifications-along-retractions.lagda.md
@@ -27,7 +27,7 @@ Consider a map `f : A → B` and a map `g : B → A` in the converse direction.
 there is an [equivalence](foundation-core.equivalences.md)
 
 ```text
-  is-retraction f g ≃ ((x : A) (y : B) → (f x ＝ y) ≃ (x ＝ g y))
+  is-retraction f g ≃ ((x : A) (y : B) → (f x ＝ y) → (x ＝ g y))
 ```
 
 In other words, any [retracting homotopy](foundation-core.retractions.md)
@@ -56,7 +56,7 @@ module _
 
   eq-transpose-is-retraction' :
     is-retraction f g → {x : A} {y : B} → f x ＝ y → x ＝ g y
-  eq-transpose-is-retraction' H {x} refl = inv (H x)
+  eq-transpose-is-retraction' H {x} p = inv (H x) ∙ ap g p
 ```
 
 ## Properties
diff --git a/src/foundation/transposition-identifications-along-sections.lagda.md b/src/foundation/transposition-identifications-along-sections.lagda.md
index 9cffc6452a..e9ded579d2 100644
--- a/src/foundation/transposition-identifications-along-sections.lagda.md
+++ b/src/foundation/transposition-identifications-along-sections.lagda.md
@@ -27,7 +27,7 @@ Consider a map `f : A → B` and a map `g : B → A` in the converse direction.
 there is an [equivalence](foundation-core.equivalences.md)
 
 ```text
-  is-section f g ≃ ((x : A) (y : B) → (x ＝ g y) ≃ (f x ＝ y))
+  is-section f g ≃ ((x : A) (y : B) → (x ＝ g y) → (f x ＝ y))
 ```
 
 In other words, any [section homotopy](foundation-core.sections.md) `f ∘ g ~ id`
@@ -54,7 +54,7 @@ module _
 
   eq-transpose-is-section' :
     f ∘ g ~ id → {x : B} {y : A} → g x ＝ y → x ＝ f y
-  eq-transpose-is-section' H {x} refl = inv (H x)
+  eq-transpose-is-section' H {x} p = inv (H x) ∙ ap f p
 ```
 
 ## Properties