# The action on identifications of dependent functions

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

Created on 2023-06-10.

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