diff --git a/src/elementary-number-theory/integers.lagda.md b/src/elementary-number-theory/integers.lagda.md
index ed178f802d..d8ccb12696 100644
--- a/src/elementary-number-theory/integers.lagda.md
+++ b/src/elementary-number-theory/integers.lagda.md
@@ -23,6 +23,8 @@ open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.negated-equality
 open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
 open import foundation.sets
 open import foundation.unit-type
 open import foundation.universe-levels
@@ -160,17 +162,17 @@ pr2 ℤ-Set = is-set-ℤ
 
 ```agda
 abstract
-  is-retraction-pred-ℤ : (pred-ℤ ∘ succ-ℤ) ~ id
+  is-retraction-pred-ℤ : is-retraction succ-ℤ pred-ℤ
   is-retraction-pred-ℤ (inl zero-ℕ) = refl
   is-retraction-pred-ℤ (inl (succ-ℕ x)) = refl
-  is-retraction-pred-ℤ (inr (inl star)) = refl
+  is-retraction-pred-ℤ (inr (inl _)) = refl
   is-retraction-pred-ℤ (inr (inr zero-ℕ)) = refl
   is-retraction-pred-ℤ (inr (inr (succ-ℕ x))) = refl
 
-  is-section-pred-ℤ : (succ-ℤ ∘ pred-ℤ) ~ id
+  is-section-pred-ℤ : is-section succ-ℤ pred-ℤ
   is-section-pred-ℤ (inl zero-ℕ) = refl
   is-section-pred-ℤ (inl (succ-ℕ x)) = refl
-  is-section-pred-ℤ (inr (inl star)) = refl
+  is-section-pred-ℤ (inr (inl _)) = refl
   is-section-pred-ℤ (inr (inr zero-ℕ)) = refl
   is-section-pred-ℤ (inr (inr (succ-ℕ x))) = refl
 
@@ -213,7 +215,7 @@ has-no-fixed-points-succ-ℤ (inr (inl star)) ()
 ### The negative function is an involution
 
 ```agda
-neg-neg-ℤ : (neg-ℤ ∘ neg-ℤ) ~ id
+neg-neg-ℤ : neg-ℤ ∘ neg-ℤ ~ id
 neg-neg-ℤ (inl n) = refl
 neg-neg-ℤ (inr (inl star)) = refl
 neg-neg-ℤ (inr (inr n)) = refl
@@ -419,7 +421,7 @@ decide-is-nonnegative-ℤ {inl x} = inr star
 decide-is-nonnegative-ℤ {inr x} = inl star
 
 is-zero-is-nonnegative-neg-is-nonnegative-ℤ :
-  (x : ℤ) → (is-nonnegative-ℤ x) → (is-nonnegative-ℤ (neg-ℤ x)) → is-zero-ℤ x
+  (x : ℤ) → is-nonnegative-ℤ x → is-nonnegative-ℤ (neg-ℤ x) → is-zero-ℤ x
 is-zero-is-nonnegative-neg-is-nonnegative-ℤ (inr (inl star)) nonneg nonpos =
   refl
 ```
diff --git a/src/elementary-number-theory/modular-arithmetic.lagda.md b/src/elementary-number-theory/modular-arithmetic.lagda.md
index 1c2632a9f5..c68a033c92 100644
--- a/src/elementary-number-theory/modular-arithmetic.lagda.md
+++ b/src/elementary-number-theory/modular-arithmetic.lagda.md
@@ -100,7 +100,7 @@ has-decidable-equality-ℤ-Mod zero-ℕ = has-decidable-equality-ℤ
 has-decidable-equality-ℤ-Mod (succ-ℕ k) = has-decidable-equality-Fin (succ-ℕ k)
 ```
 
