diff --git a/src/foundation-core/contractible-maps.lagda.md b/src/foundation-core/contractible-maps.lagda.md
index 4016cecbd3..46a3cecce5 100644
--- a/src/foundation-core/contractible-maps.lagda.md
+++ b/src/foundation-core/contractible-maps.lagda.md
@@ -129,8 +129,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of path-split maps see
   [`foundation.path-split-maps`](foundation.path-split-maps.md).
diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md
index 4fdf05534e..2010a4a555 100644
--- a/src/foundation-core/equivalences.lagda.md
+++ b/src/foundation-core/equivalences.lagda.md
@@ -749,8 +749,8 @@ syntax step-equivalence-reasoning e Z f = e ≃ Z by f
 
 ## See also
 
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).
diff --git a/src/foundation-core/path-split-maps.lagda.md b/src/foundation-core/path-split-maps.lagda.md
index 66ae437fa4..c2b94a4453 100644
--- a/src/foundation-core/path-split-maps.lagda.md
+++ b/src/foundation-core/path-split-maps.lagda.md
@@ -24,9 +24,9 @@ open import foundation-core.sections
 ## Idea
 
 A map `f : A → B` is said to be **path split** if it has a
-[section](foundation-core.sections.md) and its action on
-[identity types](foundation-core.identity-types.md) `Id x y → Id (f x) (f y)`
-has a section for each `x y : A`. By the
+[section](foundation-core.sections.md) and its
+[action on identifications](foundation.action-on-identifications-functions.md)
+`x ＝ y → f x ＝ f y` has a section for each `x y : A`. By the
 [fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md),
 it follows that a map is path-split if and only if it is an
 [equivalence](foundation-core.equivalences.md).
@@ -80,8 +80,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).
diff --git a/src/foundation-core/sets.lagda.md b/src/foundation-core/sets.lagda.md
index cecd9e33de..603e8413ec 100644
--- a/src/foundation-core/sets.lagda.md
+++ b/src/foundation-core/sets.lagda.md
@@ -147,4 +147,22 @@ abstract
     {l1 l2 : Level} (A : UU l1) {B : UU l2} (e : A ≃ B) →
     is-set A → is-set B
   is-set-equiv' = is-trunc-equiv' zero-𝕋
+
+abstract
+  is-set-equiv-is-set :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+    is-set A → is-set B → is-set (A ≃ B)
+  is-set-equiv-is-set = is-trunc-equiv-is-trunc zero-𝕋
+
+module _
+  {l1 l2 : Level} (A : Set l1) (B : Set l2)
+  where
+
+  equiv-Set : UU (l1 ⊔ l2)
+  equiv-Set = type-Set A ≃ type-Set B
+
+  equiv-set-Set : Set (l1 ⊔ l2)
+  pr1 equiv-set-Set = equiv-Set
+  pr2 equiv-set-Set =
+    is-set-equiv-is-set (is-set-type-Set A) (is-set-type-Set B)
 ```
diff --git a/src/foundation-core/transport-along-identifications.lagda.md b/src/foundation-core/transport-along-identifications.lagda.md
index 67ef4e293d..968011e96f 100644
--- a/src/foundation-core/transport-along-identifications.lagda.md
+++ b/src/foundation-core/transport-along-identifications.lagda.md
@@ -110,7 +110,7 @@ module _
 ```agda
 tr-Id-left :
   {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : b ＝ a) →
-  tr (_＝ a) q p ＝ ((inv q) ∙ p)
+  tr (_＝ a) q p ＝ (inv q ∙ p)
 tr-Id-left refl p = refl
 ```
 
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 1adc44d8a8..1badf21b0d 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -270,6 +270,7 @@ open import foundation.precomposition-type-families public
 open import foundation.preidempotent-maps public
 open import foundation.preimages-of-subtypes public
 open import foundation.preunivalence public
+open import foundation.preunivalent-type-families public
 open import foundation.principle-of-omniscience public
 open import foundation.product-decompositions public
 open import foundation.product-decompositions-subuniverse public
@@ -352,6 +353,7 @@ open import foundation.transport-along-equivalences public
 open import foundation.transport-along-higher-identifications public
 open import foundation.transport-along-homotopies public
 open import foundation.transport-along-identifications public
+open import foundation.transport-split-type-families public
 open import foundation.transposition-span-diagrams public
 open import foundation.trivial-relaxed-sigma-decompositions public
 open import foundation.trivial-sigma-decompositions public
diff --git a/src/foundation/category-of-sets.lagda.md b/src/foundation/category-of-sets.lagda.md
index be56947a17..803e007a6a 100644
--- a/src/foundation/category-of-sets.lagda.md
+++ b/src/foundation/category-of-sets.lagda.md
@@ -68,7 +68,7 @@ is-large-category-Set-Large-Precategory :
 is-large-category-Set-Large-Precategory {l} X =
   fundamental-theorem-id
     ( is-contr-equiv'
-      ( Σ (Set l) (type-equiv-Set X))
+      ( Σ (Set l) (equiv-Set X))
       ( equiv-tot (equiv-iso-equiv-Set X))
       ( is-torsorial-equiv-Set X))
     ( iso-eq-Set X)
diff --git a/src/foundation/contractible-maps.lagda.md b/src/foundation/contractible-maps.lagda.md
index df0d7ac4bc..15c5bb6786 100644
--- a/src/foundation/contractible-maps.lagda.md
+++ b/src/foundation/contractible-maps.lagda.md
@@ -133,8 +133,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of path-split maps see
   [`foundation.path-split-maps`](foundation.path-split-maps.md).
diff --git a/src/foundation/embeddings.lagda.md b/src/foundation/embeddings.lagda.md
index d231edfd31..8a4e18fbe5 100644
--- a/src/foundation/embeddings.lagda.md
+++ b/src/foundation/embeddings.lagda.md
@@ -322,9 +322,9 @@ module _
 
   abstract
     is-emb-section-ap :
-      ((x y : A) → section (ap f {x = x} {y = y})) → is-emb f
-    is-emb-section-ap section-ap-f x y =
-      fundamental-theorem-id-section x (λ y → ap f {y = y}) (section-ap-f x) y
+      ((x y : A) → section (ap f {x} {y})) → is-emb f
+    is-emb-section-ap section-ap-f x =
+      fundamental-theorem-id-section x (λ y → ap f) (section-ap-f x)
 ```
 
 ### If there is an equivalence `(f x = f y) ≃ (x = y)` that sends `refl` to `refl`, then f is an embedding
