Dependent identifications

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-06-10.
Last modified on 2023-09-11.

module foundation-core.dependent-identifications where
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.transport-along-identifications


Consider a type family B over A, an identification p : x = y in A, and two elements u : B x and v : B y. A path over p from u to v is an identification

  tr B p u = v,

where tr is the transport function. Dependent identifications also satisfy groupoid laws, which are formulated appropriately as dependent identifications. The groupoid laws for dependent identifications are proven in foundation.dependent-identifications.


Dependent identifications

dependent-identification :
  {l1 l2 : Level} {A : UU l1} (B : A  UU l2) {x x' : A} (p : x  x') 
  B x  B x'  UU l2
dependent-identification B p u v = (tr B p u  v)

refl-dependent-identification :
  {l1 l2 : Level} {A : UU l1} (B : A  UU l2) {x : A} {y : B x} 
  dependent-identification B refl y y
refl-dependent-identification B = refl

Iterated dependent identifications

module _
  {l1 l2 : Level} {A : UU l1} (B : A  UU l2)

  dependent-identification² :
    {x y : A} {p q : x  y} (α : p  q)
    {x' : B x} {y' : B y}
    (p' : dependent-identification B p x' y')
    (q' : dependent-identification B q x' y') 
    UU l2
  dependent-identification² α {x'} {y'} p' q' =
    dependent-identification  t  dependent-identification B t x' y') α p' q'

Recent changes