This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Dependent identifications

module foundation-core.dependent-identifications where

open import foundation.universe-levels

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

Idea

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.

Definition

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

  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'