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

Idea

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.

ConceptFile
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

Properties

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))
  in
  ((α₁  α₂)  α₃)  (α₄  α₅)
Mac-Lane-pentagon refl refl refl refl = refl

The groupoidal operations on identity types are equivalences

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

  abstract
    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

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

  abstract
    is-equiv-concat' :
      (x : A) {y z : A} (q : y  z)  is-equiv (concat' x q)
    is-equiv-concat' x q =
      is-equiv-is-invertible
        ( 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}
  where

  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))) 
      ( α))
    where
    α :
      ( ( 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}
  where

  abstract
    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

  abstract
    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 =
      is-equiv-comp
        ( 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)
  where

  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-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-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) =
    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 =
    is-equiv-is-invertible
      map-inv-compute-fiber-map-out-of-identity-type
      is-section-map-inv-compute-fiber-map-out-of-identity-type
      is-retraction-map-inv-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 =
    map-compute-fiber-map-out-of-identity-type
  pr2 compute-fiber-map-out-of-identity-type =
    is-equiv-map-compute-fiber-map-out-of-identity-type

Recent changes