Equivalence injective type families

Content created by Fredrik Bakke.

Created on 2024-01-28.
Last modified on 2024-01-28.

module foundation.equivalence-injective-type-families where
Imports 
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

Idea

We say a type family P is equivalence injective if for every equivalence of types P x ≃ P y we have x ＝ y . By univalence, the structure of being equivalence injective is equivalent to being injective as a map, 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, TypeTopology).

Definition

Equivalence injective type families

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

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

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

Recent changes