From 6196a04449354b2b055097c0c189a76cea0b4581 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 25 Jan 2024 12:39:44 +0100
Subject: [PATCH 1/6] equivalence injective type families

---
 .../integers.lagda.md                         |  14 +--
 .../modular-arithmetic.lagda.md               |  16 +--
 src/foundation-core/function-types.lagda.md   |   8 ++
 ...oriality-dependent-function-types.lagda.md |  19 +++-
 src/foundation.lagda.md                       |   1 +
 .../injective-type-families.lagda.md          | 100 ++++++++++++++++++
 src/group-theory/symmetric-groups.lagda.md    |   6 +-
 .../double-counting.lagda.md                  |   4 +-
 .../finite-types.lagda.md                     |  25 ++---
 .../repetitions-of-values.lagda.md            |   2 +-
 .../standard-finite-types.lagda.md            |  18 ++--
 11 files changed, 172 insertions(+), 41 deletions(-)
 create mode 100644 src/foundation/injective-type-families.lagda.md

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 d2ccfdb959..f3d0938b22 100644
--- a/src/foundation-core/functoriality-dependent-function-types.lagda.md
+++ b/src/foundation-core/functoriality-dependent-function-types.lagda.md
@@ -69,7 +69,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
@@ -81,15 +81,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 859535f3cc..0d0437c032 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -179,6 +179,7 @@ open import foundation.induction-principle-propositional-truncation public
 open import foundation.inhabited-subtypes public
 open import foundation.inhabited-types public
 open import foundation.injective-maps public
+open import foundation.injective-type-families public
 open import foundation.interchange-law public
 open import foundation.intersections-subtypes public
 open import foundation.inverse-sequential-diagrams public
diff --git a/src/foundation/injective-type-families.lagda.md b/src/foundation/injective-type-families.lagda.md
new file mode 100644
index 0000000000..fed3d0fe40
--- /dev/null
+++ b/src/foundation/injective-type-families.lagda.md
@@ -0,0 +1,100 @@
+# Injective type families
+
+```agda
+module foundation.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
+
+A type family `P : A → UU` is
+{{#concept "injective" Disambiguation="type family"}} if it is
+[injective as a map](foundation-core.injective-maps.md). However, we can also
+consider injectivity with respect to
+[equivalences of types](foundation-core.equivalences.md), which we dub
+{{#concept "equivalence injectivity" Disambiguation="type family" Agda=is-equiv-injective}}.
+By [univalence](foundation-core.univalence.md), these two structures are
+equivalent, but more generally every equivalence injective type family must
+always be injective as a map.
+
+## Definition
+
+### Equivalence injective type families
+
+```agda
+is-equiv-injective : {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2)
+is-equiv-injective {A = A} P = {x y : A} → P x ≃ P y → x ＝ y
+```
+
+## Properties
+
+### Equivalence injective type families are injective
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {P : A → UU l2}
+  where
+
+  is-injective-is-equiv-injective : is-equiv-injective P → is-injective P
+  is-injective-is-equiv-injective H = H ∘ equiv-eq
+
+  is-equiv-injective-is-injective : is-injective P → is-equiv-injective P
+  is-equiv-injective-is-injective H = H ∘ eq-equiv
+
+  is-equiv-is-injective-is-equiv-injective :
+    is-equiv is-injective-is-equiv-injective
+  is-equiv-is-injective-is-equiv-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-equiv-injective : is-equiv-injective P ≃ is-injective P
+  pr1 equiv-is-injective-is-equiv-injective =
+    is-injective-is-equiv-injective
+  pr2 equiv-is-injective-is-equiv-injective =
+    is-equiv-is-injective-is-equiv-injective
+
+  equiv-is-equiv-injective-is-injective : is-injective P ≃ is-equiv-injective P
+  equiv-is-equiv-injective-is-injective =
+    inv-equiv equiv-is-injective-is-equiv-injective
+```
+
+### For a map between sets, 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-equiv-injective : is-prop (is-equiv-injective P)
+  is-prop-is-equiv-injective =
+    is-prop-iterated-implicit-Π 2 (λ x y → is-prop-function-type (is-set-A x y))
+
+  is-equiv-injective-Prop : Prop (l1 ⊔ l2)
+  pr1 is-equiv-injective-Prop = is-equiv-injective P
+  pr2 is-equiv-injective-Prop = is-prop-is-equiv-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..5476484a95 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-equiv-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..7ccc11a0a3 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,11 @@ 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-equiv-injective-Fin (inv-equiv f ∘e e))))
 
 abstract
   is-prop-has-finite-cardinality :
