Equivalence injective type families

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
 ```

src/elementary-number-theory/modular-arithmetic.lagda.md

@@ -100,15 +100,15 @@ 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
 ℤ-Mod-Discrete-Type zero-ℕ = ℤ-Discrete-Type
 ℤ-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

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

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)

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

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
+```

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)) =

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 :