-### The integers modulo k are a discrete type
+### The integers modulo `k` are a discrete type
 
 ```agda
 ℤ-Mod-Discrete-Type : (k : ℕ) → Discrete-Type lzero
@@ -108,7 +108,7 @@ has-decidable-equality-ℤ-Mod (succ-ℕ k) = has-decidable-equality-Fin (succ-
 ℤ-Mod-Discrete-Type (succ-ℕ k) = Fin-Discrete-Type (succ-ℕ k)
 ```
 
-### The integers modulo k form a set
+### The integers modulo `k` form a set
 
 ```agda
 abstract
@@ -134,7 +134,7 @@ pr1 (ℤ-Mod-𝔽 k H) = ℤ-Mod k
 pr2 (ℤ-Mod-𝔽 k H) = is-finite-ℤ-Mod H
 ```
 
-## The inclusion of the integers modulo k into ℤ
+## The inclusion of the integers modulo `k` into ℤ
 
 ```agda
 int-ℤ-Mod : (k : ℕ) → ℤ-Mod k → ℤ
@@ -162,7 +162,7 @@ int-ℤ-Mod-bounded (succ-ℕ k) (inr x) = is-nonnegative-succ-ℤ
   (is-nonnegative-eq-ℤ (inv (left-inverse-law-add-ℤ (inl k))) star)
 ```
 
-## The successor and predecessor functions on the integers modulo k
+## The successor and predecessor functions on the integers modulo `k`
 
 ```agda
 succ-ℤ-Mod : (k : ℕ) → ℤ-Mod k → ℤ-Mod k
@@ -265,7 +265,7 @@ pr1 (equiv-neg-ℤ-Mod k) = neg-ℤ-Mod k
 pr2 (equiv-neg-ℤ-Mod k) = is-equiv-neg-ℤ-Mod k
 ```
 
-## Laws of addition modulo k
+## Laws of addition modulo `k`
 
 ```agda
 associative-add-ℤ-Mod :
@@ -347,7 +347,7 @@ is-left-add-neg-one-pred-ℤ-Mod' zero-ℕ = is-right-add-neg-one-pred-ℤ
 is-left-add-neg-one-pred-ℤ-Mod' (succ-ℕ k) = is-add-neg-one-pred-Fin' k
 ```
 
-## Multiplication modulo k
+## Multiplication modulo `k`
 
 ```agda
 mul-ℤ-Mod : (k : ℕ) → ℤ-Mod k → ℤ-Mod k → ℤ-Mod k
@@ -363,7 +363,7 @@ ap-mul-ℤ-Mod :
 ap-mul-ℤ-Mod k p q = ap-binary (mul-ℤ-Mod k) p q
 ```
 
-## Laws of multiplication modulo k
+## Laws of multiplication modulo `k`
 
 ```agda
 associative-mul-ℤ-Mod :
@@ -414,7 +414,7 @@ is-left-mul-neg-one-neg-ℤ-Mod' zero-ℕ = is-right-mul-neg-one-neg-ℤ
 is-left-mul-neg-one-neg-ℤ-Mod' (succ-ℕ k) = is-mul-neg-one-neg-Fin' k
 ```
 
-## Congruence classes of integers modulo k
+## Congruence classes of integers modulo `k`
 
 ```agda
 mod-ℕ : (k : ℕ) → ℕ → ℤ-Mod k
diff --git a/src/foundation-core/function-types.lagda.md b/src/foundation-core/function-types.lagda.md
index af53674bf7..0fad64ab6a 100644
--- a/src/foundation-core/function-types.lagda.md
+++ b/src/foundation-core/function-types.lagda.md
@@ -70,6 +70,14 @@ map-Π' :
   ((j : J) → A (α j)) →
   ((j : J) → B (α j))
 map-Π' α f = map-Π (f ∘ α)
+
+map-implicit-Π :
+  {l1 l2 l3 : Level}
+  {I : UU l1} {A : I → UU l2} {B : I → UU l3}
+  (f : (i : I) → A i → B i) →
+  ({i : I} → A i) →
+  ({i : I} → B i)
+map-implicit-Π f h {i} = map-Π f (λ i → h {i}) i
 ```
 
 ## See also