diff --git a/src/foundation/equivalences-maybe.lagda.md b/src/foundation/equivalences-maybe.lagda.md
index 5a38bc210b..47f52136b4 100644
--- a/src/foundation/equivalences-maybe.lagda.md
+++ b/src/foundation/equivalences-maybe.lagda.md
@@ -380,6 +380,11 @@ equiv-equiv-Maybe :
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} → (Maybe X ≃ Maybe Y) → (X ≃ Y)
 pr1 (equiv-equiv-Maybe e) = map-equiv-equiv-Maybe e
 pr2 (equiv-equiv-Maybe e) = is-equiv-map-equiv-equiv-Maybe e
+
+compute-equiv-equiv-Maybe-id-equiv :
+  {l1 : Level} {X : UU l1} →
+  equiv-equiv-Maybe id-equiv ＝ id-equiv {A = X}
+compute-equiv-equiv-Maybe-id-equiv = eq-htpy-equiv refl-htpy
 ```
 
 ### For any set `X`, the type of automorphisms on `X` is equivalent to the type of automorphisms on `Maybe X` that fix the exception
diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md
index e3e695b440..59256d5b1e 100644
--- a/src/foundation/equivalences.lagda.md
+++ b/src/foundation/equivalences.lagda.md
@@ -805,8 +805,8 @@ module _
 
 ## See also
 
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).
diff --git a/src/foundation/fundamental-theorem-of-identity-types.lagda.md b/src/foundation/fundamental-theorem-of-identity-types.lagda.md
index 5090cca6f8..57fa70fa94 100644
--- a/src/foundation/fundamental-theorem-of-identity-types.lagda.md
+++ b/src/foundation/fundamental-theorem-of-identity-types.lagda.md
@@ -8,11 +8,13 @@ module foundation.fundamental-theorem-of-identity-types where
 
 ```agda
 open import foundation.dependent-pair-types
+open import foundation.retracts-of-types
 open import foundation.universe-levels
 
 open import foundation-core.contractible-types
 open import foundation-core.equivalences
 open import foundation-core.families-of-equivalences
+open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
@@ -87,7 +89,7 @@ module _
 
   abstract
     fundamental-theorem-id-J' :
-      (is-fiberwise-equiv (ind-Id a (λ x p → B x) b)) → is-torsorial B
+      is-fiberwise-equiv (ind-Id a (λ x p → B x) b) → is-torsorial B
     fundamental-theorem-id-J' H =
       is-contr-is-equiv'
         ( Σ A (Id a))
@@ -105,18 +107,29 @@ module _
 
   abstract
     fundamental-theorem-id-retraction :
