The action on identifications of dependent functions

Content created by Fredrik Bakke, Egbert Rijke, Julian KG, fernabnor and louismntnu.

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

module foundation.action-on-identifications-dependent-functions where
Imports 
open import foundation.universe-levels

open import foundation-core.dependent-identifications
open import foundation-core.identity-types

Idea

Given a dependent function f : (x : A) → B x and an identification p : x ＝ y in A, we cannot directly compare the values f x and f y, since f x is an element of type B x while f y is an element of type B y. However, we can transport the value f x along p to obtain an element of type B y that is comparable to the value f y. In other words, we can consider the type of dependent identifications over p from f x to f y. The dependent action on identifications of f on p is a dependent identification

  apd f p : dependent-identification B p (f x) (f y).

Definition

Functorial action of dependent functions on identity types

apd :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) {x y : A}
  (p : x ＝ y) → dependent-identification B p (f x) (f y)
apd f refl = refl

apd' :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) {x y : A}
  (p : x ＝ y) → dependent-identification' B p (f x) (f y)
apd' f refl = refl

See also

Recent changes