diff --git a/src/foundation-core/functoriality-dependent-function-types.lagda.md b/src/foundation-core/functoriality-dependent-function-types.lagda.md
index cc5b313869..ca9dae1874 100644
--- a/src/foundation-core/functoriality-dependent-function-types.lagda.md
+++ b/src/foundation-core/functoriality-dependent-function-types.lagda.md
@@ -68,7 +68,7 @@ compute-fiber-map-Π' α f = compute-fiber-map-Π (f ∘ α)
 abstract
   is-equiv-map-Π-is-fiberwise-equiv :
     {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-    {f : (i : I) → A i → B i} (is-equiv-f : is-fiberwise-equiv f) →
+    {f : (i : I) → A i → B i} → is-fiberwise-equiv f →
     is-equiv (map-Π f)
   is-equiv-map-Π-is-fiberwise-equiv is-equiv-f =
     is-equiv-is-contr-map
@@ -80,15 +80,26 @@ abstract
 equiv-Π-equiv-family :
   {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
   (e : (i : I) → (A i) ≃ (B i)) → ((i : I) → A i) ≃ ((i : I) → B i)
-pr1 (equiv-Π-equiv-family e) = map-Π (λ i → map-equiv (e i))
+pr1 (equiv-Π-equiv-family e) =
+  map-Π (λ i → map-equiv (e i))
 pr2 (equiv-Π-equiv-family e) =
-  is-equiv-map-Π-is-fiberwise-equiv
-    ( λ i → is-equiv-map-equiv (e i))
+  is-equiv-map-Π-is-fiberwise-equiv (λ i → is-equiv-map-equiv (e i))
 ```
 
 ### Families of equivalences induce equivalences of implicit dependent function types
 
 ```agda
+is-equiv-map-implicit-Π-is-fiberwise-equiv :
+    {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
+    {f : (i : I) → A i → B i} → is-fiberwise-equiv f →
+    is-equiv (map-implicit-Π f)
+is-equiv-map-implicit-Π-is-fiberwise-equiv is-equiv-f =
+  is-equiv-comp _ _
+    ( is-equiv-explicit-implicit-Π)
+    ( is-equiv-comp _ _
+      ( is-equiv-map-Π-is-fiberwise-equiv is-equiv-f)
+      ( is-equiv-implicit-explicit-Π))
+
 equiv-implicit-Π-equiv-family :
   {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
   (e : (i : I) → (A i) ≃ (B i)) → ({i : I} → A i) ≃ ({i : I} → B i)
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index e9498652a5..1509e9ca13 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -130,6 +130,7 @@ open import foundation.equality-fibers-of-maps public
 open import foundation.equivalence-classes public
 open import foundation.equivalence-extensionality public
 open import foundation.equivalence-induction public
+open import foundation.equivalence-injective-type-families public
 open import foundation.equivalence-relations public
 open import foundation.equivalences public
 open import foundation.equivalences-arrows public
diff --git a/src/foundation/equivalence-injective-type-families.lagda.md b/src/foundation/equivalence-injective-type-families.lagda.md
new file mode 100644
index 0000000000..d565eb4308
--- /dev/null
+++ b/src/foundation/equivalence-injective-type-families.lagda.md
@@ -0,0 +1,110 @@
+# Equivalence injective type families
+
+```agda
+module foundation.equivalence-injective-type-families where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.iterated-dependent-product-types
+open import foundation.univalence
+open import foundation.universal-property-equivalences
+open import foundation.universe-levels
+
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.identity-types
+open import foundation-core.injective-maps
+open import foundation-core.propositions
+open import foundation-core.sets
+```
+
+</details>
+
+## Idea
+
+We say a type family `P` is
+{{#concept "equivalence injective" Disambiguation="type family" Agda=is-equivalence-injective}}
+if for every [equivalence of types](foundation-core.equivalences.md) `P x ≃ P y`
+we have `x ＝ y `. By [univalence](foundation-core.univalence.md), the
+[structure](foundation.structure.md) of being equivalence injective is
+equivalent to being [injective as a map](foundation-core.injective-maps.md), but
+more generally every equivalence injective type family must always be injective
+as a map.
+
+**Note.** The concept of equivalence injective type family as considered here is
+unrelated to the concept of "injective type" as studied by Martín Escardó in
+_Injective types in univalent mathematics_
+([arXiv:1903.01211](https://arxiv.org/abs/1903.01211),
+[TypeTopology](https://www.cs.bham.ac.uk/~mhe/TypeTopology/InjectiveTypes.index.html)).
+
+## Definition
+
+### Equivalence injective type families
+
+```agda
+is-equivalence-injective :
+  {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2)
+is-equivalence-injective {A = A} P = {x y : A} → P x ≃ P y → x ＝ y
+```
+
+## Properties
+
+### Equivalence injective type families are injective as maps
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {P : A → UU l2}
+  where
+
+  is-injective-is-equivalence-injective :
+    is-equivalence-injective P → is-injective P
+  is-injective-is-equivalence-injective H = H ∘ equiv-eq
+
+  is-equivalence-injective-is-injective :
+    is-injective P → is-equivalence-injective P
+  is-equivalence-injective-is-injective H = H ∘ eq-equiv
+
+  is-equiv-is-injective-is-equivalence-injective :
+    is-equiv is-injective-is-equivalence-injective
+  is-equiv-is-injective-is-equivalence-injective =
+    is-equiv-map-implicit-Π-is-fiberwise-equiv
+      ( λ x →
+        is-equiv-map-implicit-Π-is-fiberwise-equiv
+          ( λ y →
+            is-equiv-precomp-is-equiv
+              ( equiv-eq)
+              ( univalence (P x) (P y))
+              ( x ＝ y)))
+
+  equiv-is-injective-is-equivalence-injective :
+    is-equivalence-injective P ≃ is-injective P
+  pr1 equiv-is-injective-is-equivalence-injective =
+    is-injective-is-equivalence-injective
+  pr2 equiv-is-injective-is-equivalence-injective =
+    is-equiv-is-injective-is-equivalence-injective
+
+  equiv-is-equivalence-injective-is-injective :
+    is-injective P ≃ is-equivalence-injective P
+  equiv-is-equivalence-injective-is-injective =
+    inv-equiv equiv-is-injective-is-equivalence-injective
+```
+
+### For a type family over a set, being equivalence injective is a property
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (is-set-A : is-set A) (P : A → UU l2)
+  where
+
+  is-prop-is-equivalence-injective : is-prop (is-equivalence-injective P)
+  is-prop-is-equivalence-injective =
+    is-prop-iterated-implicit-Π 2 (λ x y → is-prop-function-type (is-set-A x y))
+
+  is-equivalence-injective-Prop : Prop (l1 ⊔ l2)
+  pr1 is-equivalence-injective-Prop = is-equivalence-injective P
+  pr2 is-equivalence-injective-Prop = is-prop-is-equivalence-injective
+```
diff --git a/src/group-theory/symmetric-groups.lagda.md b/src/group-theory/symmetric-groups.lagda.md
index 69d230a6f6..282ff09a2f 100644
--- a/src/group-theory/symmetric-groups.lagda.md
+++ b/src/group-theory/symmetric-groups.lagda.md
@@ -147,8 +147,10 @@ module _
 
   iso-symmetric-group-equiv-Set :
     iso-Group (symmetric-Group X) (symmetric-Group Y)
-  pr1 iso-symmetric-group-equiv-Set = hom-symmetric-group-equiv-Set
-  pr1 (pr2 iso-symmetric-group-equiv-Set) = hom-inv-symmetric-group-equiv-Set
+  pr1 iso-symmetric-group-equiv-Set =
+    hom-symmetric-group-equiv-Set
+  pr1 (pr2 iso-symmetric-group-equiv-Set) =
+    hom-inv-symmetric-group-equiv-Set
   pr1 (pr2 (pr2 iso-symmetric-group-equiv-Set)) =
     is-section-hom-inv-symmetric-group-equiv-Set
   pr2 (pr2 (pr2 iso-symmetric-group-equiv-Set)) =
diff --git a/src/univalent-combinatorics/double-counting.lagda.md b/src/univalent-combinatorics/double-counting.lagda.md
index 2b78897478..a6a55dcc85 100644
--- a/src/univalent-combinatorics/double-counting.lagda.md
+++ b/src/univalent-combinatorics/double-counting.lagda.md
@@ -30,8 +30,8 @@ abstract
     {l1 l2 : Level} {A : UU l1} {B : UU l2} (count-A : count A)
     (count-B : count B) (e : A ≃ B) →
     Id (number-of-elements-count count-A) (number-of-elements-count count-B)
-  double-counting-equiv (pair k f) (pair l g) e =
-    is-injective-Fin ((inv-equiv g ∘e e) ∘e f)
+  double-counting-equiv (k , f) (l , g) e =
+    is-equivalence-injective-Fin (inv-equiv g ∘e e ∘e f)
 
 abstract
   double-counting :
diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md
index eadaae7c67..8fdc0f7f01 100644
--- a/src/univalent-combinatorics/finite-types.lagda.md
+++ b/src/univalent-combinatorics/finite-types.lagda.md
@@ -84,11 +84,11 @@ abstract
 𝔽 l = Σ (UU l) is-finite
 
 type-𝔽 : {l : Level} → 𝔽 l → UU l
-type-𝔽 X = pr1 X
+type-𝔽 = pr1
 
 is-finite-type-𝔽 :
   {l : Level} (X : 𝔽 l) → is-finite (type-𝔽 X)
-is-finite-type-𝔽 X = pr2 X
+is-finite-type-𝔽 = pr2
 ```
 
 ### Types with cardinality `k`
@@ -96,11 +96,11 @@ is-finite-type-𝔽 X = pr2 X
 ```agda
 has-cardinality-Prop :
   {l : Level} → ℕ → UU l → Prop l
-has-cardinality-Prop k X = mere-equiv-Prop (Fin k) X
+has-cardinality-Prop k = mere-equiv-Prop (Fin k)
 
 has-cardinality :
   {l : Level} → ℕ → UU l → UU l
-has-cardinality k X = mere-equiv (Fin k) X
+has-cardinality k = mere-equiv (Fin k)
 ```
 
 ### The type of all types of cardinality `k` of a given universe level
@@ -110,13 +110,13 @@ UU-Fin : (l : Level) → ℕ → UU (lsuc l)
 UU-Fin l k = Σ (UU l) (mere-equiv (Fin k))
 
 type-UU-Fin : {l : Level} (k : ℕ) → UU-Fin l k → UU l
-type-UU-Fin k X = pr1 X
+type-UU-Fin k = pr1
 
 abstract
   has-cardinality-type-UU-Fin :
     {l : Level} (k : ℕ) (X : UU-Fin l k) →
     mere-equiv (Fin k) (type-UU-Fin k X)
-  has-cardinality-type-UU-Fin k X = pr2 X
+  has-cardinality-type-UU-Fin k = pr2
 ```
 
 ### Types of finite cardinality
@@ -311,11 +311,12 @@ abstract
     eq-type-subtype
       ( λ k → mere-equiv-Prop (Fin k) X)
       ( apply-universal-property-trunc-Prop K
-        ( pair (Id k l) (is-set-ℕ k l))
+        ( Id-Prop ℕ-Set k l)
         ( λ (e : Fin k ≃ X) →
           apply-universal-property-trunc-Prop L
-            ( pair (Id k l) (is-set-ℕ k l))
-            ( λ (f : Fin l ≃ X) → is-injective-Fin ((inv-equiv f) ∘e e))))
+            ( Id-Prop ℕ-Set k l)
+            ( λ (f : Fin l ≃ X) →
+              is-equivalence-injective-Fin (inv-equiv f ∘e e))))
 
 abstract
   is-prop-has-finite-cardinality :
@@ -341,7 +342,7 @@ module _
     is-finite-has-finite-cardinality (pair k K) =
       apply-universal-property-trunc-Prop K
         ( is-finite-Prop X)
-        ( is-finite-count ∘ (pair k))
+        ( is-finite-count ∘ pair k)
 
   abstract
     is-finite-has-cardinality : (k : ℕ) → has-cardinality k X → is-finite X
@@ -380,7 +381,8 @@ module _
             ( number-of-elements-count e)
             ( number-of-elements-is-finite g))
         ( λ g →
-          ( is-injective-Fin ((inv-equiv (equiv-count g)) ∘e (equiv-count e))) ∙
+          ( is-equivalence-injective-Fin
+            ( inv-equiv (equiv-count g) ∘e equiv-count e)) ∙
           ( ap pr1
             ( eq-is-prop' is-prop-has-finite-cardinality
               ( has-finite-cardinality-count g)
@@ -408,7 +410,7 @@ eq-cardinality H K =
     ( λ e →
       apply-universal-property-trunc-Prop K
         ( Id-Prop ℕ-Set _ _)
-        ( λ f → is-injective-Fin (inv-equiv f ∘e e)))
+        ( λ f → is-equivalence-injective-Fin (inv-equiv f ∘e e)))
 ```
 
 ### Any finite type is a set
diff --git a/src/univalent-combinatorics/repetitions-of-values.lagda.md b/src/univalent-combinatorics/repetitions-of-values.lagda.md
index 26fc1db429..18cc0d5e52 100644
--- a/src/univalent-combinatorics/repetitions-of-values.lagda.md
+++ b/src/univalent-combinatorics/repetitions-of-values.lagda.md
@@ -129,7 +129,7 @@ is-decidable-has-repetition-of-values-Fin k l f =
 ```text
 is-injective-map-Fin-zero-Fin :
   {k : ℕ} (f : Fin zero-ℕ → Fin k) → is-injective f
-is-injective-map-Fin-zero-Fin f {()} {y}
+is-injective-map-Fin-zero-Fin f {()}
 
 is-injective-map-Fin-one-Fin : {k : ℕ} (f : Fin 1 → Fin k) → is-injective f
 is-injective-map-Fin-one-Fin f {inr star} {inr star} p = refl
diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md
index ee86b556ee..aec18df6b8 100644
--- a/src/univalent-combinatorics/standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/standard-finite-types.lagda.md
@@ -20,6 +20,7 @@ open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.empty-types
 open import foundation.equality-coproduct-types
+open import foundation.equivalence-injective-type-families
 open import foundation.equivalences
 open import foundation.equivalences-maybe
 open import foundation.function-types
@@ -430,12 +431,18 @@ leq-nat-succ-Fin (succ-ℕ k) (inr star) =
 
 ```agda
 abstract
-  is-injective-Fin : {k l : ℕ} → (Fin k ≃ Fin l) → k ＝ l
-  is-injective-Fin {zero-ℕ} {zero-ℕ} e = refl
-  is-injective-Fin {zero-ℕ} {succ-ℕ l} 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-injective-Fin {succ-ℕ k} {zero-ℕ} e =
+  is-equivalence-injective-Fin {succ-ℕ k} {zero-ℕ} e =
     ex-falso (map-equiv e (zero-Fin k))
-  is-injective-Fin {succ-ℕ k} {succ-ℕ l} e =
-    ap succ-ℕ (is-injective-Fin (equiv-equiv-Maybe e))
+  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
 ```