diff --git a/references.bib b/references.bib
index 2c7232900e..938394ca2d 100644
--- a/references.bib
+++ b/references.bib
@@ -304,6 +304,16 @@ @article{Esc08
   primaryclass = {cs.LO}
 }
 
+@online{Esc17YetAnother,
+  title        = {Yet another characterization of univalence},
+  author       = {Escardó, Martín Hötzel},
+  date         = {2017-11-18},
+  year         = {2017},
+  month        = {11},
+  url          = {https://groups.google.com/g/homotopytypetheory/c/FfiZj1vrkmQ/m/GJETdy0AAgAJ},
+  howpublished = {{{Google}} groups forum discussion}
+}
+
 @online{Esc19DefinitionsEquivalence,
   title        = {Definitions of Equivalence Satisfying Judgmental/Strict Groupoid Laws?},
   author       = {Escardó, Martín Hötzel},
diff --git a/src/category-theory/categories.lagda.md b/src/category-theory/categories.lagda.md
index 810689aba3..81114b2cc7 100644
--- a/src/category-theory/categories.lagda.md
+++ b/src/category-theory/categories.lagda.md
@@ -17,6 +17,7 @@ open import foundation.1-types
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
+open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.propositions
@@ -170,8 +171,11 @@ module _
 
   is-preunivalent-category-Category :
     is-preunivalent-Precategory (precategory-Category C)
-  is-preunivalent-category-Category x y =
-    is-emb-is-equiv (is-category-Category C x y)
+  is-preunivalent-category-Category x =
+    is-set-is-contr
+      ( fundamental-theorem-id'
+        ( iso-eq-Precategory (precategory-Category C) x)
+        ( is-category-Category C x))
 
   preunivalent-category-Category : Preunivalent-Category l1 l2
   pr1 preunivalent-category-Category = precategory-Category C
@@ -301,7 +305,7 @@ module _
     is-surjective-iso-eq-C x y =
     is-equiv-is-emb-is-surjective
       ( is-surjective-iso-eq-C x y)
-      ( is-preunivalent-Preunivalent-Category C x y)
+      ( preunivalence-Preunivalent-Category C x y)
 
   is-surjective-iso-eq-is-category-Preunivalent-Category :
     is-category-Precategory (precategory-Preunivalent-Category C) →
diff --git a/src/category-theory/indiscrete-precategories.lagda.md b/src/category-theory/indiscrete-precategories.lagda.md
index 68479adbd5..02f42fb044 100644
--- a/src/category-theory/indiscrete-precategories.lagda.md
+++ b/src/category-theory/indiscrete-precategories.lagda.md
@@ -212,7 +212,11 @@ module _
   is-strict-category-is-preunivalent-indiscrete-Precategory H x y =
     is-prop-is-emb
       ( iso-eq-Precategory (indiscrete-Precategory X) x y)
-      ( H x y)
+      ( preunivalence-is-preunivalent-Precategory
+        ( indiscrete-Precategory X)
+        ( H)
+        ( x)
+        ( y))
       ( is-prop-Σ
         ( is-prop-unit)
         ( is-prop-is-iso-Precategory (indiscrete-Precategory X) {x} {y}))
diff --git a/src/category-theory/opposite-preunivalent-categories.lagda.md b/src/category-theory/opposite-preunivalent-categories.lagda.md
index 4ea17ae265..2819a2d057 100644
--- a/src/category-theory/opposite-preunivalent-categories.lagda.md
+++ b/src/category-theory/opposite-preunivalent-categories.lagda.md
@@ -15,6 +15,7 @@ open import category-theory.preunivalent-categories
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
+open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.involutions
 open import foundation.sets
@@ -41,17 +42,13 @@ abstract
     {l1 l2 : Level} (C : Precategory l1 l2) →
     is-preunivalent-Precategory C →
     is-preunivalent-Precategory (opposite-Precategory C)
-  is-preunivalent-opposite-is-preunivalent-Precategory C is-preunivalent-C x y =
-    is-emb-htpy-emb
-      ( comp-emb
-        ( emb-equiv
-          ( compute-iso-opposite-Precategory C ∘e equiv-inv-iso-Precategory C))
-        ( _ , is-preunivalent-C x y))
-      ( λ where
-        refl →
-          eq-type-subtype
-            ( is-iso-prop-Precategory (opposite-Precategory C))
-            ( refl))
+  is-preunivalent-opposite-is-preunivalent-Precategory C is-preunivalent-C x =
+    is-set-equiv'
+      ( Σ (obj-opposite-Precategory C) (iso-Precategory C x))
+      ( equiv-tot
+        ( λ _ →
+          compute-iso-opposite-Precategory C ∘e equiv-inv-iso-Precategory C))
+      ( is-preunivalent-C x)
 
 abstract
   is-preunivalent-is-preunivalent-opposite-Precategory :
diff --git a/src/category-theory/preunivalent-categories.lagda.md b/src/category-theory/preunivalent-categories.lagda.md
index 9f593f0cbe..0b283e3c0b 100644
--- a/src/category-theory/preunivalent-categories.lagda.md
+++ b/src/category-theory/preunivalent-categories.lagda.md
@@ -15,10 +15,13 @@ open import foundation.1-types
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.embeddings
+open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
+open import foundation.propositional-maps
 open import foundation.propositions
 open import foundation.sets
 open import foundation.strictly-involutive-identity-types
+open import foundation.structured-equality-duality
 open import foundation.universe-levels
 ```
 
@@ -26,34 +29,32 @@ open import foundation.universe-levels
 
 ## Idea
 
-A **preunivalent category** is a [precategory](category-theory.precategories.md)
-for which the [identifications](foundation-core.identity-types.md) between the
-objects [embed](foundation-core.embeddings.md) into the
-[isomorphisms](category-theory.isomorphisms-in-precategories.md). More
-specifically, an equality between objects gives rise to an isomorphism between
-them, by the J-rule. A precategory is a preunivalent category if this function,
-called `iso-eq`, is an embedding.
-
-The idea of [preunivalence](foundation.preunivalence.md) is that it is a common
-generalization of univalent mathematics and mathematics with Axiom K. Hence
-preunivalent categories generalize both
-[(univalent) categories](category-theory.categories.md) and
+A {{#concept "preunivalent category" Agda=Preunivalent-Category}} `𝒞` is a
+[precategory](category-theory.precategories.md) for which every mapping of the
+concrete groupoid of objects into the groupoid of
+[isomorphisms](category-theory.isomorphisms-in-precategories.md) is an
+[embedding](foundation-core.embeddings.md). Equivalently, by
+[subuniverse equality duality](foundation.structured-equality-duality.md), a
+preunivalent category is a precategory whose based isomorphism types
+`Σ (x : 𝒞₀), (* ≅ x)` are [sets](foundation-core.sets.md).
+
+The main function of _preunivalence_ is to serve as a common generalization of
+univalent mathematics and mathematics with Axiom K by restricting the ways that
+identity and equivalence may interact. Hence preunivalent categories generalize
+both [(univalent) categories](category-theory.categories.md) and
 [strict categories](category-theory.strict-categories.md), which are
-precategories whose objects form a [set](foundation-core.sets.md).
-
-The preunivalence condition on precategories states that the type of objects is
-a subgroupoid of the [groupoid](category-theory.groupoids.md) of isomorphisms.
-For univalent categories the groupoid of objects is equivalent to the groupoid
-of isomorphisms, while for strict categories the groupoid of objects is
-discrete. Indeed, in this sense preunivalence provides a generalization of both
-notions of "category", with _no more structure_. This is opposed to the even
-more general notion of precategory, where the homotopy structure on the objects
-can be almost completely unrelated to the homotopy structure of the morphisms.
+precategories whose objects form a [set](foundation-core.sets.md). Note,
+however, that our definition of preunivalence here is a
+[strengthening](foundation.strong-preunivalence.md) of the
+[preunivalence axiom](foundation.preunivalence.md).
 
 ## Definitions
 
 ### The predicate on precategories of being a preunivalent category
 
+We define preunivalence of a precategory `𝒞` to be the condition that for every
+`x : 𝒞₀`, the type `Σ (y : 𝒞₀), (x ≅ y)` is a set.
+
 ```agda
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
@@ -64,12 +65,25 @@ module _
     Π-Prop
       ( obj-Precategory C)
       ( λ x →
-        Π-Prop
-          ( obj-Precategory C)
-          ( λ y → is-emb-Prop (iso-eq-Precategory C x y)))
+        is-set-Prop
+          ( Σ ( obj-Precategory C)
+              ( iso-Precategory C x)))
 
   is-preunivalent-Precategory : UU (l1 ⊔ l2)
   is-preunivalent-Precategory = type-Prop is-preunivalent-prop-Precategory
+
+  preunivalence-is-preunivalent-Precategory :
+    is-preunivalent-Precategory →
+    (x y : obj-Precategory C) →
+    is-emb (iso-eq-Precategory C x y)
+  preunivalence-is-preunivalent-Precategory H x y =
+    is-emb-is-prop-map
+      ( backward-implication-subuniverse-equality-duality
+        ( is-prop-Prop)
+        (H x)
+        ( x)
+        ( iso-eq-Precategory C x)
+        ( y))
 ```
 
 ### The type of preunivalent categories
@@ -168,13 +182,44 @@ module _
     is-preunivalent-Precategory precategory-Preunivalent-Category
   is-preunivalent-Preunivalent-Category = pr2 C
 
+  iso-Preunivalent-Category : (x y : obj-Preunivalent-Category) → UU l2
+  iso-Preunivalent-Category = iso-Precategory precategory-Preunivalent-Category
+
+  iso-eq-Preunivalent-Category :
+    (x y : obj-Preunivalent-Category) → x ＝ y → iso-Preunivalent-Category x y
+  iso-eq-Preunivalent-Category =
+    iso-eq-Precategory precategory-Preunivalent-Category
+
+  preunivalence-Preunivalent-Category :
+    (x y : obj-Preunivalent-Category) →
+    is-emb (iso-eq-Preunivalent-Category x y)
+  preunivalence-Preunivalent-Category =
+    preunivalence-is-preunivalent-Precategory
+      ( precategory-Preunivalent-Category)
+      ( is-preunivalent-Preunivalent-Category)
+
   emb-iso-eq-Preunivalent-Category :
     {x y : obj-Preunivalent-Category} →
     (x ＝ y) ↪ (iso-Precategory precategory-Preunivalent-Category x y)
-  pr1 (emb-iso-eq-Preunivalent-Category {x} {y}) =
-    iso-eq-Precategory precategory-Preunivalent-Category x y
-  pr2 (emb-iso-eq-Preunivalent-Category {x} {y}) =
-    is-preunivalent-Preunivalent-Category x y
+  emb-iso-eq-Preunivalent-Category {x} {y} =
+    ( iso-eq-Precategory precategory-Preunivalent-Category x y ,
+      preunivalence-Preunivalent-Category x y)
+```
+
+### The right-based isomorphism types of a preunivalent category are also sets
+
+```agda
+is-preunivalent-Preunivalent-Category' :
+  {l1 l2 : Level} (C : Preunivalent-Category l1 l2) →
+  ( x : obj-Preunivalent-Category C) →
+  is-set
+    ( Σ (obj-Preunivalent-Category C) (λ y → iso-Preunivalent-Category C y x))
+is-preunivalent-Preunivalent-Category' C x =
+  is-set-equiv
+    ( Σ (obj-Preunivalent-Category C) (iso-Preunivalent-Category C x))
+    ( equiv-tot
+      ( λ y → equiv-inv-iso-Precategory (precategory-Preunivalent-Category C)))
+    ( is-preunivalent-Preunivalent-Category C x)
 ```
 
 ### The total hom-type of a preunivalent category
@@ -255,7 +300,7 @@ module _
   is-1-type-obj-Preunivalent-Category x y =
     is-set-is-emb
       ( iso-eq-Precategory (precategory-Preunivalent-Category C) x y)
-      ( is-preunivalent-Preunivalent-Category C x y)
+      ( preunivalence-Preunivalent-Category C x y)
       ( is-set-iso-Precategory (precategory-Preunivalent-Category C))
 
   obj-1-type-Preunivalent-Category : 1-Type l1
diff --git a/src/category-theory/strict-categories.lagda.md b/src/category-theory/strict-categories.lagda.md
index d26990c1f5..66a81cdc1c 100644
--- a/src/category-theory/strict-categories.lagda.md
+++ b/src/category-theory/strict-categories.lagda.md
@@ -192,12 +192,10 @@ module _
   abstract
     is-preunivalent-Strict-Category :
       is-preunivalent-Precategory (precategory-Strict-Category C)
-    is-preunivalent-Strict-Category x y =
-      is-emb-is-injective
-        ( is-set-type-subtype
-          ( is-iso-prop-Precategory (precategory-Strict-Category C))
-          ( is-set-hom-Strict-Category C x y))
-        ( λ _ → eq-is-prop (is-set-obj-Strict-Category C x y))
+    is-preunivalent-Strict-Category x =
+      is-set-Σ
+        ( is-set-obj-Strict-Category C)
+        ( λ y → is-set-iso-Precategory (precategory-Strict-Category C) {x} {y})
 
   preunivalent-category-Strict-Category : Preunivalent-Category l1 l2
   pr1 preunivalent-category-Strict-Category = precategory-Strict-Category C
diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md
index 9dacb2ce72..bcc2650afd 100644
--- a/src/foundation-core/equality-dependent-pair-types.lagda.md
+++ b/src/foundation-core/equality-dependent-pair-types.lagda.md
@@ -168,6 +168,17 @@ module _
   ap-pr1-eq-pair-Σ refl refl = refl
 ```
 
+### Transport in `B` along the first projection of an identification in `Σ A B`
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  tr-eq-Σ : {x y : Σ A B} (p : x ＝ y) → tr B (ap pr1 p) (pr2 x) ＝ pr2 y
+  tr-eq-Σ refl = refl
+```
+
 ## See also
 
 - Equality proofs in cartesian product types are characterized in
diff --git a/src/foundation-core/injective-maps.lagda.md b/src/foundation-core/injective-maps.lagda.md
index bf6bc84c72..72003be269 100644
--- a/src/foundation-core/injective-maps.lagda.md
+++ b/src/foundation-core/injective-maps.lagda.md
@@ -90,6 +90,9 @@ module _
     is-injective h → is-injective g → is-injective (g ∘ h)
   is-injective-comp is-inj-h is-inj-g = is-inj-h ∘ is-inj-g
 
+  comp-injection : injection B C → injection A B → injection A C
+  comp-injection (g , G) (h , H) = (g ∘ h , is-injective-comp H G)
+
   is-injective-left-map-triangle :
     (f : A → C) (g : B → C) (h : A → B) → f ~ (g ∘ h) →
     is-injective h → is-injective g → is-injective f
@@ -111,6 +114,9 @@ module _
   is-injective-equiv : (e : A ≃ B) → is-injective (map-equiv e)
   is-injective-equiv e = is-injective-is-equiv (is-equiv-map-equiv e)
 
+  injection-equiv : A ≃ B → injection A B
+  injection-equiv e = (map-equiv e , is-injective-equiv e)
+
 abstract
   is-injective-map-inv-equiv :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 4e72fe1c04..1f6f173430 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -392,9 +392,11 @@ open import foundation.standard-ternary-pullbacks public
 open import foundation.strict-symmetrization-binary-relations public
 open import foundation.strictly-involutive-identity-types public
 open import foundation.strictly-right-unital-concatenation-identifications public
+open import foundation.strong-preunivalence public
 open import foundation.strongly-extensional-maps public
 open import foundation.structure public
 open import foundation.structure-identity-principle public
+open import foundation.structured-equality-duality public
 open import foundation.structured-type-duality public
 open import foundation.subsingleton-induction public
 open import foundation.subterminal-types public
diff --git a/src/foundation/functoriality-dependent-function-types.lagda.md b/src/foundation/functoriality-dependent-function-types.lagda.md
index 5993ac6c2a..9fc8e6c98c 100644
--- a/src/foundation/functoriality-dependent-function-types.lagda.md
+++ b/src/foundation/functoriality-dependent-function-types.lagda.md
@@ -121,7 +121,7 @@ id-map-equiv-Π B h = eq-htpy (compute-map-equiv-Π B id-equiv (λ _ → id-equi
 
 ```agda
 module _
-  { l1 l2 l3 : Level} {A : UU l1}
+  {l1 l2 l3 : Level} {A : UU l1}
   where
 
   equiv-htpy-map-Π-fam-equiv :
@@ -133,35 +133,32 @@ module _
       ( λ a → equiv-ap (e a) (f a) (g a))
 ```
 
-### Truncated families of maps induce truncated maps on dependent function types
+### Families of truncated maps induce truncated maps on dependent function types
 
 ```agda
-abstract
-  is-trunc-map-map-Π :
-    (k : 𝕋) {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-    (f : (i : I) → A i → B i) →
-    ((i : I) → is-trunc-map k (f i)) → is-trunc-map k (map-Π f)
-  is-trunc-map-map-Π k {I = I} f H h =
-    is-trunc-equiv' k
-      ( (i : I) → fiber (f i) (h i))
-      ( compute-fiber-map-Π f h)
-      ( is-trunc-Π k (λ i → H i (h i)))
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
+  where
 
-abstract
-  is-emb-map-Π :
-    {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-    {f : (i : I) → A i → B i} →
-    ((i : I) → is-emb (f i)) → is-emb (map-Π f)
-  is-emb-map-Π {f = f} H =
-    is-emb-is-prop-map
-      ( is-trunc-map-map-Π neg-one-𝕋 f
-        ( λ i → is-prop-map-is-emb (H i)))
-
-emb-Π :
-  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3} →
-  ((i : I) → A i ↪ B i) → ((i : I) → A i) ↪ ((i : I) → B i)
-pr1 (emb-Π f) = map-Π (λ i → map-emb (f i))
-pr2 (emb-Π f) = is-emb-map-Π (λ i → is-emb-map-emb (f i))
+  abstract
+    is-trunc-map-map-Π :
+      (k : 𝕋) (f : (i : I) → A i → B i) →
+      ((i : I) → is-trunc-map k (f i)) → is-trunc-map k (map-Π f)
+    is-trunc-map-map-Π k f H h =
+      is-trunc-equiv' k
+        ( (i : I) → fiber (f i) (h i))
+        ( compute-fiber-map-Π f h)
+        ( is-trunc-Π k (λ i → H i (h i)))
+
+  abstract
+    is-emb-map-Π :
+      {f : (i : I) → A i → B i} → ((i : I) → is-emb (f i)) → is-emb (map-Π f)
+    is-emb-map-Π {f} H =
+      is-emb-is-prop-map
+        ( is-trunc-map-map-Π neg-one-𝕋 f (λ i → is-prop-map-is-emb (H i)))
+
+  emb-Π : ((i : I) → A i ↪ B i) → ((i : I) → A i) ↪ ((i : I) → B i)
+  emb-Π f = (map-Π (map-emb ∘ f) , is-emb-map-Π (is-emb-map-emb ∘ f))
 ```
 
 ### A family of truncated maps over any map induces a truncated map on dependent function types
diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md
index 8bbd6bea4c..2f517ddffe 100644
--- a/src/foundation/identity-types.lagda.md
+++ b/src/foundation/identity-types.lagda.md
@@ -318,21 +318,21 @@ module _
 
 ### Computation of fibers of families of maps out of the identity type
 
-We show that `fiber (f x) y ≃ ((* , f * refl) ＝ (x , y))` for every `x : A` and
-`y : B x`.
+Given a map `f : (x : A) → (* ＝ x) → B x`, we show that
+`fiber (f x) y ≃ ((* , f * refl) ＝ (x , y))` for every `x : A` and `y : B x`.
 
 ```agda
 module _
   {l1 l2 : Level} {A : UU l1} {a : A} {B : A → UU l2}
-  (f : (x : A) → (a ＝ x) → B x) (x : A) (y : B x)
+  (f : (x : A) → (a ＝ x) → B x) (x : A) (x' : B x)
   where
 
   map-compute-fiber-map-out-of-identity-type :
-    fiber (f x) y → ((a , f a refl) ＝ (x , y))
+    fiber (f x) x' → ((a , f a refl) ＝ (x , x'))
   map-compute-fiber-map-out-of-identity-type (refl , refl) = refl
 
   map-inv-compute-fiber-map-out-of-identity-type :
-    ((a , f a refl) ＝ (x , y)) → fiber (f x) y
+    ((a , f a refl) ＝ (x , x')) → fiber (f x) x'
   map-inv-compute-fiber-map-out-of-identity-type refl =
     refl , refl
 
@@ -355,10 +355,42 @@ module _
       is-section-map-inv-compute-fiber-map-out-of-identity-type
       is-retraction-map-inv-compute-fiber-map-out-of-identity-type
 
+  is-equiv-map-inv-compute-fiber-map-out-of-identity-type :
+    is-equiv map-inv-compute-fiber-map-out-of-identity-type
+  is-equiv-map-inv-compute-fiber-map-out-of-identity-type =
+    is-equiv-is-invertible
+      map-compute-fiber-map-out-of-identity-type
+      is-retraction-map-inv-compute-fiber-map-out-of-identity-type
+      is-section-map-inv-compute-fiber-map-out-of-identity-type
+
   compute-fiber-map-out-of-identity-type :
-    fiber (f x) y ≃ ((a , f a refl) ＝ (x , y))
-  pr1 compute-fiber-map-out-of-identity-type =
-    map-compute-fiber-map-out-of-identity-type
-  pr2 compute-fiber-map-out-of-identity-type =
-    is-equiv-map-compute-fiber-map-out-of-identity-type
+    fiber (f x) x' ≃ ((a , f a refl) ＝ (x , x'))
+  compute-fiber-map-out-of-identity-type =
+    ( map-compute-fiber-map-out-of-identity-type ,
+      is-equiv-map-compute-fiber-map-out-of-identity-type)
+
+  inv-compute-fiber-map-out-of-identity-type :
+    ((a , f a refl) ＝ (x , x')) ≃ fiber (f x) x'
+  inv-compute-fiber-map-out-of-identity-type =
+    ( map-inv-compute-fiber-map-out-of-identity-type ,
+      is-equiv-map-inv-compute-fiber-map-out-of-identity-type)
+```
+
+### Computation of fibers of families of unbased maps out of the identity type
+
+Given a map `f : (x y : A) → (x ＝ y) → B x y`, we show that
+`fiber (f x y) b ≃ ((x , f x x refl) ＝ (y , b))` for every `x y : A` and
+`b : B x y`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → A → UU l2}
+  (f : (x y : A) → x ＝ y → B x y)
+  where
+
+  compute-fiber-unbased-map-out-of-identity-type :
+    (x y : A) (b : B x y) →
+    fiber (f x y) b ≃ ((x , f x x refl) ＝ (y , b))
+  compute-fiber-unbased-map-out-of-identity-type x =
+    compute-fiber-map-out-of-identity-type (f x)
 ```
diff --git a/src/foundation/injective-maps.lagda.md b/src/foundation/injective-maps.lagda.md
index 8114a8e0f3..8ab3913353 100644
--- a/src/foundation/injective-maps.lagda.md
+++ b/src/foundation/injective-maps.lagda.md
@@ -9,12 +9,18 @@ open import foundation-core.injective-maps public
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-dependent-functions
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.function-extensionality
 open import foundation.logical-equivalences
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.embeddings
 open import foundation-core.empty-types
+open import foundation-core.equality-dependent-pair-types
+open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.identity-types
 open import foundation-core.negation
@@ -102,15 +108,51 @@ module _
     is-set A → (f : A → B) → is-prop (is-injective f)
   is-prop-is-injective H f =
     is-prop-implicit-Π
-      ( λ x →
-        is-prop-implicit-Π
-          ( λ y → is-prop-function-type (H x y)))
+      ( λ x → is-prop-implicit-Π (λ y → is-prop-function-type (H x y)))
 
   is-injective-Prop : is-set A → (A → B) → Prop (l1 ⊔ l2)
   pr1 (is-injective-Prop H f) = is-injective f
   pr2 (is-injective-Prop H f) = is-prop-is-injective H f
 ```
 
+### The map on total spaces induced by a family of injective maps is an injective map
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
+  where
+  is-injective-tot :
+    {f : (x : A) → B x → C x} →
+    ((x : A) → is-injective (f x)) →
+    is-injective (tot f)
+  is-injective-tot {f} H {x} {y} p =
+    eq-pair-Σ
+      ( ap pr1 p)
+      ( H (pr1 y) (preserves-tr f (ap pr1 p) (pr2 x) ∙ tr-eq-Σ p))
+
+  injection-tot : ((x : A) → injection (B x) (C x)) → injection (Σ A B) (Σ A C)
+  injection-tot f = (tot (pr1 ∘ f) , is-injective-tot (pr2 ∘ f))
+```
+
+### Families of injective maps induce injective maps on dependent function types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
+  where
+
+  abstract
+    is-injective-map-Π :
+      {f : (i : I) → A i → B i} →
+      ((i : I) → is-injective (f i)) → is-injective (map-Π f)
+    is-injective-map-Π {f = f} H {x} {y} p = eq-htpy (λ i → H i (htpy-eq p i))
+
+  injection-Π :
+    ((i : I) → injection (A i) (B i)) →
+    injection ((i : I) → A i) ((i : I) → B i)
+  injection-Π f = (map-Π (pr1 ∘ f) , is-injective-map-Π (pr2 ∘ f))
+```
+
 ## See also
 
 - [Embeddings](foundation-core.embeddings.md)
diff --git a/src/foundation/maps-in-subuniverses.lagda.md b/src/foundation/maps-in-subuniverses.lagda.md
index 54aab010e1..52c43cb7cc 100644
--- a/src/foundation/maps-in-subuniverses.lagda.md
+++ b/src/foundation/maps-in-subuniverses.lagda.md
@@ -7,6 +7,7 @@ module foundation.maps-in-subuniverses where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.homotopies
 open import foundation.subuniverses
 open import foundation.universe-levels
 
@@ -33,6 +34,22 @@ is-in-subuniverse-map :
 is-in-subuniverse-map P {A} {B} f = (b : B) → is-in-subuniverse P (fiber f b)
 ```
 
+## Properties
+
+### Subuniverses are closed under homotopies of maps
+
+```agda
+module _
+  {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) {A : UU l1} {B : UU l2}
+  {f g : A → B}
+  where
+
+  is-in-subuniverse-map-htpy :
+    f ~ g → is-in-subuniverse-map P f → is-in-subuniverse-map P g
+  is-in-subuniverse-map-htpy H F y =
+    is-in-subuniverse-equiv' P (equiv-fiber-htpy H y) (F y)
+```
+
 ## See also
 
 - [Maps in global subuniverses](foundation.maps-in-global-subuniverses.md)
diff --git a/src/foundation/preunivalence.lagda.md b/src/foundation/preunivalence.lagda.md
index 298f482891..9fe3c4409c 100644
--- a/src/foundation/preunivalence.lagda.md
+++ b/src/foundation/preunivalence.lagda.md
@@ -107,5 +107,6 @@ preunivalence = preunivalence-axiom-univalence-axiom univalence
 - Preunivalence is sufficient to prove that `Id : A → (A → 𝒰)` is an embedding.
   This fact is proven in
   [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md)
+- [The strong preunivalence axiom](foundation.strong-preunivalence.md)
 - [Preunivalent type families](foundation.preunivalent-type-families.md)
 - [Preunivalent categories](category-theory.preunivalent-categories.md)
diff --git a/src/foundation/preunivalent-type-families.lagda.md b/src/foundation/preunivalent-type-families.lagda.md
index 96fb37312b..933a182ad5 100644
--- a/src/foundation/preunivalent-type-families.lagda.md
+++ b/src/foundation/preunivalent-type-families.lagda.md
@@ -39,7 +39,12 @@ the map
   equiv-tr B : x ＝ y → B x ≃ B y
 ```
 
-is an [embedding](foundation-core.embeddings.md) for every `x y : A`.
+is an [embedding](foundation-core.embeddings.md) for every `x y : A`. By
+[the preunivalence axiom](foundation.preunivalence.md), which follows from
+[the univalence axiom](foundation.univalence.md), the type family `B` is
+preunivalent if and only if it is [faithful](foundation.faithful-maps.md) as a
+map. In other words, if `A` is a [set](foundation-core.sets.md)-level
+[structure](foundation.structure.md) on types.
 
 ## Definition
 
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 14db96e387..5381fa28bb 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
@@ -25,8 +25,10 @@ open import foundation.identity-types
 open import foundation.inhabited-types
 open import foundation.logical-equivalences
 open import foundation.maps-in-subuniverses
+open import foundation.mere-equality
 open import foundation.propositional-truncations
 open import foundation.separated-types-subuniverses
+open import foundation.structured-equality-duality
 open import foundation.subuniverses
 open import foundation.surjective-maps
 open import foundation.truncated-maps
@@ -39,7 +41,8 @@ open import foundation.universe-levels
 
 ## Idea
 
-The **Regensburg extension** of the
+The {{#concept "Regensburg extension" Agda=extended-fundamental-theorem-id}} of
+the
 [fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md)
 asserts that for any [subuniverse](foundation.subuniverses.md) `P`, and any
 [pointed](structured-types.pointed-types.md)
@@ -82,48 +85,87 @@ agda-unimath.
 
 ## Theorem
 
+### The extended fundamental theorem of identity types
+
 ```agda
 module _
-  {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3)
+  {l1 l2 l3 : Level} (𝒫 : subuniverse (l1 ⊔ l2) l3)
   {A : UU l1} (a : A) {B : A → UU l2}
   where
 
   abstract
     forward-implication-extended-fundamental-theorem-id :
       is-0-connected A →
-      ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map P (f x)) →
-      is-separated P (Σ A B)
-    forward-implication-extended-fundamental-theorem-id H K (x , y) (x' , y') =
-      apply-universal-property-trunc-Prop
-        ( mere-eq-is-0-connected H a x)
-        ( P _)
-        ( λ where
-          refl →
-            is-in-subuniverse-equiv P
-              ( compute-fiber-map-out-of-identity-type
-                ( ind-Id a (λ u v → B u) y)
-                ( x')
-                ( y'))
-              ( K (ind-Id a (λ u v → B u) y) x' y'))
+      ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map 𝒫 (f x)) →
+      is-separated 𝒫 (Σ A B)
+    forward-implication-extended-fundamental-theorem-id H K =
+      forward-implication-subuniverse-equality-duality 𝒫
+        ( λ x f y b →
+          apply-universal-property-trunc-Prop
+            ( mere-eq-is-0-connected H a x)
+            ( 𝒫 (fiber (f y) b))
+            ( λ where refl → K f y b))
 
   abstract
     backward-implication-extended-fundamental-theorem-id :
-      is-separated P (Σ A B) →
-      (f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map P (f x)
-    backward-implication-extended-fundamental-theorem-id K f x y =
-      is-in-subuniverse-equiv' P
-        ( compute-fiber-map-out-of-identity-type f x y)
-        ( K (a , f a refl) (x , y))
+      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
 
-  abstract
-    extended-fundamental-theorem-id :
-      is-0-connected A →
-      ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map P (f x)) ↔
-      is-separated P (Σ A B)
-    pr1 (extended-fundamental-theorem-id H) =
-      forward-implication-extended-fundamental-theorem-id H
-    pr2 (extended-fundamental-theorem-id H) =
-      backward-implication-extended-fundamental-theorem-id
+  extended-fundamental-theorem-id :
+    is-0-connected A →
+    ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map 𝒫 (f x)) ↔
+    is-separated 𝒫 (Σ A B)
+  extended-fundamental-theorem-id H =
+    ( forward-implication-extended-fundamental-theorem-id H ,
+    backward-implication-extended-fundamental-theorem-id)
+```
+
+### The unbased extended fundamental theorem of identity types
+
+We give a similar characterization for a binary family of types `B : A → A → 𝒰`
+over a not necessarily pointed or inhabited type `A` whose elements are all
+merely equal. In other words, `A` is any π₀-trivial type. The characterization
+asserts that the following are equivalent:
+
+1. For every `x : A` and every family of maps out of the identity types
+   `f : (y : A) → (x ＝ y) → B x y`, then for every `y : A` the `f y` is a
+   `𝒫`-map.
+2. For every `x : A` the type `Σ A (B x)` is `𝒫`-separated.
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒫 : subuniverse (l1 ⊔ l2) l3)
+  {A : UU l1} {B : A → A → UU l2}
+  where
+
+  forward-implication-extended-fundamental-theorem-unbased-id :
+    ( (x y : A) → mere-eq x y) →
+    ( (x : A) (f : (y : A) → (x ＝ y) → B x y)
+      (y : A) → is-in-subuniverse-map 𝒫 (f y)) →
+    ( (x : A) → is-separated 𝒫 (Σ A (B x)))
+  forward-implication-extended-fundamental-theorem-unbased-id H K x =
+    forward-implication-extended-fundamental-theorem-id 𝒫
+      ( x)
+      ( is-0-connected-mere-eq x (H x))
+      ( K x)
+
+  backward-implication-extended-fundamental-theorem-unbased-id :
+    ( (x : A) → is-separated 𝒫 (Σ A (B x))) →
+    ( (x : A) (f : (y : A) → (x ＝ y) → B x y)
+      (y : A) → is-in-subuniverse-map 𝒫 (f y))
+  backward-implication-extended-fundamental-theorem-unbased-id K x =
+    backward-implication-extended-fundamental-theorem-id 𝒫 x (K x)
+
+  extended-fundamental-theorem-unbased-id :
+    ( (x y : A) → mere-eq x y) →
+    ( (x : A) (f : (y : A) → (x ＝ y) → B x y)
+      (y : A) → is-in-subuniverse-map 𝒫 (f y)) ↔
+    ( (x : A) → is-separated 𝒫 (Σ A (B x)))
+  extended-fundamental-theorem-unbased-id H =
+    ( forward-implication-extended-fundamental-theorem-unbased-id H ,
+      backward-implication-extended-fundamental-theorem-unbased-id)
 ```
 
 ## Corollaries
diff --git a/src/foundation/strong-preunivalence.lagda.md b/src/foundation/strong-preunivalence.lagda.md
new file mode 100644
index 0000000000..ac56a91a6a
--- /dev/null
+++ b/src/foundation/strong-preunivalence.lagda.md
@@ -0,0 +1,142 @@
+# The strong preunivalence axiom
+
+```agda
+module foundation.strong-preunivalence where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.functoriality-dependent-pair-types
+open import foundation.preunivalence
+open import foundation.propositional-maps
+open import foundation.propositions
+open import foundation.sets
+open import foundation.small-types
+open import foundation.structured-equality-duality
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+{{#concept "The strong preunivalence axiom" Agda=strong-preunivalence-axiom}} is
+a common generalization of the [univalence axiom](foundation.univalence.md) and
+[axiom K](foundation-core.sets.md). It asserts that for any type `X : 𝒰` and any
+other universe `𝒱`, the [smallness predicate](foundation-core.small-types.md)
+`is-small 𝒱 X ≐ Σ (Y : 𝒱), (X ≃ Y)` is a [set](foundation-core.sets.md).
+
+The strong preunivalence axiom is a strengthening of
+[the preunivalence axiom](foundation.preunivalence.md) in the following way. If
+we restrict to `𝒱 ≐ 𝒰`,
+[subuniverse equality duality](foundation.structured-equality-duality.md) says
+that `Σ (Y : 𝒰), (X ≃ Y)` is a set if and only if every binary family of maps
+
+```text
+  (Z Y : 𝒰) → (Z ＝ Y) → (X ≃ Y)
+```
+
+is a binary family of [embeddings](foundation-core.embeddings.md). The
+preunivalence axiom asserts that the particular family of maps
+`(Y : 𝒰) → (X ＝ Y) → (X ≃ Y)` defined by identity induction as
+`refl ↦ id-equiv` is a family of embeddings.
+
+While the strong preunivalence axiom is a strengthening of the preunivalence
+axiom, it is still a common generalization of the
+[univalence axiom](foundation.univalence.md) and
+[axiom K](foundation-core.sets.md): if we assume the univalence axiom then
+`is-small 𝒱 X` is a proposition, and if we assume axiom K then every type is a
+set.
+
+## Definitions
+
+```agda
+instance-strong-preunivalence :
+  {l1 : Level} (l2 : Level) (X : UU l1) → UU (l1 ⊔ lsuc l2)
+instance-strong-preunivalence l2 X = is-set (is-small l2 X)
+
+strong-preunivalence-axiom-Level : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+strong-preunivalence-axiom-Level l1 l2 =
+  (X : UU l1) → instance-strong-preunivalence l2 X
+
+strong-preunivalence-axiom : UUω
+strong-preunivalence-axiom =
+  {l1 l2 : Level} → strong-preunivalence-axiom-Level l1 l2
+```
+
+## Properties
+
+### The strong preunivalence axiom strengthens the preunivalence axiom
+
+```agda
+based-preunivalence-instance-strong-preunivalence :
+  {l : Level} (X : UU l) →
+  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)
+      ( L)
+      ( X)
+      ( λ _ → equiv-eq)
+      ( Y))
+
+preunivalence-axiom-strong-preunivalence-axiom :
+  strong-preunivalence-axiom → preunivalence-axiom
+preunivalence-axiom-strong-preunivalence-axiom L X =
+  based-preunivalence-instance-strong-preunivalence X (L X)
+```
+
+### The strong preunivalence axiom generalizes axiom K
+
+To show that preunivalence generalizes axiom K, we assume axiom K for types of
+equivalences and for the universe itself.
+
+```agda
+instance-strong-preunivalence-instance-axiom-K :
+  {l1 : Level} (l2 : Level) (A : UU l1) →
+  instance-axiom-K (UU l2) →
+  ((B : UU l2) → instance-axiom-K (A ≃ B)) →
+  instance-strong-preunivalence l2 A
+instance-strong-preunivalence-instance-axiom-K l2 A K-Type K-A≃B =
+  is-set-Σ (is-set-axiom-K K-Type) (is-set-axiom-K ∘ K-A≃B)
+
+strong-preunivalence-axiom-axiom-K : axiom-K → strong-preunivalence-axiom
+strong-preunivalence-axiom-axiom-K K {l1} {l2} A =
+  instance-strong-preunivalence-instance-axiom-K l2 A
+    ( K (UU l2))
+    ( λ B → K (A ≃ B))
+```
+
+### The strong preunivalence axiom generalizes the univalence axiom
+
+```agda
+strong-preunivalence-axiom-univalence-axiom :
+  univalence-axiom → strong-preunivalence-axiom
+strong-preunivalence-axiom-univalence-axiom UA {l1} {l2} A =
+  is-set-is-prop
+  ( is-prop-is-proof-irrelevant
+    ( λ (X , e) →
+      is-contr-equiv'
+        ( is-small l2 X)
+        ( equiv-tot (equiv-precomp-equiv e))
+        ( is-torsorial-equiv-based-univalence X (UA X))))
+```
+
+### Strong preunivalence holds in univalent foundations
+
+```agda
+strong-preunivalence : strong-preunivalence-axiom
+strong-preunivalence = strong-preunivalence-axiom-univalence-axiom univalence
+```
+
+## See also
+
+- [Preunivalent categories](category-theory.preunivalent-categories.md)
diff --git a/src/foundation/structure.lagda.md b/src/foundation/structure.lagda.md
index 0aa7762c1e..6a5b9217b7 100644
--- a/src/foundation/structure.lagda.md
+++ b/src/foundation/structure.lagda.md
@@ -21,40 +21,46 @@ open import foundation-core.transport-along-identifications
 
 ## Idea
 
-Given a type family `P` on the universe, a **`P`-structured type** consists of a
-type `A` equipped with an element of type `P A`.
+Given a type family `𝒫` on the universe, a {{#concept "`𝒫`-structured type"}}
+consists of a type `A` _equipped_ with an element of type `𝒫 A`.
 
-## Definition
+## Definitions
 
 ```agda
-structure : {l1 l2 : Level} (P : UU l1 → UU l2) → UU (lsuc l1 ⊔ l2)
-structure {l1} P = Σ (UU l1) P
+structure : {l1 l2 : Level} (𝒫 : UU l1 → UU l2) → UU (lsuc l1 ⊔ l2)
+structure {l1} 𝒫 = Σ (UU l1) 𝒫
 
 fam-structure :
-  {l1 l2 l3 : Level} (P : UU l1 → UU l2) (A : UU l3) → UU (lsuc l1 ⊔ l2 ⊔ l3)
-fam-structure P A = A → structure P
+  {l1 l2 l3 : Level} (𝒫 : UU l1 → UU l2) (A : UU l3) → UU (lsuc l1 ⊔ l2 ⊔ l3)
+fam-structure 𝒫 A = A → structure 𝒫
 
 structure-map :
-  {l1 l2 l3 : Level} (P : UU (l1 ⊔ l2) → UU l3) {A : UU l1} {B : UU l2}
+  {l1 l2 l3 : Level} (𝒫 : UU (l1 ⊔ l2) → UU l3) {A : UU l1} {B : UU l2}
   (f : A → B) → UU (l2 ⊔ l3)
-structure-map P {A} {B} f = (b : B) → P (fiber f b)
+structure-map 𝒫 {A} {B} f = (b : B) → 𝒫 (fiber f b)
 
 hom-structure :
-  {l1 l2 l3 : Level} (P : UU (l1 ⊔ l2) → UU l3) →
+  {l1 l2 l3 : Level} (𝒫 : UU (l1 ⊔ l2) → UU l3) →
   UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ l3)
-hom-structure P A B = Σ (A → B) (structure-map P)
+hom-structure 𝒫 A B = Σ (A → B) (structure-map 𝒫)
+
+structure-equality :
+  {l1 l2 : Level} (𝒫 : UU l1 → UU l2) → UU l1 → UU (l1 ⊔ l2)
+structure-equality 𝒫 A = (x y : A) → 𝒫 (x ＝ y)
 ```
 
 ## Properties
 
 ### Having structure is closed under equivalences
 
+This is a consequence of [the univalence axiom](foundation.univalence.md)
+
 ```agda
 has-structure-equiv :
-  {l1 l2 : Level} (P : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → P X → P Y
-has-structure-equiv P e = tr P (eq-equiv e)
+  {l1 l2 : Level} (𝒫 : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → 𝒫 X → 𝒫 Y
+has-structure-equiv 𝒫 e = tr 𝒫 (eq-equiv e)
 
 has-structure-equiv' :
-  {l1 l2 : Level} (P : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → P Y → P X
-has-structure-equiv' P e = tr P (inv (eq-equiv e))
+  {l1 l2 : Level} (𝒫 : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → 𝒫 Y → 𝒫 X
+has-structure-equiv' 𝒫 e = tr 𝒫 (inv (eq-equiv e))
 ```
diff --git a/src/foundation/structured-equality-duality.lagda.md b/src/foundation/structured-equality-duality.lagda.md
new file mode 100644
index 0000000000..463afb643d
--- /dev/null
+++ b/src/foundation/structured-equality-duality.lagda.md
@@ -0,0 +1,131 @@
+# Structured equality duality
+
+```agda
+module foundation.structured-equality-duality where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.maps-in-subuniverses
+open import foundation.separated-types-subuniverses
+open import foundation.structure
+open import foundation.subuniverses
+open import foundation.universe-levels
+
+open import foundation-core.equivalences
+```
+
+</details>
+
+## Idea
+
+Given a [structure](foundation.structure.md) `𝒫` on types that transfers along
+[equivalences](foundation-core.equivalences.md) in the sense that `𝒫` comes
+equipped with a family of maps
+
+```text
+  {X Y : 𝒰} → (X ≃ Y) → 𝒫 X → 𝒫 Y,
+```
+
+then for every type `A` and type family `B : A → 𝒰` there is a
+[mutual correspondence](foundation.logical-equivalences.md) between the
+following:
+
+1. `𝒫`-structured families of maps `f : (y : A) → (x ＝ y) → B y` for every
+   `x : A`.
+2. `𝒫`-structures on the equality of `Σ A B`.
+
+We refer to this as
+{{#concept "structured equality duality" Agda=structured-equality-duality}}.
+
+**Note.** by [the univalence axiom](foundation.univalence.md), every structure
+[transfers along equivalences](foundation.transport-along-equivalences.md).
+However, we maintain this as an assumption, since for most common notions of
+structure this property is independent of the univalence axiom.
+
+## Duality
+
+### Structured equality duality
+
+```agda
+module _
+  {l1 l2 l3 : Level} {𝒫 : UU (l1 ⊔ l2) → UU l3}
+  (tr-𝒫 : {X Y : UU (l1 ⊔ l2)} → X ≃ Y → 𝒫 X → 𝒫 Y)
+  {A : UU l1} {B : A → UU l2}
+  where
+
+  forward-implication-structured-equality-duality :
+    ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) →
+    structure-equality 𝒫 (Σ A B)
+  forward-implication-structured-equality-duality
+    K (x , b) (x' , b') =
+    tr-𝒫
+      ( compute-fiber-map-out-of-identity-type (ind-Id x (λ u _ → B u) b) x' b')
+      ( K x (ind-Id x (λ u _ → B u) b) x' b')
+
+  backward-implication-structured-equality-duality :
+    structure-equality 𝒫 (Σ A B) →
+    ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y))
+  backward-implication-structured-equality-duality K x f y b =
+    tr-𝒫
+      ( inv-compute-fiber-map-out-of-identity-type f y b)
+      ( K (x , f x refl) (y , b))
+
+  structured-equality-duality :
+    ( (x : A) (f : (y : A) → (x ＝ y) → B y) (y : A) → structure-map 𝒫 (f y)) ↔
+    ( structure-equality 𝒫 (Σ A B))
+  structured-equality-duality =
+    ( forward-implication-structured-equality-duality ,
+      backward-implication-structured-equality-duality)
+```
+
+### Subuniverse equality duality
+
+Given a [subuniverse](foundation.subuniverses.md) `𝒫` then the following are
+logically equivalent:
+
+1. For every `x : A`, every family of maps `f : (y : A) → (x ＝ y) → B y` is a
+   family of `𝒫`-maps.
+2. The dependent sum `Σ A B` is `𝒫`-separated.
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒫 : subuniverse (l1 ⊔ l2) l3)
+  {A : UU l1} {B : A → UU l2}
+  where
+
+  forward-implication-subuniverse-equality-duality :
+    ( (x : A) (f : (y : A) → (x ＝ y) → B y)
+      (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 𝒫)
+
+  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 𝒫)
+
+  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 𝒫)
+```
+
+## See also
+
+This duality is applied in
+
+- [The Regensburg extension of the fundamental theorem of identity types](foundation.regensburg-extension-fundamental-theorem-of-identity-types.md)
+- [The strong preunivalence axiom](foundation.strong-preunivalence.md)
+- [Preunivalent categories](category-theory.preunivalent-categories.md)
diff --git a/src/foundation/univalent-type-families.lagda.md b/src/foundation/univalent-type-families.lagda.md
index 129dfaf7be..9a7c109a9a 100644
--- a/src/foundation/univalent-type-families.lagda.md
+++ b/src/foundation/univalent-type-families.lagda.md
@@ -43,7 +43,8 @@ map
 is an [equivalence](foundation-core.equivalences.md) for every `x y : A`. By
 [the univalence axiom](foundation-core.univalence.md), this is equivalent to the
 type family `B` being an [embedding](foundation-core.embeddings.md) considered
-as a map.
+as a map. In other words, that `A` is a
+[subuniverse](foundation.subuniverses.md).
 
 ## Definition
 
diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md
index 678401d075..1412af1bae 100644
--- a/src/foundation/universal-property-identity-types.lagda.md
+++ b/src/foundation/universal-property-identity-types.lagda.md
@@ -17,6 +17,7 @@ open import foundation.function-extensionality
 open import foundation.functoriality-dependent-function-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
+open import foundation.injective-maps
 open import foundation.preunivalence
 open import foundation.univalence
 open import foundation.universe-levels
@@ -28,7 +29,6 @@ open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
-open import foundation-core.injective-maps
 open import foundation-core.propositional-maps
 open import foundation-core.propositions
 open import foundation-core.torsorial-type-families
@@ -38,9 +38,10 @@ open import foundation-core.torsorial-type-families
 
 ## Idea
 
-The **universal property of identity types** characterizes families of maps out
-of the [identity type](foundation-core.identity-types.md). This universal
-property is also known as the **type theoretic Yoneda lemma**.
+The {{#concept "universal property of identity types" Agda=equiv-ev-refl}}
+characterizes families of maps out of the
+[identity type](foundation-core.identity-types.md). This universal property is
+also known as the **type theoretic Yoneda lemma**.
 
 ## Theorem
 
@@ -113,73 +114,117 @@ module _
 
 ### `Id : A → (A → 𝒰)` is an embedding
 
-We first show that [the preunivalence axiom](foundation.preunivalence.md)
-implies that the map `Id : A → (A → 𝒰)` is an
-[embedding](foundation.embeddings.md). Since the
-[univalence axiom](foundation.univalence.md) implies preunivalence, it follows
-that `Id : A → (A → 𝒰)` is an embedding under the postulates of agda-unimath.
+We first show that [injectivity](foundation-core.injective-maps.md) of the map
 
-#### Preunivalence implies that `Id : A → (A → 𝒰)` is an embedding
+```text
+  equiv-eq : {X Y : 𝒰} → (X ＝ Y) → (X ≃ Y)
+```
+
+for the identity types of `A` implies that the map `Id : A → (A → 𝒰)` is an
+[embedding](foundation.embeddings.md), a result due to Martín Escardó
+{{#cite TypeTopology}}. Since the [univalence axiom](foundation.univalence.md)
+implies [the preunivalence axiom](foundation.preunivalence.md) implies
+injectivity of `equiv-eq`, it follows that `Id : A → (A → 𝒰)` is an embedding
+under the postulates of agda-unimath.
+
+#### Injectivity of `equiv-eq` implies `Id : A → (A → 𝒰)` is an embedding
 
-The proof that preunivalence implies that `Id : A → (A → 𝒰)` is an embedding
-proceeds via the
+The proof that injectivity of `equiv-eq` implies that `Id : A → (A → 𝒰)` is an
+embedding proceeds via the
 [fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md)
 by showing that the [fiber](foundation.fibers-of-maps.md) of `Id` at `Id a` is
 [contractible](foundation.contractible-types.md) for each `a : A`. To see this,
 we first note that this fiber has an element `(a , refl)`. Therefore it suffices
 to show that this fiber is a proposition. We do this by constructing an
-embedding
+injection
 
 ```text
-  fiber Id (Id a) ↪ Σ A (Id a).
+  fiber Id (Id a) ↣ Σ A (Id a).
 ```
 
-Since the codomain of this embedding is contractible, the claim follows. The
-above embedding is constructed as the composite of the following embeddings
+Since the codomain of this injection is contractible, the claim follows. The
+above injection is constructed as the following composite injection
 
 ```text
-  Σ (x : A), Id x ＝ Id a
-    ↪ Σ (x : A), (y : A) → (x ＝ y) ＝ (a ＝ y)
-    ↪ Σ (x : A), (y : A) → (x ＝ y) ≃ (a ＝ y)
-    ↪ Σ (x : A), Σ (e : (y : A) → (x ＝ y) → (a ＝ y)), (y : A) → is-equiv (e y)
-    ↪ Σ (x : A), (y : A) → (x ＝ y) → (a ＝ y)
-    ↪ Σ (x : A), a ＝ x.
+  Σ (x : A), Id a ＝ Id x
+  ≃ Σ (x : A), Id x ＝ Id a
+  ≃ Σ (x : A), ((y : A) → (x ＝ y) ＝ (a ＝ y))
+  ↣ Σ (x : A), ((y : A) → (x ＝ y) ≃ (a ＝ y))
+  ≃ Σ (x : A), ((y : A) → (x ＝ y) → (a ＝ y))
+  ≃ Σ (x : A), a ＝ x.
 ```
 
-In this composite, we used preunivalence at the second step.
+In this composite, the injectivity of `equiv-eq` is used in the third step.
 
 ```agda
 module _
   {l : Level} (A : UU l)
-  (L : (a x y : A) → instance-preunivalence (Id x y) (Id a y))
+  (L : (a x y : A) → is-injective (equiv-eq {A = Id x y} {B = Id a y}))
   where
 
-  emb-fiber-Id-preunivalent-Id :
-    (a : A) → fiber' Id (Id a) ↪ Σ A (Id a)
-  emb-fiber-Id-preunivalent-Id a =
-    comp-emb
-      ( comp-emb
-        ( emb-equiv
-          ( equiv-tot
-            ( λ x →
-              ( equiv-ev-refl x) ∘e
-              ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a)))))
-        ( emb-tot
-          ( λ x →
-            comp-emb
-              ( emb-Π (λ y → _ , L a x y))
-              ( emb-equiv equiv-funext))))
-      ( emb-equiv (inv-equiv (equiv-fiber Id (Id a))))
-
-  is-emb-Id-preunivalent-Id : is-emb (Id {A = A})
-  is-emb-Id-preunivalent-Id a =
+  injection-Id-is-injective-equiv-eq-Id :
+    (a x : A) → injection (Id a ＝ Id x) (a ＝ x)
+  injection-Id-is-injective-equiv-eq-Id a x =
+    comp-injection
+      ( injection-equiv
+        ( ( equiv-ev-refl x) ∘e
+          ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a))))
+      ( comp-injection
+        ( injection-Π (λ y → _ , L a x y))
+        ( injection-equiv (equiv-funext ∘e equiv-inv (Id a) (Id x))))
+
+  injection-fiber-Id-is-injective-equiv-eq-Id :
+    (a : A) → injection (fiber' Id (Id a)) (Σ A (Id a))
+  injection-fiber-Id-is-injective-equiv-eq-Id a =
+    injection-tot (injection-Id-is-injective-equiv-eq-Id a)
+
+  is-emb-Id-is-injective-equiv-eq-Id : is-emb (Id {A = A})
+  is-emb-Id-is-injective-equiv-eq-Id a =
     fundamental-theorem-id
       ( ( a , refl) ,
         ( λ _ →
-          is-injective-emb
-            ( emb-fiber-Id-preunivalent-Id a)
+          pr2
+            ( injection-fiber-Id-is-injective-equiv-eq-Id a)
             ( eq-is-contr (is-torsorial-Id a))))
       ( λ _ → ap Id)
+```
+
+#### Preunivalence implies that `Id : A → (A → 𝒰)` is an embedding
+
+Assuming preunivalence, then in particular `equiv-eq` is injective and so the
+previous argument applies. However, in this case we do get a slightly stronger
+result, since now the fiber inclusion
+
+```text
+  fiber Id (Id a) → Σ A (Id a)
+```
+
+is a proper embedding.
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  (L : (a x y : A) → instance-preunivalence (Id x y) (Id a y))
+  where
+
+  emb-Id-is-injective-equiv-eq-Id : (a x : A) → (Id a ＝ Id x) ↪ (a ＝ x)
+  emb-Id-is-injective-equiv-eq-Id a x =
+    comp-emb
+      ( emb-equiv
+        ( ( equiv-ev-refl x) ∘e
+          ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a))))
+      ( comp-emb
+        ( emb-Π (λ y → _ , L a x y))
+        ( emb-equiv (equiv-funext ∘e equiv-inv (Id a) (Id x))))
+
+  emb-fiber-Id-preunivalent-Id : (a : A) → fiber' Id (Id a) ↪ Σ A (Id a)
+  emb-fiber-Id-preunivalent-Id a =
+    emb-tot (emb-Id-is-injective-equiv-eq-Id a)
+
+  is-emb-Id-preunivalent-Id : is-emb (Id {A = A})
+  is-emb-Id-preunivalent-Id =
+    is-emb-Id-is-injective-equiv-eq-Id A
+      ( λ a x y → is-injective-is-emb (L a x y))
 
 module _
   (L : preunivalence-axiom) {l : Level} (A : UU l)
@@ -187,18 +232,31 @@ module _
 
   is-emb-Id-preunivalence-axiom : is-emb (Id {A = A})
   is-emb-Id-preunivalence-axiom =
-    is-emb-Id-preunivalent-Id A (λ a x y → L (Id x y) (Id a y))
+    is-emb-Id-is-injective-equiv-eq-Id A
+      ( λ a x y → is-injective-is-emb (L (Id x y) (Id a y)))
 ```
 
 #### `Id : A → (A → 𝒰)` is an embedding
 
 ```agda
-module _
-  {l : Level} (A : UU l)
-  where
+is-emb-Id : {l : Level} (A : UU l) → is-emb (Id {A = A})
+is-emb-Id = is-emb-Id-preunivalence-axiom preunivalence
+```
 
-  is-emb-Id : is-emb (Id {A = A})
-  is-emb-Id = is-emb-Id-preunivalence-axiom preunivalence A
+### Characteriation of equality of `Id`
+
+```agda
+equiv-Id :
+  {l : Level} {A : UU l} (a x : A) → (Id a ＝ Id x) ≃ (a ＝ x)
+equiv-Id a x =
+  ( equiv-ev-refl x) ∘e
+  ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a)) ∘e
+  ( equiv-Π-equiv-family (λ _ → equiv-univalence)) ∘e
+  ( equiv-funext) ∘e
+  ( equiv-inv (Id a) (Id x))
+
+equiv-fiber-Id : {l : Level} {A : UU l} (a : A) → fiber' Id (Id a) ≃ Σ A (Id a)
+equiv-fiber-Id a = equiv-tot (equiv-Id a)
 ```
 
 #### For any type family `B` over `A`, the type of pairs `(a , e)` consisting of `a : A` and a family of equivalences `e : (x : A) → (a ＝ x) ≃ B x` is a proposition
@@ -248,15 +306,12 @@ module _
 
   abstract
     is-torsorial-pointed-fam-equiv-is-torsorial :
-      is-torsorial
-        ( λ (e : (x : A) → (a ＝ x) ≃ B x) →
-          map-equiv (e a) refl ＝ b)
+      is-torsorial (λ (e : (x : A) → (a ＝ x) ≃ B x) → map-equiv (e a) refl ＝ b)
     is-torsorial-pointed-fam-equiv-is-torsorial =
       is-contr-equiv'
-        ( fiber (ev-refl a {B = λ x _ → B x}) b)
+        ( fiber (ev-refl a) b)
         ( equiv-Σ _
-          ( inv-equiv
-            ( equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B))
+          ( inv-equiv (equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B))
           ( λ h →
             equiv-inv-concat
               ( inv
@@ -266,23 +321,23 @@ module _
                     ( equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B)
                     ( h))))
               ( b)))
-        ( is-contr-map-is-equiv
-          ( is-equiv-ev-refl a)
-          ( b))
+        ( is-contr-map-is-equiv (is-equiv-ev-refl a) b)
 ```
 
 ## See also
 
 - In
   [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md)
-  we will show that the fiber of `Id : A → (A → 𝒰)` at `B : A → 𝒰` is equivalent
-  to `is-torsorial B`.
+  we show that the fiber of `Id : A → (A → 𝒰)` at `B : A → 𝒰` is equivalent to
+  `is-torsorial B`.
 
 ## References
 
-- The fact that preunivalence, or axiom L, is sufficient to prove that
-  `Id : A → (A → 𝒰)` is an embedding was first observed and formalized by Martín
-  Escardó,
-  [https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html](https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html).
+It was first observed and proved by Evan Cavallo that preunivalence, or Axiom L,
+is sufficient to deduce that `Id : A → (A → 𝒰)` is an embedding. It was later
+observed and formalized by Martín Escardó that assuming the map
+`equiv-eq : (X ＝ Y) → (X ≃ Y)` is injective is enough. {{#cite TypeTopology}}
+Martín Escardó's formalizations can be found here:
+[https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html](https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html).
 
-{{#bibliography}} {{#reference TypeTopology}}
+{{#bibliography}} {{#reference TypeTopology}} {{#reference Esc17YetAnother}}
diff --git a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
index 51dfe0ed13..b2397aee3c 100644
--- a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
+++ b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
@@ -167,14 +167,14 @@ module _
 Given a map `a : I → A`, and a homotopy `H : f ~ g`, where `f, g : J → I`, we
 know that there is an identification `a ∘ f ＝ a ∘ g`. Transporting along this
 identification in the type of lifts of families of elements into a type family
-`B : A → 𝓤`, we get a map
+`B : A → 𝒰`, we get a map
 
 ```text
   ((j : J) → B (a (f j))) → ((j : J) → B (a (g j))) .
 ```
 
 We show that this map is homotopic to transporting along `H` in the type family
-`B ∘ a : I → 𝓤`.
+`B ∘ a : I → 𝒰`.
 
 ```agda
 module _
diff --git a/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md
index c197c952bc..8b53882043 100644
--- a/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md
+++ b/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md
@@ -33,7 +33,7 @@ open import orthogonal-factorization-systems.lifts-families-of-elements
 
 ## Idea
 
-Consider a type family `B : A → 𝓤` and a map `a : I → A`. Then, given a map
+Consider a type family `B : A → 𝒰` and a map `a : I → A`. Then, given a map
 `f : J → I`, we may pull back a
 [lift](orthogonal-factorization-systems.lifts-families-of-elements.md) of `a` to
 a lift of `a ∘ f`.
diff --git a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
index d7951a5d85..552c91b146 100644
--- a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
@@ -45,7 +45,7 @@ given a coequalizer
      f
 ```
 
-with homotopy `H : e ∘ f ~ e ∘ g`, and a type family `P : X → 𝓤` over `X`, the
+with homotopy `H : e ∘ f ~ e ∘ g`, and a type family `P : X → 𝒰` over `X`, the
 cofork
 
 ```text