The universal property of identity types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2022-01-31.
Last modified on 2023-09-11.

module foundation.universal-property-identity-types where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.axiom-l
open import foundation.dependent-pair-types
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.type-theoretic-principle-of-choice
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.contractible-types
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.injective-maps
open import foundation-core.propositional-maps
open import foundation-core.propositions

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

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

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

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

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

The proof that axiom L 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 axiom L at the second step.

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

  is-emb-Id-axiom-L : is-emb (Id {A = A})
  is-emb-Id-axiom-L a =
    fundamental-theorem-id
      ( pair
        ( pair a refl)
        ( λ _ →
          is-injective-emb
            ( emb-fiber a)
            ( eq-is-contr (is-contr-total-path a))))
      ( λ _ → ap Id)
    where
    emb-fiber : (a : A) → fiber' Id (Id a) ↪ Σ A (Id a)
    emb-fiber a =
      comp-emb
        ( comp-emb
          ( emb-equiv
            ( equiv-tot
              ( λ x →
                ( equiv-ev-refl x) ∘e
                ( ( equiv-inclusion-is-full-subtype
                    ( Π-Prop A ∘ (is-equiv-Prop ∘_))
                    ( fundamental-theorem-id (is-contr-total-path a))) ∘e
                  ( distributive-Π-Σ)))))
          ( emb-Σ
            ( λ x → (y : A) → Id x y ≃ Id a y)
            ( id-emb)
            ( λ x →
              comp-emb
                ( emb-Π (λ y → emb-L L (Id x y) (Id a y)))
                ( emb-equiv equiv-funext))))
        ( emb-equiv (inv-equiv (equiv-fiber Id (Id a))))

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-axiom-L (axiom-L-univalence univalence) 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)

See also

References

Recent changes