The universal property of identity types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, Vojtěch Štěpančík, fernabnor and louismntnu.

Created on 2022-01-31.
Last modified on 2024-06-06.

module foundation.universal-property-identity-types where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.dependent-universal-property-equivalences
open import foundation.embeddings
open import foundation.equivalences
open import foundation.full-subtypes
open import foundation.function-extensionality
open import foundation.functoriality-dependent-function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.preunivalence
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.families-of-equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.injective-maps
open import foundation-core.propositional-maps
open import foundation-core.propositions
open import foundation-core.torsorial-type-families

Idea

The universal property of identity types characterizes families of maps out of the identity type. This universal property is also known as the type theoretic Yoneda lemma.

Theorem

ev-refl :
  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → a ＝ x → UU l2} →
  ((x : A) (p : a ＝ x) → B x p) → B a refl
ev-refl a f = f a refl

ev-refl' :
  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → x ＝ a → UU l2} →
  ((x : A) (p : x ＝ a) → B x p) → B a refl
ev-refl' a f = f a refl

abstract
  is-equiv-ev-refl :
    {l1 l2 : Level} {A : UU l1} (a : A)
    {B : (x : A) → a ＝ x → UU l2} → is-equiv (ev-refl a {B})
  is-equiv-ev-refl a =
    is-equiv-is-invertible
      ( ind-Id a _)
      ( λ b → refl)
      ( λ f → eq-htpy
        ( λ x → eq-htpy
          ( ind-Id a
            ( λ x' p' → ind-Id a _ (f a refl) x' p' ＝ f x' p')
            ( refl) x)))

equiv-ev-refl :
  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → a ＝ x → UU l2} →
  ((x : A) (p : a ＝ x) → B x p) ≃ (B a refl)
pr1 (equiv-ev-refl a) = ev-refl a
pr2 (equiv-ev-refl a) = is-equiv-ev-refl a

equiv-ev-refl' :
  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → x ＝ a → UU l2} →
  ((x : A) (p : x ＝ a) → B x p) ≃ B a refl
equiv-ev-refl' a {B} =
  ( equiv-ev-refl a) ∘e
  ( equiv-Π-equiv-family (λ x → equiv-precomp-Π (equiv-inv a x) (B x)))

is-equiv-ev-refl' :
  {l1 l2 : Level} {A : UU l1} (a : A)
  {B : (x : A) → x ＝ a → UU l2} → is-equiv (ev-refl' a {B})
is-equiv-ev-refl' a = is-equiv-map-equiv (equiv-ev-refl' a)

The type of fiberwise maps from Id a to a torsorial type family B is equivalent to the type of fiberwise equivalences

Note that the type of fiberwise equivalences is a subtype of the type of fiberwise maps. By the fundamental theorem of identity types, it is a full subtype, hence it is equivalent to the whole type of fiberwise maps.

module _
  {l1 l2 : Level} {A : UU l1} (a : A) {B : A → UU l2}
  (is-torsorial-B : is-torsorial B)
  where

  equiv-fam-map-fam-equiv-is-torsorial :
    ((x : A) → (a ＝ x) ≃ B x) ≃ ((x : A) → (a ＝ x) → B x)
  equiv-fam-map-fam-equiv-is-torsorial =
    ( equiv-inclusion-is-full-subtype
      ( λ h → Π-Prop A (λ a → is-equiv-Prop (h a)))
      ( fundamental-theorem-id is-torsorial-B)) ∘e
    ( equiv-fiberwise-equiv-fam-equiv _ _)

Id : A → (A → 𝒰) is an embedding

We first show that the preunivalence axiom implies that the map Id : A → (A → 𝒰) is an embedding. Since the univalence axiom implies preunivalence, it follows that Id : A → (A → 𝒰) is an embedding under the postulates of agda-unimath.

Preunivalence implies that Id : A → (A → 𝒰) is an embedding

The proof that preunivalence implies that Id : A → (A → 𝒰) is an embedding proceeds via the fundamental theorem of identity types by showing that the fiber of Id at Id a is contractible for each a : A. To see this, we first note that this fiber has an element (a , refl). Therefore it suffices to show that this fiber is a proposition. We do this by constructing an embedding

  fiber Id (Id a) ↪ Σ A (Id a).

Since the codomain of this embedding is contractible, the claim follows. The above embedding is constructed as the composite of the following embeddings

  Σ (x : A), Id x ＝ Id a
    ↪ Σ (x : A), (y : A) → (x ＝ y) ＝ (a ＝ y)
    ↪ Σ (x : A), (y : A) → (x ＝ y) ≃ (a ＝ y)
    ↪ Σ (x : A), Σ (e : (y : A) → (x ＝ y) → (a ＝ y)), (y : A) → is-equiv (e y)
    ↪ Σ (x : A), (y : A) → (x ＝ y) → (a ＝ y)
    ↪ Σ (x : A), a ＝ x.