@@ -341,7 +341,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 +380,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-equiv-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 +409,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-equiv-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..4a075a004e 100644
--- a/src/univalent-combinatorics/standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/standard-finite-types.lagda.md
@@ -26,6 +26,7 @@ open import foundation.function-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.injective-maps
+open import foundation.injective-type-families
 open import foundation.negated-equality
 open import foundation.negation
 open import foundation.noncontractible-types
@@ -430,12 +431,17 @@ 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-equiv-injective-Fin : is-equiv-injective Fin
+  is-equiv-injective-Fin {zero-ℕ} {zero-ℕ} e =
+    refl
+  is-equiv-injective-Fin {zero-ℕ} {succ-ℕ l} e =
     ex-falso (map-inv-equiv e (zero-Fin l))
-  is-injective-Fin {succ-ℕ k} {zero-ℕ} e =
+  is-equiv-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-equiv-injective-Fin {succ-ℕ k} {succ-ℕ l} e =
+    ap succ-ℕ (is-equiv-injective-Fin (equiv-equiv-Maybe e))
+
+abstract
+  is-injective-Fin : is-injective Fin
+  is-injective-Fin = is-injective-is-equiv-injective is-equiv-injective-Fin
 ```

From 7ef885fb600e69ec3598273a4bc8d93959d43341 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 26 Jan 2024 22:45:23 +0100
Subject: [PATCH 2/6] review

---
 src/foundation.lagda.md                       |   2 +-
 ...uivalence-injective-type-families.lagda.md | 105 ++++++++++++++++++
 .../injective-type-families.lagda.md          | 100 -----------------
 .../double-counting.lagda.md                  |   2 +-
 .../finite-types.lagda.md                     |   7 +-
 .../standard-finite-types.lagda.md            |  15 +--
 6 files changed, 119 insertions(+), 112 deletions(-)
 create mode 100644 src/foundation/equivalence-injective-type-families.lagda.md
 delete mode 100644 src/foundation/injective-type-families.lagda.md

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 0d0437c032..b886cb30af 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -129,6 +129,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-inverse-sequential-diagrams public
@@ -179,7 +180,6 @@ open import foundation.induction-principle-propositional-truncation public
 open import foundation.inhabited-subtypes public
 open import foundation.inhabited-types public
 open import foundation.injective-maps public
-open import foundation.injective-type-families public
 open import foundation.interchange-law public
 open import foundation.intersections-subtypes public
 open import foundation.inverse-sequential-diagrams 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..aebd272d43
--- /dev/null
+++ b/src/foundation/equivalence-injective-type-families.lagda.md
@@ -0,0 +1,105 @@
+# 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 can say a type family `P : A → 𝒰` is
+{{#concept "injective" Disambiguation="type family"}} if it is
+[injective as a map](foundation-core.injective-maps.md). However, we can also
+consider injectivity with respect to
+[equivalences of types](foundation-core.equivalences.md), which we dub
+{{#concept "equivalence injectivity" Disambiguation="type family" Agda=is-equivalence-injective}}.
+By [univalence](foundation-core.univalence.md), these two
+[structures](foundation.structure.md) are equivalent, but more generally every
+equivalence injective type family must always be injective as a map.
+
+## 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 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 map between sets, 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/foundation/injective-type-families.lagda.md b/src/foundation/injective-type-families.lagda.md
deleted file mode 100644
index fed3d0fe40..0000000000
--- a/src/foundation/injective-type-families.lagda.md
+++ /dev/null
@@ -1,100 +0,0 @@
-# Injective type families
-
-```agda
-module foundation.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
-
-A type family `P : A → UU` is
-{{#concept "injective" Disambiguation="type family"}} if it is
-[injective as a map](foundation-core.injective-maps.md). However, we can also
-consider injectivity with respect to
-[equivalences of types](foundation-core.equivalences.md), which we dub
-{{#concept "equivalence injectivity" Disambiguation="type family" Agda=is-equiv-injective}}.
-By [univalence](foundation-core.univalence.md), these two structures are
-equivalent, but more generally every equivalence injective type family must
-always be injective as a map.
-
-## Definition
-
-### Equivalence injective type families
-
-```agda
-is-equiv-injective : {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2)
-is-equiv-injective {A = A} P = {x y : A} → P x ≃ P y → x ＝ y
-```
-
-## Properties
-
-### Equivalence injective type families are injective
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} {P : A → UU l2}
-  where
-
-  is-injective-is-equiv-injective : is-equiv-injective P → is-injective P
-  is-injective-is-equiv-injective H = H ∘ equiv-eq
-
-  is-equiv-injective-is-injective : is-injective P → is-equiv-injective P
-  is-equiv-injective-is-injective H = H ∘ eq-equiv
-
-  is-equiv-is-injective-is-equiv-injective :
-    is-equiv is-injective-is-equiv-injective
-  is-equiv-is-injective-is-equiv-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-equiv-injective : is-equiv-injective P ≃ is-injective P
-  pr1 equiv-is-injective-is-equiv-injective =
-    is-injective-is-equiv-injective
-  pr2 equiv-is-injective-is-equiv-injective =
-    is-equiv-is-injective-is-equiv-injective
-
-  equiv-is-equiv-injective-is-injective : is-injective P ≃ is-equiv-injective P
-  equiv-is-equiv-injective-is-injective =
-    inv-equiv equiv-is-injective-is-equiv-injective
-```
-
-### For a map between sets, 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-equiv-injective : is-prop (is-equiv-injective P)
-  is-prop-is-equiv-injective =
-    is-prop-iterated-implicit-Π 2 (λ x y → is-prop-function-type (is-set-A x y))
-
-  is-equiv-injective-Prop : Prop (l1 ⊔ l2)
-  pr1 is-equiv-injective-Prop = is-equiv-injective P
-  pr2 is-equiv-injective-Prop = is-prop-is-equiv-injective
-```
diff --git a/src/univalent-combinatorics/double-counting.lagda.md b/src/univalent-combinatorics/double-counting.lagda.md
index 5476484a95..a6a55dcc85 100644
--- a/src/univalent-combinatorics/double-counting.lagda.md
+++ b/src/univalent-combinatorics/double-counting.lagda.md
@@ -31,7 +31,7 @@ abstract
     (count-B : count B) (e : A ≃ B) →
     Id (number-of-elements-count count-A) (number-of-elements-count count-B)
   double-counting-equiv (k , f) (l , g) e =
-    is-equiv-injective-Fin (inv-equiv g ∘e e ∘e f)
+    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 7ccc11a0a3..8fdc0f7f01 100644
--- a/src/univalent-combinatorics/finite-types.lagda.md
+++ b/src/univalent-combinatorics/finite-types.lagda.md
@@ -315,7 +315,8 @@ abstract
         ( λ (e : Fin k ≃ X) →
           apply-universal-property-trunc-Prop L
             ( Id-Prop ℕ-Set k l)
-            ( λ (f : Fin l ≃ X) → is-equiv-injective-Fin (inv-equiv f ∘e e))))
+            ( λ (f : Fin l ≃ X) →
+              is-equivalence-injective-Fin (inv-equiv f ∘e e))))
 
 abstract
   is-prop-has-finite-cardinality :
