Identity types

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Vojtěch Štěpančík, Eléonore Mangel, Elisabeth Bonnevier, Julian KG, Raymond Baker, fernabnor and louismntnu.

Created on 2022-01-26.
Last modified on 2023-09-29.

module foundation.identity-types where

open import foundation-core.identity-types public
open import foundation.action-on-identifications-functions
open import foundation.binary-equivalences
open import foundation.dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.function-extensionality
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.homotopies


The equality relation on a type is a reflexive relation, with the universal property that it maps uniquely into any other reflexive relation. In type theory, we introduce the identity type as an inductive family of types, where the induction principle can be understood as expressing that the identity type is the least reflexive relation.

The following table lists files that are about identity types and operations on identifications in arbitrary types.

Action on identifications of binary functionsfoundation.action-on-identifications-binary-functions
Action on identifications of dependent functionsfoundation.action-on-identifications-dependent-functions
Action on identifications of functionsfoundation.action-on-identifications-functions
Binary transportfoundation.binary-transport
Commuting hexagons of identificationsfoundation.commuting-hexagons-of-identifications
Commuting squares of identificationsfoundation.commuting-squares-of-identifications
Dependent identifications (foundation)foundation.dependent-identifications
Dependent identifications (foundation-core)foundation-core.dependent-identifications
The fundamental theorem of identity typesfoundation.fundamental-theorem-of-identity-types
Identity systemsfoundation.identity-systems
The identity type (foundation)foundation.identity-types
The identity type (foundation-core)foundation-core.identity-types
Large identity typesfoundation.large-identity-types
Path algebrafoundation.path-algebra
The Regensburg extension of the fundamental theorem of identity typesfoundation.regensburg-extension-fundamental-theorem-of-identity-types
Symmetric identity typesfoundation.symmetric-identity-types
Torsorial type familiesfoundation.torsorial-type-families
Transport along higher identificationsfoundation.transport-along-higher-identifications
Transport along identifications (foundation)foundation.transport-along-identifications
Transport along identifications (foundation-core)foundation-core.transport-along-identifications
The universal property of identity systemsfoundation.universal-property-identity-systems
The universal property of identity typesfoundation.universal-property-identity-types


The Mac Lane pentagon for identity types

Mac-Lane-pentagon :
  {l : Level} {A : UU l} {a b c d e : A}
  (p : a  b) (q : b  c) (r : c  d) (s : d  e) 
  let α₁ = (ap  t  t  s) (assoc p q r))
      α₂ = (assoc p (q  r) s)
      α₃ = (ap  t  p  t) (assoc q r s))
      α₄ = (assoc (p  q) r s)
      α₅ = (assoc p q (r  s))
  ((α₁  α₂)  α₃)  (α₄  α₅)
Mac-Lane-pentagon refl refl refl refl = refl

The groupoidal operations on identity types are equivalences

