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


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


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


Equivalence injective type families are injective as maps

module _
  {l1 l2 : Level} {A : UU l1} {P : A  UU l2}

  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 =
      ( λ x 
          ( λ y 
              ( 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 =
  pr2 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)

  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