In this composite, we used preunivalence at the second step.

module _
  {l : Level} (A : UU l)
  (L : (a x y : A) → instance-preunivalence (Id x y) (Id a y))
  where

  emb-fiber-Id-preunivalent-Id :
    (a : A) → fiber' Id (Id a) ↪ Σ A (Id a)
  emb-fiber-Id-preunivalent-Id a =
    comp-emb
      ( comp-emb
        ( emb-equiv
          ( equiv-tot
            ( λ x →
              ( equiv-ev-refl x) ∘e
              ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a)))))
        ( emb-tot
          ( λ x →
            comp-emb
              ( emb-Π (λ y → _ , L a x y))
              ( emb-equiv equiv-funext))))
      ( emb-equiv (inv-equiv (equiv-fiber Id (Id a))))

  is-emb-Id-preunivalent-Id : is-emb (Id {A = A})
  is-emb-Id-preunivalent-Id a =
    fundamental-theorem-id
      ( ( a , refl) ,
        ( λ _ →
          is-injective-emb
            ( emb-fiber-Id-preunivalent-Id a)
            ( eq-is-contr (is-torsorial-Id a))))
      ( λ _ → ap Id)

module _
  (L : preunivalence-axiom) {l : Level} (A : UU l)
  where

  is-emb-Id-preunivalence-axiom : is-emb (Id {A = A})
  is-emb-Id-preunivalence-axiom =
    is-emb-Id-preunivalent-Id A (λ a x y → L (Id x y) (Id a y))

Id : A → (A → 𝒰) is an embedding

module _
  {l : Level} (A : UU l)
  where

  is-emb-Id : is-emb (Id {A = A})
  is-emb-Id = is-emb-Id-preunivalence-axiom preunivalence A

For any type family B over A, the type of pairs (a , e) consisting of a : A and a family of equivalences e : (x : A) → (a ＝ x) ≃ B x is a proposition

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  is-proof-irrelevant-total-family-of-equivalences-Id :
    is-proof-irrelevant (Σ A (λ a → (x : A) → (a ＝ x) ≃ B x))
  is-proof-irrelevant-total-family-of-equivalences-Id (a , e) =
    is-contr-equiv
      ( Σ A (λ b → (x : A) → (b ＝ x) ≃ (a ＝ x)))
      ( equiv-tot
        ( λ b →
          equiv-Π-equiv-family
            ( λ x → equiv-postcomp-equiv (inv-equiv (e x)) (b ＝ x))))
      ( is-contr-equiv'
        ( fiber Id (Id a))
        ( equiv-tot
          ( λ b →
            equiv-Π-equiv-family (λ x → equiv-univalence) ∘e equiv-funext))
        ( is-proof-irrelevant-is-prop
          ( is-prop-map-is-emb (is-emb-Id A) (Id a))
          ( a , refl)))

  is-prop-total-family-of-equivalences-Id :
    is-prop (Σ A (λ a → (x : A) → (a ＝ x) ≃ B x))
  is-prop-total-family-of-equivalences-Id =
    is-prop-is-proof-irrelevant
      ( is-proof-irrelevant-total-family-of-equivalences-Id)

The type of point-preserving fiberwise equivalences between Id x and a pointed torsorial type family is contractible

Proof: Since ev-refl is an equivalence, it follows that its fibers are contractible. Explicitly, given a point b : B a, the type of maps h : (x : A) → (a = x) → B x such that h a refl = b is contractible. But the type of fiberwise maps is equivalent to the type of fiberwise equivalences.

module _
  {l1 l2 : Level} {A : UU l1} {a : A} {B : A → UU l2} (b : B a)
  (is-torsorial-B : is-torsorial B)
  where

  abstract
    is-torsorial-pointed-fam-equiv-is-torsorial :
      is-torsorial
        ( λ (e : (x : A) → (a ＝ x) ≃ B x) →
          map-equiv (e a) refl ＝ b)
    is-torsorial-pointed-fam-equiv-is-torsorial =
      is-contr-equiv'
        ( fiber (ev-refl a {B = λ x _ → B x}) b)
        ( equiv-Σ _
          ( inv-equiv
            ( equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B))
          ( λ h →
            equiv-inv-concat
              ( inv
                ( ap
                  ( ev-refl a)
                  ( is-section-map-inv-equiv
                    ( equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B)
                    ( h))))
              ( b)))
        ( is-contr-map-is-equiv
          ( is-equiv-ev-refl a)
          ( b))

See also

References

[Esc]
Martín Hötzel Escardó and contributors. TypeTopology. GitHub repository. Agda development. URL: https://github.com/martinescardo/TypeTopology.

Recent changes