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

Recent changes