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

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

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

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

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-equiv-injective-Fin (inv-equiv g ∘e e ∘e f)
 
 abstract
   double-counting :

src/univalent-combinatorics/finite-types.lagda.md

@@ -84,23 +84,23 @@ 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`
 
 ```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