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

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

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 (_∙ 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))
  in
    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}
  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

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

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

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

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

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

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

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

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

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

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

  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)

  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

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