-      (i : (x : A) → B x → a ＝ x) → (R : (x : A) → retraction (i x)) →
+      (i : (x : A) → B x → a ＝ x) →
+      ((x : A) → retraction (i x)) →
       is-fiberwise-equiv i
     fundamental-theorem-id-retraction i R =
       is-fiberwise-equiv-is-equiv-tot
         ( is-equiv-is-contr (tot i)
-          ( is-contr-retract-of (Σ _ (λ y → a ＝ y))
-            ( pair (tot i)
-              ( pair (tot λ x → pr1 (R x))
-                ( ( inv-htpy (preserves-comp-tot i (λ x → pr1 (R x)))) ∙h
-                  ( ( tot-htpy λ x → pr2 (R x)) ∙h (tot-id B)))))
+          ( is-contr-retract-of
+            ( Σ _ (λ y → a ＝ y))
+            ( ( tot i) ,
+              ( tot (λ x → pr1 (R x))) ,
+              ( ( inv-htpy (preserves-comp-tot i (pr1 ∘ R))) ∙h
+                ( tot-htpy (pr2 ∘ R)) ∙h
+                ( tot-id B)))
             ( is-torsorial-path a))
           ( is-torsorial-path a))
+
+    fundamental-theorem-id-retract :
+      (R : (x : A) → (B x) retract-of (a ＝ x)) →
+      is-fiberwise-equiv (inclusion-retract ∘ R)
+    fundamental-theorem-id-retract R =
+      fundamental-theorem-id-retraction
+        ( inclusion-retract ∘ R)
+        ( retraction-retract ∘ R)
 ```
 
 ### The fundamental theorem of identity types, using sections
@@ -128,19 +141,18 @@ module _
 
   abstract
     fundamental-theorem-id-section :
-      (f : (x : A) → a ＝ x → B x) → ((x : A) → section (f x)) →
+      (f : (x : A) → a ＝ x → B x) →
+      ((x : A) → section (f x)) →
       is-fiberwise-equiv f
     fundamental-theorem-id-section f section-f x =
-      is-equiv-section-is-equiv (f x) (section-f x) (is-fiberwise-equiv-i x)
-      where
-      i : (x : A) → B x → a ＝ x
-      i = λ x → pr1 (section-f x)
-      retraction-i : (x : A) → retraction (i x)
-      pr1 (retraction-i x) = f x
-      pr2 (retraction-i x) = pr2 (section-f x)
-      is-fiberwise-equiv-i : is-fiberwise-equiv i
-      is-fiberwise-equiv-i =
-        fundamental-theorem-id-retraction a i retraction-i
+      is-equiv-section-is-equiv
+        ( f x)
+        ( section-f x)
+        ( fundamental-theorem-id-retraction
+          ( a)
+          ( λ x → map-section (f x) (section-f x))
+          ( λ x → (f x , is-section-map-section (f x) (section-f x)))
+          ( x))
 ```
 
 ## See also
diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md
index 4829557c6b..44e04f05f9 100644
--- a/src/foundation/identity-systems.lagda.md
+++ b/src/foundation/identity-systems.lagda.md
@@ -15,6 +15,7 @@ open import foundation.universe-levels
 open import foundation-core.contractible-types
 open import foundation-core.families-of-equivalences
 open import foundation-core.identity-types
+open import foundation-core.propositions
 open import foundation-core.sections
 open import foundation-core.torsorial-type-families
 open import foundation-core.transport-along-identifications
@@ -59,11 +60,11 @@ module _
 
 ```agda
 module _
-    {l1 l2 : Level} {A : UU l1} (B : A → UU l2) (a : A) (b : B a)
-    where
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) (a : A) (b : B a)
+  where
 
-    is-identity-system : UUω
-    is-identity-system = {l : Level} → is-identity-system-Level l B a b
+  is-identity-system : UUω
+  is-identity-system = {l : Level} → is-identity-system-Level l B a b
 ```
 
 ## Properties
diff --git a/src/foundation/isomorphisms-of-sets.lagda.md b/src/foundation/isomorphisms-of-sets.lagda.md
index f13a4ac68e..c1f3c53125 100644
--- a/src/foundation/isomorphisms-of-sets.lagda.md
+++ b/src/foundation/isomorphisms-of-sets.lagda.md
@@ -73,15 +73,15 @@ module _
       ( htpy-eq (pr1 (pr2 H)))
       ( htpy-eq (pr2 (pr2 H)))
 
-  iso-equiv-Set : type-equiv-Set A B → iso-Set
+  iso-equiv-Set : equiv-Set A B → iso-Set
   pr1 (iso-equiv-Set e) = map-equiv e
   pr2 (iso-equiv-Set e) = is-iso-is-equiv-Set (is-equiv-map-equiv e)
 
-  equiv-iso-Set : iso-Set → type-equiv-Set A B
+  equiv-iso-Set : iso-Set → equiv-Set A B
   pr1 (equiv-iso-Set f) = map-iso-Set f
   pr2 (equiv-iso-Set f) = is-equiv-is-iso-Set (is-iso-map-iso-Set f)
 
-  equiv-iso-equiv-Set : type-equiv-Set A B ≃ iso-Set
+  equiv-iso-equiv-Set : equiv-Set A B ≃ iso-Set
   equiv-iso-equiv-Set =
     equiv-type-subtype
       ( is-property-is-equiv)
diff --git a/src/foundation/path-split-maps.lagda.md b/src/foundation/path-split-maps.lagda.md
index a55bbed9d3..57d49b87c3 100644
--- a/src/foundation/path-split-maps.lagda.md
+++ b/src/foundation/path-split-maps.lagda.md
@@ -74,8 +74,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).
diff --git a/src/foundation/preunivalence.lagda.md b/src/foundation/preunivalence.lagda.md
index be874acfdd..298f482891 100644
--- a/src/foundation/preunivalence.lagda.md
+++ b/src/foundation/preunivalence.lagda.md
@@ -107,4 +107,5 @@ 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)
+- [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
new file mode 100644
index 0000000000..5d647dfedd
--- /dev/null
+++ b/src/foundation/preunivalent-type-families.lagda.md
@@ -0,0 +1,177 @@
+# Preunivalent type families
+
+```agda
+module foundation.preunivalent-type-families where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.0-maps
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalence-injective-type-families
+open import foundation.faithful-maps
+open import foundation.function-types
+open import foundation.preunivalence
+open import foundation.retractions
+open import foundation.subuniverses
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import foundation-core.equivalences
+open import foundation-core.identity-types
+open import foundation-core.injective-maps
+open import foundation-core.sets
+open import foundation-core.univalence
+```
+
+</details>
+
+## Idea
+
+A type family `B` over `A` is said to be
+{{#concept "preunivalent" Disambiguation="type family" Agda=is-preunivalent}} if
+the map
+
+```text
+  equiv-tr B : x ＝ y → B x ≃ B y
+```
+
+is an [embedding](foundation-core.embeddings.md) for every `x y : A`.
+
+## Definition
+
+```agda
+is-preunivalent :
+  {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2)
+is-preunivalent {A = A} B = (x y : A) → is-emb (λ (p : x ＝ y) → equiv-tr B p)
+```
+
+## Properties
+
+### Assuming the preunivalence axiom, type families are preunivalent if and only if they are faithful as maps
+
+**Proof:** We have the
+[commuting triangle of maps](foundation-core.commuting-triangles-of-maps.md)
+
+```text
+                ap B
+       (x ＝ y) -----> (B x ＝ B y)
+           \               /
+            \             /
+  equiv-tr B \           / equiv-eq
+              v         v
+              (B x ≃ B y)
+```
+
+where the right edge is an embedding by the
+[preunivalence axiom](foundation.preunivalence.md). Hence, the top map is an
+embedding if and only if the left map is.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  abstract
+    is-faithful-is-preunivalent :
+      is-preunivalent B → is-faithful B
+    is-faithful-is-preunivalent U x y =
+      is-emb-top-map-triangle
+        ( equiv-tr B)
+        ( equiv-eq)
+        ( ap B)
+        ( λ where refl → refl)
+        ( preunivalence (B x) (B y))
+        ( U x y)
+
+    is-preunivalent-is-faithful :
+      is-faithful B → is-preunivalent B
+    is-preunivalent-is-faithful is-faithful-B x y =
+      is-emb-left-map-triangle
+        ( equiv-tr B)
+        ( equiv-eq)
+        ( ap B)
+        ( λ where refl → refl)
+        ( preunivalence (B x) (B y))
+        ( is-faithful-B x y)
+
+    is-0-map-is-preunivalent :
+      is-preunivalent B → is-0-map B
+    is-0-map-is-preunivalent U =
+      is-0-map-is-faithful (is-faithful-is-preunivalent U)
+
+    is-preunivalent-is-0-map :
+      is-0-map B → is-preunivalent B
+    is-preunivalent-is-0-map H =
+      is-preunivalent-is-faithful (is-faithful-is-0-map H)
+```
+
+### Families of sets are preunivalent if `equiv-tr` is fiberwise injective
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2)
+  (is-set-B : (x : A) → is-set (B x))
+  where
+
+  is-preunivalent-is-injective-equiv-tr-is-set :
+    ((x y : A) → is-injective (equiv-tr B {x} {y})) →
+    is-preunivalent B
+  is-preunivalent-is-injective-equiv-tr-is-set is-inj-B x y =
+    is-emb-is-injective
+      ( is-set-equiv-is-set (is-set-B x) (is-set-B y))
+      ( is-inj-B x y)
+
+  is-preunivalent-retraction-equiv-tr-is-set :
+    ((x y : A) → retraction (equiv-tr B {x} {y})) →
+    is-preunivalent B
+  is-preunivalent-retraction-equiv-tr-is-set R =
+    is-preunivalent-is-injective-equiv-tr-is-set
+      ( λ x y → is-injective-retraction (equiv-tr B) (R x y))
+
+module _
+  {l1 l2 : Level} {A : UU l1} (B : A → Set l2)
+  where
+
+  is-preunivalent-is-injective-equiv-tr-Set :
+    ((x y : A) → is-injective (equiv-tr (type-Set ∘ B) {x} {y})) →
+    is-preunivalent (type-Set ∘ B)
+  is-preunivalent-is-injective-equiv-tr-Set =
+    is-preunivalent-is-injective-equiv-tr-is-set
+      ( type-Set ∘ B)
+      ( is-set-type-Set ∘ B)
+
+  is-preunivalent-retraction-equiv-tr-Set :
+    ((x y : A) → retraction (equiv-tr (type-Set ∘ B) {x} {y})) →
+    is-preunivalent (type-Set ∘ B)
+  is-preunivalent-retraction-equiv-tr-Set =
+    is-preunivalent-retraction-equiv-tr-is-set
+      ( type-Set ∘ B)
+      ( is-set-type-Set ∘ B)
+```
+
+### Inclusions of subuniverses into the universe are preunivalent
+
+**Note.** These proofs rely on essential use of the preunivalence axiom.
+
+```agda
+is-preunivalent-projection-Type-With-Set-Element :
+  {l1 l2 : Level} (S : UU l1 → Set l2) →
+  is-preunivalent (pr1 {A = UU l1} {B = type-Set ∘ S})
+is-preunivalent-projection-Type-With-Set-Element S =
+  is-preunivalent-is-0-map (is-0-map-pr1 (is-set-type-Set ∘ S))
+
+is-preunivalent-inclusion-subuniverse :
+  {l1 l2 : Level} (S : subuniverse l1 l2) →
+  is-preunivalent (inclusion-subuniverse S)
+is-preunivalent-inclusion-subuniverse S =
+  is-preunivalent-projection-Type-With-Set-Element (set-Prop ∘ S)
+```
+
+## See also
+
+- [Univalent type families](foundation.univalent-type-families.md)
+- [Transport-split type families](foundation.transport-split-type-families.md)
diff --git a/src/foundation/set-truncations.lagda.md b/src/foundation/set-truncations.lagda.md
index 8e4f26493e..c5080bce61 100644
--- a/src/foundation/set-truncations.lagda.md
+++ b/src/foundation/set-truncations.lagda.md
@@ -423,7 +423,7 @@ module _
   abstract
     distributive-trunc-coprod-Set :
       is-contr
-        ( Σ ( type-equiv-Set
+        ( Σ ( equiv-Set
               ( trunc-Set (A + B))
               ( coprod-Set (trunc-Set A) (trunc-Set B)))
             ( λ e →
@@ -451,7 +451,7 @@ module _
                 ( is-set-truncation-trunc-Set B C))))
 
   equiv-distributive-trunc-coprod-Set :
-    type-equiv-Set (trunc-Set (A + B)) (coprod-Set (trunc-Set A) (trunc-Set B))
+    equiv-Set (trunc-Set (A + B)) (coprod-Set (trunc-Set A) (trunc-Set B))
   equiv-distributive-trunc-coprod-Set =
     pr1 (center distributive-trunc-coprod-Set)
 
diff --git a/src/foundation/sets.lagda.md b/src/foundation/sets.lagda.md
index 8799c286aa..862fb3d31a 100644
--- a/src/foundation/sets.lagda.md
+++ b/src/foundation/sets.lagda.md
@@ -13,6 +13,7 @@ open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.subuniverses
 open import foundation.truncated-types
+open import foundation.univalent-type-families
 open import foundation.universe-levels
 
 open import foundation-core.1-types
@@ -23,6 +24,7 @@ open import foundation-core.identity-types
 open import foundation-core.precomposition-functions
 open import foundation-core.propositional-maps
 open import foundation-core.propositions
+open import foundation-core.subtypes
 open import foundation-core.torsorial-type-families
 open import foundation-core.truncation-levels
 ```
@@ -173,28 +175,6 @@ precomp-Set :
 precomp-Set f C = precomp f (type-Set C)
 ```
 
-### The type of equivalences between sets is a set
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  where
-
-  is-set-equiv-is-set : is-set A → is-set B → is-set (A ≃ B)
-  is-set-equiv-is-set = is-trunc-equiv-is-trunc zero-𝕋
-
-module _
-  {l1 l2 : Level} (A : Set l1) (B : Set l2)
-  where
-
-  type-equiv-Set : UU (l1 ⊔ l2)
-  type-equiv-Set = type-Set A ≃ type-Set B
-
-  equiv-Set : Set (l1 ⊔ l2)
-  pr1 equiv-Set = type-equiv-Set
-  pr2 equiv-Set = is-set-equiv-is-set (is-set-type-Set A) (is-set-type-Set B)
-```
-
 ### Extensionality of sets
 
 ```agda
@@ -202,11 +182,11 @@ module _
   {l : Level} (X : Set l)
   where
 
-  equiv-eq-Set : (Y : Set l) → X ＝ Y → type-equiv-Set X Y
+  equiv-eq-Set : (Y : Set l) → X ＝ Y → equiv-Set X Y
   equiv-eq-Set = equiv-eq-subuniverse is-set-Prop X
 
   abstract
-    is-torsorial-equiv-Set : is-torsorial (λ (Y : Set l) → type-equiv-Set X Y)
+    is-torsorial-equiv-Set : is-torsorial (λ (Y : Set l) → equiv-Set X Y)
     is-torsorial-equiv-Set =
       is-torsorial-equiv-subuniverse is-set-Prop X
 
@@ -214,10 +194,10 @@ module _
     is-equiv-equiv-eq-Set : (Y : Set l) → is-equiv (equiv-eq-Set Y)
     is-equiv-equiv-eq-Set = is-equiv-equiv-eq-subuniverse is-set-Prop X
 
-  eq-equiv-Set : (Y : Set l) → type-equiv-Set X Y → X ＝ Y
+  eq-equiv-Set : (Y : Set l) → equiv-Set X Y → X ＝ Y
   eq-equiv-Set Y = eq-equiv-subuniverse is-set-Prop
 
-  extensionality-Set : (Y : Set l) → (X ＝ Y) ≃ type-equiv-Set X Y
+  extensionality-Set : (Y : Set l) → (X ＝ Y) ≃ equiv-Set X Y
   pr1 (extensionality-Set Y) = equiv-eq-Set Y
   pr2 (extensionality-Set Y) = is-equiv-equiv-eq-Set Y
 ```
@@ -263,3 +243,23 @@ set-Truncated-Type :
 pr1 (set-Truncated-Type k A) = type-Set A
 pr2 (set-Truncated-Type k A) = is-trunc-is-set k (is-set-type-Set A)
 ```
+
+### The type of equivalences is a set if the domain or codomain is a set
+
+```agda
+abstract
+  is-set-equiv-is-set-codomain :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-set B → is-set (A ≃ B)
+  is-set-equiv-is-set-codomain = is-trunc-equiv-is-trunc-codomain neg-one-𝕋
+
+  is-set-equiv-is-set-domain :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-set A → is-set (A ≃ B)
+  is-set-equiv-is-set-domain = is-trunc-equiv-is-trunc-domain neg-one-𝕋
+```
+
+### The canonical type family over `Set` is univalent
+
+```agda
+is-univalent-type-Set : {l : Level} → is-univalent (type-Set {l})
+is-univalent-type-Set = is-univalent-inclusion-subuniverse is-set-Prop
+```
diff --git a/src/foundation/transport-along-identifications.lagda.md b/src/foundation/transport-along-identifications.lagda.md
index 35d9f29985..0edb4f76e6 100644
--- a/src/foundation/transport-along-identifications.lagda.md
+++ b/src/foundation/transport-along-identifications.lagda.md
@@ -56,7 +56,7 @@ module _
       ( is-section-inv-tr p)
       ( is-retraction-inv-tr p)
 
-  equiv-tr : x ＝ y → (B x) ≃ (B y)
+  equiv-tr : x ＝ y → B x ≃ B y
   pr1 (equiv-tr p) = tr B p
   pr2 (equiv-tr p) = is-equiv-tr p
 ```
diff --git a/src/foundation/transport-split-type-families.lagda.md b/src/foundation/transport-split-type-families.lagda.md
new file mode 100644
index 0000000000..f4fc0dad2f
--- /dev/null
+++ b/src/foundation/transport-split-type-families.lagda.md
@@ -0,0 +1,158 @@
+# Transport-split type families
+
+```agda
+module foundation.transport-split-type-families where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-equivalences-functions
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.equivalence-extensionality
+open import foundation.equivalence-injective-type-families
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.iterated-dependent-product-types
+open import foundation.transport-along-identifications
+open import foundation.unit-type
+open import foundation.univalent-type-families
+open import foundation.universal-property-identity-systems
+open import foundation.universe-levels
+
+open import foundation-core.embeddings
+open import foundation-core.identity-types
+open import foundation-core.propositions
+open import foundation-core.sections
+open import foundation-core.torsorial-type-families
+```
+
+</details>
+
+## Idea
+
+A type family `B` over `A` is said to be
+{{#concept "transport-split" Disambiguation="type family" Agda=is-transport-split}}
+if the map
+
+```text
+  equiv-tr B : x ＝ y → B x ≃ B y
+```
+
+admits a [section](foundation-core.sections.md) for every `x y : A`. By a
+corollary of
+[the fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md)
+every transport-split type family is
+[univalent](foundation.univalent-type-families.md), meaning that `equiv-tr B` is
+in fact an [equivalence](foundation-core.equivalences.md) for all `x y : A`.
+
+## Definition
+
+### Transport-split type families
+
+```agda
+is-transport-split :
+  {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2)
+is-transport-split {A = A} B =
+  (x y : A) → section (λ (p : x ＝ y) → equiv-tr B p)
+```
+
+## Properties
+
+### Transport-split type families are equivalence injective
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  is-equivalence-injective-is-transport-split :
+    is-transport-split B → is-equivalence-injective B
+  is-equivalence-injective-is-transport-split s {x} {y} =
+    map-section (equiv-tr B) (s x y)
+```
+
+### Transport-split type families are univalent
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  is-transport-split-is-univalent :
+    is-univalent B → is-transport-split B
+  is-transport-split-is-univalent U x y = section-is-equiv (U x y)
+
+  is-univalent-is-transport-split :
+    is-transport-split B → is-univalent B
+  is-univalent-is-transport-split s x =
+    fundamental-theorem-id-section x (λ y → equiv-tr B) (s x)
+```
+
+### The type `is-transport-split` is a proposition
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  is-proof-irrelevant-is-transport-split :
+    is-proof-irrelevant (is-transport-split B)
+  is-proof-irrelevant-is-transport-split s =
+    is-contr-iterated-Π 2
+      ( λ x y →
+        is-contr-section-is-equiv (is-univalent-is-transport-split s x y))
+
+  is-prop-is-transport-split :
+    is-prop (is-transport-split B)
+  is-prop-is-transport-split =
+    is-prop-is-proof-irrelevant is-proof-irrelevant-is-transport-split
+```
+
+### Assuming the univalence axiom, type families are transport-split if and only if they are embeddings as maps
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  is-emb-is-transport-split : is-transport-split B → is-emb B
+  is-emb-is-transport-split s =
+    is-emb-is-univalent (is-univalent-is-transport-split s)
+
+  is-transport-split-is-emb : is-emb B → is-transport-split B
+  is-transport-split-is-emb H =
+    is-transport-split-is-univalent (is-univalent-is-emb H)
+```
+
+### Transport-split type families satisfy equivalence induction
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  (s : is-transport-split B)
+  where
+
+  is-torsorial-fam-equiv-is-transport-split :
+    {x : A} → is-torsorial (λ y → B x ≃ B y)
+  is-torsorial-fam-equiv-is-transport-split =
+    is-torsorial-fam-equiv-is-univalent (is-univalent-is-transport-split s)
+
+  dependent-universal-property-identity-system-fam-equiv-is-transport-split :
+    {x : A} →
+    dependent-universal-property-identity-system (λ y → B x ≃ B y) id-equiv
+  dependent-universal-property-identity-system-fam-equiv-is-transport-split =
+    dependent-universal-property-identity-system-is-torsorial
+      ( id-equiv)
+      ( is-torsorial-fam-equiv-is-transport-split)
+```
+
+## See also
+
+- [Univalent type families](foundation.univalent-type-families.md)
+- [Preunivalent type families](foundation.preunivalent-type-families.md)
diff --git a/src/foundation/truncated-types.lagda.md b/src/foundation/truncated-types.lagda.md
index 33d95d4812..3adb80b12a 100644
--- a/src/foundation/truncated-types.lagda.md
+++ b/src/foundation/truncated-types.lagda.md
@@ -12,13 +12,13 @@ open import foundation-core.truncated-types public
 open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.equivalences
 open import foundation.subtype-identity-principle
 open import foundation.truncation-levels
 open import foundation.univalence
 open import foundation.universe-levels
 
 open import foundation-core.embeddings
-open import foundation-core.equivalences
 open import foundation-core.identity-types
 open import foundation-core.propositions
 open import foundation-core.subtypes
@@ -110,3 +110,32 @@ module _
       ( is-trunc-equiv' k A e)
       ( is-trunc-equiv k B e)
 ```
+
+### If the domain or codomain is `k+1`-truncated, then the type of equivalences is `k+1`-truncated
+
+```agda
+module _
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
+  where
+
+  is-trunc-equiv-is-trunc-codomain :
+    is-trunc (succ-𝕋 k) B → is-trunc (succ-𝕋 k) (A ≃ B)
+  is-trunc-equiv-is-trunc-codomain is-trunc-B =
+    is-trunc-type-subtype
+      ( k)
+      ( is-equiv-Prop)
+      ( is-trunc-function-type (succ-𝕋 k) is-trunc-B)
+
+module _
+  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
+  where
+
+  is-trunc-equiv-is-trunc-domain :
+    is-trunc (succ-𝕋 k) A → is-trunc (succ-𝕋 k) (A ≃ B)
+  is-trunc-equiv-is-trunc-domain is-trunc-A =
+    is-trunc-equiv
+      ( succ-𝕋 k)
+      ( B ≃ A)
+      ( equiv-inv-equiv)
+      ( is-trunc-equiv-is-trunc-codomain k is-trunc-A)
+```
diff --git a/src/foundation/univalent-type-families.lagda.md b/src/foundation/univalent-type-families.lagda.md
index 8297c1c7a7..d68a061924 100644
--- a/src/foundation/univalent-type-families.lagda.md
+++ b/src/foundation/univalent-type-families.lagda.md
@@ -7,29 +7,164 @@ module foundation.univalent-type-families where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-systems
+open import foundation.iterated-dependent-product-types
+open import foundation.propositions
+open import foundation.subuniverses
 open import foundation.transport-along-identifications
+open import foundation.univalence
+open import foundation.universal-property-identity-systems
 open import foundation.universe-levels
 
-open import foundation-core.equivalences
+open import foundation-core.embeddings
 open import foundation-core.identity-types
+open import foundation-core.sections
+open import foundation-core.torsorial-type-families
 ```
 
 </details>
 
 ## Idea
 
-A type family `B` over `A` is said to be univalent if the map
+A type family `B` over `A` is said to be
+{{#concept "univalent" Disambiguation="type family" Agda=is-univalent}} if the
+map
 
 ```text
-  equiv-tr : (Id x y) → (B x ≃ B y)
+  equiv-tr B : x ＝ y → B x ≃ B y
 ```
 
-is an equivalence for every `x y : A`.
+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.
 
 ## Definition
 
+### The predicate on type families of being univalent
+
 ```agda
 is-univalent :
   {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2)
 is-univalent {A = A} B = (x y : A) → is-equiv (λ (p : x ＝ y) → equiv-tr B p)
+
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  is-prop-is-univalent : is-prop (is-univalent B)
+  is-prop-is-univalent =
+    is-prop-iterated-Π 2 (λ x y → is-property-is-equiv (equiv-tr B))
+
+  is-univalent-Prop : Prop (l1 ⊔ l2)
+  pr1 is-univalent-Prop = is-univalent B
+  pr2 is-univalent-Prop = is-prop-is-univalent
+```
+
+### Univalent type families
+
+```agda
+univalent-type-family :
+  {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2)
+univalent-type-family l2 A = Σ (A → UU l2) is-univalent
+```
+
+## Properties
+
+### Assuming the univalence axiom, type families are univalent if and only if they are embeddings as maps
+
+**Proof:** We have the
+[commuting triangle of maps](foundation-core.commuting-triangles-of-maps.md)
+
+```text
+                ap B
+       (x ＝ y) -----> (B x ＝ B y)
+           \               /
+            \             /
+  equiv-tr B \           / equiv-eq
+              v         v
+              (B x ≃ B y)
+```
+
+where the right edge is an equivalence by the univalence axiom. Hence, the top
+map is an equivalence if and only if the left map is.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  abstract
+    is-emb-is-univalent :
+      is-univalent B → is-emb B
+    is-emb-is-univalent U x y =
+      is-equiv-top-map-triangle
+        ( equiv-tr B)
+        ( equiv-eq)
+        ( ap B)
+        ( λ where refl → refl)
+        ( univalence (B x) (B y))
+        ( U x y)
+
+    is-univalent-is-emb :
+      is-emb B → is-univalent B
+    is-univalent-is-emb is-emb-B x y =
+      is-equiv-left-map-triangle
+        ( equiv-tr B)
+        ( equiv-eq)
+        ( ap B)
+        ( λ where refl → refl)
+        ( is-emb-B x y)
+        ( univalence (B x) (B y))
+```
+
+### Univalent type families satisfy equivalence induction
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  (U : is-univalent B)
+  where
+
+  is-torsorial-fam-equiv-is-univalent :
+    {x : A} → is-torsorial (λ y → B x ≃ B y)
+  is-torsorial-fam-equiv-is-univalent {x} =
+    fundamental-theorem-id' (λ y → equiv-tr B) (U x)
+
+  dependent-universal-property-identity-system-fam-equiv-is-univalent :
+    {x : A} →
+    dependent-universal-property-identity-system (λ y → B x ≃ B y) id-equiv
+  dependent-universal-property-identity-system-fam-equiv-is-univalent {x} =
+    dependent-universal-property-identity-system-is-torsorial
+      ( id-equiv)
+      ( is-torsorial-fam-equiv-is-univalent {x})
 ```
+
+### Inclusions of subuniverses into the universe are univalent
+
+**Note.** This proof relies on essential use of the univalence axiom.
+
+```agda
+module _
+  {l1 l2 : Level} (S : subuniverse l1 l2)
+  where
+
+  is-univalent-inclusion-subuniverse : is-univalent (inclusion-subuniverse S)
+  is-univalent-inclusion-subuniverse =
+    is-univalent-is-emb (is-emb-inclusion-subuniverse S)
+```
+
+## See also
+
+- [Preunivalent type families](foundation.preunivalent-type-families.md)
+- [Transport-split type families](foundation.transport-split-type-families.md):
+  By a corollary of
+  [the fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md),
+  `equiv-tr B` is a
+  [fiberwise equivalence](foundation-core.families-of-equivalences.md) as soon
+  as it admits a fiberwise [section](foundation-core.sections.md).
diff --git a/src/foundation/universal-property-identity-systems.lagda.md b/src/foundation/universal-property-identity-systems.lagda.md
index 8748ea89d0..a29595fa9d 100644
--- a/src/foundation/universal-property-identity-systems.lagda.md
+++ b/src/foundation/universal-property-identity-systems.lagda.md
@@ -36,8 +36,8 @@ also follows for identity systems.
 
 ```agda
 dependent-universal-property-identity-system :
-  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {a : A} (b : B a) → UUω
-dependent-universal-property-identity-system {A = A} {B} b =
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {a : A} (b : B a) → UUω
+dependent-universal-property-identity-system {A = A} B b =
   {l3 : Level} (P : (x : A) (y : B x) → UU l3) →
   is-equiv (ev-refl-identity-system b {P})
 ```
@@ -53,7 +53,7 @@ module _
 
   dependent-universal-property-identity-system-is-torsorial :
     is-torsorial B →
-    dependent-universal-property-identity-system {B = B} b
+    dependent-universal-property-identity-system B b
   dependent-universal-property-identity-system-is-torsorial
     H P =
     is-equiv-left-factor
@@ -75,7 +75,7 @@ module _
     dependent-universal-property-identity-system-is-torsorial H _
 
   is-torsorial-dependent-universal-property-identity-system :
-    dependent-universal-property-identity-system {B = B} b →
+    dependent-universal-property-identity-system B b →
     is-torsorial B
   pr1 (is-torsorial-dependent-universal-property-identity-system H) = (a , b)
   pr2 (is-torsorial-dependent-universal-property-identity-system H) u =
@@ -95,13 +95,13 @@ module _
 
   dependent-universal-property-identity-system-is-identity-system :
     is-identity-system B a b →
-    dependent-universal-property-identity-system {B = B} b
+    dependent-universal-property-identity-system B b
   dependent-universal-property-identity-system-is-identity-system H =
     dependent-universal-property-identity-system-is-torsorial b
       ( is-torsorial-is-identity-system a b H)
 
   is-identity-system-dependent-universal-property-identity-system :
-    dependent-universal-property-identity-system {B = B} b →
+    dependent-universal-property-identity-system B b →
     is-identity-system B a b
   is-identity-system-dependent-universal-property-identity-system H P =
     section-is-equiv (H P)
diff --git a/src/group-theory/equivalences-concrete-group-actions.lagda.md b/src/group-theory/equivalences-concrete-group-actions.lagda.md
index a631706793..27c37431a5 100644
--- a/src/group-theory/equivalences-concrete-group-actions.lagda.md
+++ b/src/group-theory/equivalences-concrete-group-actions.lagda.md
@@ -41,7 +41,7 @@ module _
   equiv-action-Concrete-Group :
     {l3 : Level} (Y : action-Concrete-Group l3 G) → UU (l1 ⊔ l2 ⊔ l3)
   equiv-action-Concrete-Group Y =
-    (u : classifying-type-Concrete-Group G) → type-equiv-Set (X u) (Y u)
+    (u : classifying-type-Concrete-Group G) → equiv-Set (X u) (Y u)
 
   id-equiv-action-Concrete-Group : equiv-action-Concrete-Group X
   id-equiv-action-Concrete-Group u = id-equiv
@@ -50,7 +50,7 @@ module _
     (Y : action-Concrete-Group l2 G) → (X ＝ Y) ≃ equiv-action-Concrete-Group Y
   extensionality-action-Concrete-Group =
     extensionality-Π X
-      ( λ u → type-equiv-Set (X u))
+      ( λ u → equiv-Set (X u))
       ( λ u → extensionality-Set (X u))
 
   equiv-eq-action-Concrete-Group :
diff --git a/src/group-theory/symmetric-concrete-groups.lagda.md b/src/group-theory/symmetric-concrete-groups.lagda.md
index b329c223a9..006ef44e03 100644
--- a/src/group-theory/symmetric-concrete-groups.lagda.md
+++ b/src/group-theory/symmetric-concrete-groups.lagda.md
@@ -57,7 +57,7 @@ module _
   equiv-classifying-type-symmetric-Concrete-Group :
     (X Y : classifying-type-symmetric-Concrete-Group A) → UU l
   equiv-classifying-type-symmetric-Concrete-Group X Y =
-    type-equiv-Set (pr1 X) (pr1 Y)
+    equiv-Set (pr1 X) (pr1 Y)
 
   type-symmetric-Concrete-Group : UU l
   type-symmetric-Concrete-Group =
diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md
index b15edfc919..01e0347945 100644
--- a/src/univalent-combinatorics/2-element-types.lagda.md
+++ b/src/univalent-combinatorics/2-element-types.lagda.md
@@ -410,7 +410,7 @@ is-identity-system-type-2-Element-Type X x =
 dependent-universal-property-identity-system-type-2-Element-Type :
   {l1 : Level} (X : 2-Element-Type l1) (x : type-2-Element-Type X) →
   dependent-universal-property-identity-system
-    { B = type-2-Element-Type {l1}}
+    ( type-2-Element-Type {l1})
     { a = X}
     ( x)
 dependent-universal-property-identity-system-type-2-Element-Type X x =
diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md
index aec18df6b8..9103b85ba3 100644
--- a/src/univalent-combinatorics/standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/standard-finite-types.lagda.md
@@ -30,8 +30,13 @@ open import foundation.injective-maps
 open import foundation.negated-equality
 open import foundation.negation
 open import foundation.noncontractible-types
+open import foundation.path-algebra
+open import foundation.preunivalent-type-families
 open import foundation.raising-universe-levels
+open import foundation.retractions
+open import foundation.sections
 open import foundation.sets
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -427,22 +432,55 @@ leq-nat-succ-Fin (succ-ℕ k) (inr star) =
     ( leq-zero-ℕ (succ-ℕ (nat-Fin (succ-ℕ k) (inr star))))
 ```
 
-### Fin is injective
+### `Fin` is injective
 
 ```agda
-abstract
-  is-equivalence-injective-Fin : is-equivalence-injective Fin
-  is-equivalence-injective-Fin {zero-ℕ} {zero-ℕ} e =
-    refl
-  is-equivalence-injective-Fin {zero-ℕ} {succ-ℕ l} e =
-    ex-falso (map-inv-equiv e (zero-Fin l))
-  is-equivalence-injective-Fin {succ-ℕ k} {zero-ℕ} e =
-    ex-falso (map-equiv e (zero-Fin k))
-  is-equivalence-injective-Fin {succ-ℕ k} {succ-ℕ l} e =
-    ap succ-ℕ (is-equivalence-injective-Fin (equiv-equiv-Maybe e))
+is-equivalence-injective-Fin : is-equivalence-injective Fin
+is-equivalence-injective-Fin {zero-ℕ} {zero-ℕ} e =
+  refl
+is-equivalence-injective-Fin {zero-ℕ} {succ-ℕ l} e =
+  ex-falso (map-inv-equiv e (zero-Fin l))
+is-equivalence-injective-Fin {succ-ℕ k} {zero-ℕ} e =
+  ex-falso (map-equiv e (zero-Fin k))
+is-equivalence-injective-Fin {succ-ℕ k} {succ-ℕ l} e =
+  ap succ-ℕ (is-equivalence-injective-Fin (equiv-equiv-Maybe e))
 
 abstract
   is-injective-Fin : is-injective Fin
   is-injective-Fin =
     is-injective-is-equivalence-injective is-equivalence-injective-Fin
+
+compute-is-equivalence-injective-Fin-id-equiv :
+  {n : ℕ} → is-equivalence-injective-Fin {n} {n} id-equiv ＝ refl
+compute-is-equivalence-injective-Fin-id-equiv {zero-ℕ} = refl
+compute-is-equivalence-injective-Fin-id-equiv {succ-ℕ n} =
+  ap² succ-ℕ
+    ( ( ap is-equivalence-injective-Fin compute-equiv-equiv-Maybe-id-equiv) ∙
+      ( compute-is-equivalence-injective-Fin-id-equiv {n}))
+```
+
+### `Fin` is a preunivalent type family
+
+The proof does not rely on the (pre-)univalence axiom.
+
+```agda
+is-section-on-diagonal-is-equivalence-injective-Fin :
+  {n : ℕ} →
+  equiv-tr Fin (is-equivalence-injective-Fin {n} {n} id-equiv) ＝ id-equiv
+is-section-on-diagonal-is-equivalence-injective-Fin =
+  ap (equiv-tr Fin) compute-is-equivalence-injective-Fin-id-equiv
+
+is-retraction-is-equivalence-injective-Fin :
+  {n m : ℕ} →
+  is-retraction (equiv-tr Fin) (is-equivalence-injective-Fin {n} {m})
+is-retraction-is-equivalence-injective-Fin refl =
+  compute-is-equivalence-injective-Fin-id-equiv
+
+retraction-equiv-tr-Fin : (n m : ℕ) → retraction (equiv-tr Fin {n} {m})
+pr1 (retraction-equiv-tr-Fin n m) = is-equivalence-injective-Fin
+pr2 (retraction-equiv-tr-Fin n m) = is-retraction-is-equivalence-injective-Fin
+
+is-preunivalent-Fin : is-preunivalent Fin
+is-preunivalent-Fin =
+  is-preunivalent-retraction-equiv-tr-Set Fin-Set retraction-equiv-tr-Fin
 ```