module _
  {l : Level} {A : UU l}

    is-equiv-inv : (x y : A)  is-equiv  (p : x  y)  inv p)
    is-equiv-inv x y = is-equiv-is-invertible inv inv-inv inv-inv

  equiv-inv : (x y : A)  (x  y)  (y  x)
  pr1 (equiv-inv x y) = inv
  pr2 (equiv-inv x y) = is-equiv-inv x y

  inv-concat : {x y : A} (p : x  y) (z : A)  x  z  y  z
  inv-concat p = concat (inv p)

  is-retraction-inv-concat :
    {x y : A} (p : x  y) (z : A)  (inv-concat p z  concat p z) ~ id
  is-retraction-inv-concat refl z q = refl

  is-section-inv-concat :
    {x y : A} (p : x  y) (z : A)  (concat p z  inv-concat p z) ~ id
  is-section-inv-concat refl z refl = refl

    is-equiv-concat :
      {x y : A} (p : x  y) (z : A)  is-equiv (concat p z)
    is-equiv-concat p z =
        ( inv-concat p z)
        ( is-section-inv-concat p z)
        ( is-retraction-inv-concat p z)

  equiv-concat :
    {x y : A} (p : x  y) (z : A)  (y  z)  (x  z)
  pr1 (equiv-concat p z) = concat p z
  pr2 (equiv-concat p z) = is-equiv-concat p z

  equiv-concat-equiv :
    {x x' : A}  ((y : A)  (x  y)  (x'  y))  (x'  x)
  pr1 (equiv-concat-equiv {x}) e = map-equiv (e x) refl
  pr2 equiv-concat-equiv =
       { refl  refl})
       e  eq-htpy  y  eq-htpy-equiv  { refl  right-unit})))

  inv-concat' : (x : A) {y z : A}  y  z  x  z  x  y
  inv-concat' x q = concat' x (inv q)

  is-retraction-inv-concat' :
    (x : A) {y z : A} (q : y  z)  (inv-concat' x q  concat' x q) ~ id
  is-retraction-inv-concat' x refl refl = refl

  is-section-inv-concat' :
    (x : A) {y z : A} (q : y  z)  (concat' x q  inv-concat' x q) ~ id
  is-section-inv-concat' x refl refl = refl

    is-equiv-concat' :
      (x : A) {y z : A} (q : y  z)  is-equiv (concat' x q)
    is-equiv-concat' x q =
        ( inv-concat' x q)
        ( is-section-inv-concat' x q)
        ( is-retraction-inv-concat' x q)

  equiv-concat' :
    (x : A) {y z : A} (q : y  z)  (x  y)  (x  z)
  pr1 (equiv-concat' x q) = concat' x q
  pr2 (equiv-concat' x q) = is-equiv-concat' x q

is-binary-equiv-concat :
  {l : Level} {A : UU l} {x y z : A} 
  is-binary-equiv  (p : x  y) (q : y  z)  p  q)
pr1 (is-binary-equiv-concat {x = x}) q = is-equiv-concat' x q
pr2 (is-binary-equiv-concat {z = z}) p = is-equiv-concat p z

equiv-binary-concat :
  {l : Level} {A : UU l} {x y z w : A}  (p : x  y) (q : z  w) 
  (y  z)  (x  w)
equiv-binary-concat {x = x} {z = z} p q =
  (equiv-concat' x q) ∘e (equiv-concat p z)

convert-eq-values :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A  B} (H : f ~ g)
  (x y : A)  (f x  f y)  (g x  g y)
convert-eq-values {f = f} {g} H x y =
  ( equiv-concat' (g x) (H y)) ∘e (equiv-concat (inv (H x)) (f y))

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

  is-section-is-injective-concat :
    {x y z : A} (p : x  y) {q r : y  z} (s : (p  q)  (p  r)) 
    ap (concat p z) (is-injective-concat p s)  s
  is-section-is-injective-concat refl refl = refl

  cases-is-section-is-injective-concat' :
    {x y : A} {p q : x  y} (s : p  q) 
    ( ap
      ( concat' x refl)
      ( is-injective-concat' refl (right-unit  (s  inv right-unit)))) 
    ( right-unit  (s  inv right-unit))
  cases-is-section-is-injective-concat' {p = refl} refl = refl

  is-section-is-injective-concat' :
    {x y z : A} (r : y  z) {p q : x  y} (s : (p  r)  (q  r)) 
    ap (concat' x r) (is-injective-concat' r s)  s
  is-section-is-injective-concat' refl s =
    ( ap  u  ap (concat' _ refl) (is-injective-concat' refl u)) (inv α)) 
    ( ( cases-is-section-is-injective-concat'
        ( inv right-unit  (s  right-unit))) 
      ( α))
    α :
      ( ( right-unit) 
        ( ( inv right-unit  (s  right-unit)) 
          ( inv right-unit))) 
      ( s)
    α =
      ( ap
        ( concat right-unit _)
        ( ( assoc (inv right-unit) (s  right-unit) (inv right-unit)) 
          ( ( ap
              ( concat (inv right-unit) _)
              ( ( assoc s right-unit (inv right-unit)) 
                ( ( ap (concat s _) (right-inv right-unit)) 
                  ( right-unit))))))) 
      ( ( inv (assoc right-unit (inv right-unit) s)) 
        ( ( ap (concat' _ s) (right-inv right-unit))))

Transposing inverses is an equivalence

module _
  {l : Level} {A : UU l} {x y z : A}

    is-equiv-left-transpose-eq-concat :
      (p : x  y) (q : y  z) (r : x  z) 
      is-equiv (left-transpose-eq-concat p q r)
    is-equiv-left-transpose-eq-concat refl q r = is-equiv-id

  equiv-left-transpose-eq-concat :
    (p : x  y) (q : y  z) (r : x  z) 
    ((p  q)  r)  (q  ((inv p)  r))
  pr1 (equiv-left-transpose-eq-concat p q r) = left-transpose-eq-concat p q r
  pr2 (equiv-left-transpose-eq-concat p q r) =
    is-equiv-left-transpose-eq-concat p q r

    is-equiv-right-transpose-eq-concat :
      (p : x  y) (q : y  z) (r : x  z) 
      is-equiv (right-transpose-eq-concat p q r)
    is-equiv-right-transpose-eq-concat p refl r =
        ( concat' p (inv right-unit))
        ( concat (inv right-unit) r)
        ( is-equiv-concat (inv right-unit) r)
        ( is-equiv-concat' p (inv right-unit))

  equiv-right-transpose-eq-concat :
    (p : x  y) (q : y  z) (r : x  z) 
    ((p  q)  r)  (p  (r  (inv q)))
  pr1 (equiv-right-transpose-eq-concat p q r) = right-transpose-eq-concat p q r
  pr2 (equiv-right-transpose-eq-concat p q r) =
    is-equiv-right-transpose-eq-concat p q r

Computation of fibers of families of maps out of the identity type

We show that fiber (f x) y ≃ ((* , f * refl) = (x , y)) for every x : A and y : B x.

module _
  {l1 l2 : Level} {A : UU l1} {a : A} {B : A  UU l2}
  (f : (x : A)  (a  x)  B x) (x : A) (y : B x)

  map-compute-fiber-map-out-of-identity-type :
    fiber (f x) y  ((a , f a refl)  (x , y))
  map-compute-fiber-map-out-of-identity-type (refl , refl) = refl

  map-inv-compute-fiber-map-out-of-identity-type :
    ((a , f a refl)  (x , y))  fiber (f x) y
  map-inv-compute-fiber-map-out-of-identity-type refl =
    refl , refl

  is-section-map-inv-compute-fiber-map-out-of-identity-type :
    map-inv-compute-fiber-map-out-of-identity-type ~ id
  is-section-map-inv-compute-fiber-map-out-of-identity-type refl = refl

  is-retraction-map-inv-compute-fiber-map-out-of-identity-type :
    map-compute-fiber-map-out-of-identity-type ~ id
  is-retraction-map-inv-compute-fiber-map-out-of-identity-type (refl , refl) =

  is-equiv-map-compute-fiber-map-out-of-identity-type :
    is-equiv map-compute-fiber-map-out-of-identity-type
  is-equiv-map-compute-fiber-map-out-of-identity-type =

  compute-fiber-map-out-of-identity-type :
    fiber (f x) y  ((a , f a refl)  (x , y))
  pr1 compute-fiber-map-out-of-identity-type =
  pr2 compute-fiber-map-out-of-identity-type =

Recent changes