@@ -380,7 +381,7 @@ module _
             ( number-of-elements-count e)
             ( number-of-elements-is-finite g))
         ( λ g →
-          ( is-equiv-injective-Fin
+          ( is-equivalence-injective-Fin
             ( inv-equiv (equiv-count g) ∘e equiv-count e)) ∙
           ( ap pr1
             ( eq-is-prop' is-prop-has-finite-cardinality
@@ -409,7 +410,7 @@ eq-cardinality H K =
     ( λ e →
       apply-universal-property-trunc-Prop K
         ( Id-Prop ℕ-Set _ _)
-        ( λ f → is-equiv-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/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md
index 4a075a004e..ffae18e9eb 100644
--- a/src/univalent-combinatorics/standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/standard-finite-types.lagda.md
@@ -431,17 +431,18 @@ leq-nat-succ-Fin (succ-ℕ k) (inr star) =
 
 ```agda
 abstract
-  is-equiv-injective-Fin : is-equiv-injective Fin
-  is-equiv-injective-Fin {zero-ℕ} {zero-ℕ} e =
+  is-equivalence-injective-Fin : is-equivalence-injective Fin
+  is-equivalence-injective-Fin {zero-ℕ} {zero-ℕ} e =
     refl
-  is-equiv-injective-Fin {zero-ℕ} {succ-ℕ l} e =
+  is-equivalence-injective-Fin {zero-ℕ} {succ-ℕ l} e =
     ex-falso (map-inv-equiv e (zero-Fin l))
-  is-equiv-injective-Fin {succ-ℕ k} {zero-ℕ} e =
+  is-equivalence-injective-Fin {succ-ℕ k} {zero-ℕ} e =
     ex-falso (map-equiv e (zero-Fin k))
-  is-equiv-injective-Fin {succ-ℕ k} {succ-ℕ l} e =
-    ap succ-ℕ (is-equiv-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-equiv-injective is-equiv-injective-Fin
+  is-injective-Fin =
+    is-injective-is-equivalence-injective is-equivalence-injective-Fin
 ```

From 07d34f7cb5546e0598d5a4a289f70dc2607ad56c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 26 Jan 2024 23:16:11 +0100
Subject: [PATCH 3/6] fix import

---
 src/univalent-combinatorics/standard-finite-types.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md
index ffae18e9eb..aec18df6b8 100644
--- a/src/univalent-combinatorics/standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/standard-finite-types.lagda.md
@@ -20,13 +20,13 @@ 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
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.injective-maps
-open import foundation.injective-type-families
 open import foundation.negated-equality
 open import foundation.negation
 open import foundation.noncontractible-types

From a4fda1401a99ab4cac27396b4d0434c694e9c040 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sat, 27 Jan 2024 19:28:47 +0100
Subject: [PATCH 4/6] wip prose

---
 ...equivalence-injective-type-families.lagda.md | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/foundation/equivalence-injective-type-families.lagda.md b/src/foundation/equivalence-injective-type-families.lagda.md
index aebd272d43..09a517dc0c 100644
--- a/src/foundation/equivalence-injective-type-families.lagda.md
+++ b/src/foundation/equivalence-injective-type-families.lagda.md
@@ -26,15 +26,14 @@ open import foundation-core.sets
 
 ## Idea
 
-We can say a type family `P : A → 𝒰` is
-{{#concept "injective" Disambiguation="type family"}} if it is
-[injective as a map](foundation-core.injective-maps.md). However, we can also
-consider injectivity with respect to
-[equivalences of types](foundation-core.equivalences.md), which we dub
-{{#concept "equivalence injectivity" Disambiguation="type family" Agda=is-equivalence-injective}}.
-By [univalence](foundation-core.univalence.md), these two
-[structures](foundation.structure.md) are equivalent, but more generally every
-equivalence injective type family must always be injective as a map.
+We say a type family `P` is
+{{#concept "equivalence injective" Disambiguation="type family" Agda=is-equivalence-injective}}
+if for every [equivalences 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.
 
 ## Definition
 

From c348a2f73321735d8254be17c8e66253bcd6adac Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 28 Jan 2024 13:40:02 +0100
Subject: [PATCH 5/6] add note about injective types

---
 .../equivalence-injective-type-families.lagda.md     | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/foundation/equivalence-injective-type-families.lagda.md b/src/foundation/equivalence-injective-type-families.lagda.md
index 09a517dc0c..1ac92b3347 100644
--- a/src/foundation/equivalence-injective-type-families.lagda.md
+++ b/src/foundation/equivalence-injective-type-families.lagda.md
@@ -28,13 +28,19 @@ open import foundation-core.sets
 
 We say a type family `P` is
 {{#concept "equivalence injective" Disambiguation="type family" Agda=is-equivalence-injective}}
-if for every [equivalences 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
+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

From cf542b4b8f707dc571b769cbf81ff0f4f0e0aef8 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 28 Jan 2024 13:41:34 +0100
Subject: [PATCH 6/6] fix headers

---
 src/foundation/equivalence-injective-type-families.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/foundation/equivalence-injective-type-families.lagda.md b/src/foundation/equivalence-injective-type-families.lagda.md
index 1ac92b3347..d565eb4308 100644
--- a/src/foundation/equivalence-injective-type-families.lagda.md
+++ b/src/foundation/equivalence-injective-type-families.lagda.md
@@ -53,7 +53,7 @@ is-equivalence-injective {A = A} P = {x y : A} → P x ≃ P y → x ＝ y
 
 ## Properties
 
-### Equivalence injective type families are injective maps
+### Equivalence injective type families are injective as maps
 
 ```agda
 module _
@@ -93,7 +93,7 @@ module _
     inv-equiv equiv-is-injective-is-equivalence-injective
 ```
 
-### For a map between sets, being equivalence injective is a property
+### For a type family over a set, being equivalence injective is a property
 
 ```agda
 module _