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


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.


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

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

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

  emb-fiber-Id-preunivalent-Id :
    (a : A)  fiber' Id (Id a)  Σ A (Id a)
  emb-fiber-Id-preunivalent-Id a =
      ( 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 
              ( 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 =
      ( ( a , refl) ,
        ( λ _ 
            ( emb-fiber-Id-preunivalent-Id a)
            ( eq-is-contr (is-torsorial-Id a))))
      ( λ _  ap Id)

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

  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)

  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}

  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) =
      ( Σ A  b  (x : A)  (b  x)  (a  x)))
      ( equiv-tot
        ( λ b 
            ( λ 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-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)

    is-torsorial-pointed-fam-equiv-is-torsorial :
        ( λ (e : (x : A)  (a  x)  B x) 
          map-equiv (e a) refl  b)
    is-torsorial-pointed-fam-equiv-is-torsorial =
        ( fiber (ev-refl a {B = λ x _  B x}) b)
        ( equiv-Σ _
          ( inv-equiv
            ( equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B))
          ( λ h 
              ( 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


Martín Hötzel Escardó and contributors. TypeTopology. GitHub repository. Agda development. URL:

Recent changes