Dependent identifications

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-06-10.

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'