Identity types

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

Created on 2022-01-26.
Last modified on 2024-04-17.

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.commuting-pentagons-of-identifications
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 higher identifications of functionsfoundation.action-on-higher-identifications-functions
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 pentagons of identificationsfoundation.commuting-pentagons-of-identifications
Commuting squares of identificationsfoundation.commuting-squares-of-identifications
Commuting triangles of identificationsfoundation.commuting-triangles-of-identifications
The computational identity typefoundation.computational-identity-types
The strictly involutive identity typefoundation.strictly-involutive-identity-types
The strictly right unital concatenation operation on identificationsfoundation.strictly-right-unital-concatenation-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
Negated equalityfoundation.negated-equality
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 families (foundation)foundation.torsorial-type-families
Torsorial type familes (foundation-core)foundation-core.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
Transposition of identifications along equivalencesfoundation.transposition-identifications-along-equivalences
The universal property of identity systemsfoundation.universal-property-identity-systems
The universal property of identity typesfoundation.universal-property-identity-types
Whiskering identificationsfoundation.whiskering-identifications-concatenation
The Yoneda identity typefoundation.yoneda-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 (_∙ s) (assoc p q r))
      α₂ = (assoc p (q  r) s)
      α₃ = (ap (p ∙_) (assoc q r s))
      α₄ = (assoc (p  q) r s)
      α₅ = (assoc p q (r  s))
    coherence-pentagon-identifications α₁ α₄ α₂ α₅ α₃
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

    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)
        ( is-retraction-inv-concat p)

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

  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-inv-concat :
    {x y : A} (p : x  y) (z : A)  (x  z)  (y  z)
  pr1 (equiv-inv-concat p z) = inv-concat p z
  pr2 (equiv-inv-concat p z) = is-equiv-inv-concat p z

  map-equiv-concat-equiv :
    {x x' : A}  ((y : A)  (x  y)  (x'  y))  (x'  x)
  map-equiv-concat-equiv {x} e = map-equiv (e x) refl

  is-section-equiv-concat :
    {x x' : A}  map-equiv-concat-equiv {x} {x'}  equiv-concat ~ id
  is-section-equiv-concat refl = refl

    is-retraction-equiv-concat :
      {x x' : A}  equiv-concat  map-equiv-concat-equiv {x} {x'} ~ id
    is-retraction-equiv-concat e =
      eq-htpy  y  eq-htpy-equiv  where refl  right-unit))

    is-equiv-map-equiv-concat-equiv :
      {x x' : A}  is-equiv (map-equiv-concat-equiv {x} {x'})
    is-equiv-map-equiv-concat-equiv =
        ( equiv-concat)
        ( is-section-equiv-concat)
        ( is-retraction-equiv-concat)

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

    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' q)
        ( is-retraction-inv-concat' q)

    is-equiv-inv-concat' :
      (x : A) {y z : A} (q : y  z)  is-equiv (inv-concat' x q)
    is-equiv-inv-concat' x q =
        ( concat' x q)
        ( is-retraction-inv-concat' q)
        ( is-section-inv-concat' 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

  equiv-inv-concat' :
    (x : A) {y z : A} (q : y  z)  (x  z)  (x  y)
  pr1 (equiv-inv-concat' x q) = inv-concat' x q
  pr2 (equiv-inv-concat' x q) = is-equiv-inv-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))))

Applying the right unit law on one side of a higher identification is an equivalence

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

  equiv-right-unit : (p : x  y) (q : x  y)  (p  q)  (p  refl  q)
  equiv-right-unit p = equiv-concat right-unit

  equiv-right-unit' : (p : x  y) (q : x  y)  (p  q  refl)  (p  q)
  equiv-right-unit' p q = equiv-concat' p right-unit

Reassociating one side of a higher identification is an equivalence

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

  equiv-concat-assoc :
    (p : x  y) (q : y  z) (r : z  u) (s : x  u) 
    ((p  q)  r  s)  (p  (q  r)  s)
  equiv-concat-assoc p q r = equiv-concat (inv (assoc p q r))

  equiv-concat-assoc' :
    (s : x  u) (p : x  y) (q : y  z) (r : z  u) 
    (s  (p  q)  r)  (s  p  (q  r))
  equiv-concat-assoc' s p q r = equiv-concat' s (assoc p q r)

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

  equiv-left-transpose-eq-concat' :
    (p : x  z) (q : x  y) (r : y  z) 
    (p  q  r)  (inv q  p  r)
  equiv-left-transpose-eq-concat' p q r =
    equiv-inv _ _ ∘e equiv-left-transpose-eq-concat q r p ∘e equiv-inv _ _

  left-transpose-eq-concat' :
    (p : x  z) (q : x  y) (r : y  z) 
    p  q  r  inv q  p  r
  left-transpose-eq-concat' p q r =
    map-equiv (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

  equiv-right-transpose-eq-concat' :
    (p : x  z) (q : x  y) (r : y  z) 
    (p  q  r)  (p  inv r  q)
  equiv-right-transpose-eq-concat' p q r =
    equiv-inv q (p  inv r) ∘e
    equiv-right-transpose-eq-concat q r p ∘e
    equiv-inv p (q  r)

  right-transpose-eq-concat' :
    (p : x  z) (q : x  y) (r : y  z) 
    p  q  r  p  inv r  q
  right-transpose-eq-concat' p q r =
    map-equiv (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