# Dependent homotopies

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-22.

module foundation.dependent-homotopies where

Imports
open import foundation.universe-levels

open import foundation-core.dependent-identifications
open import foundation-core.homotopies


## Idea

Consider a homotopy H : f ~ g between two functions f g : (x : A) → B x. Furthermore, consider a type family C : (x : A) → B x → 𝒰 and two functions

  f' : (x : A) → C x (f x)
g' : (x : A) → C x (g x)


A dependent homotopy from f' to g' over H is a family of dependent identifications from f' x to g' x over H x.

## Definitions

### Dependent homotopies

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3)
{f g : (x : A) → B x} (H : f ~ g)
where

dependent-homotopy :
((x : A) → C x (f x)) → ((x : A) → C x (g x)) → UU (l1 ⊔ l3)
dependent-homotopy f' g' =
(x : A) → dependent-identification (C x) (H x) (f' x) (g' x)


### The reflexive dependent homotopy

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3)
{f : (x : A) → B x}
where

refl-dependent-homotopy :
{f' : (x : A) → C x (f x)} → dependent-homotopy C refl-htpy f' f'
refl-dependent-homotopy = refl-htpy


### Iterated dependent homotopies

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3)
{f g : (x : A) → B x} {H K : f ~ g} (L : H ~ K)
where

dependent-homotopy² :
{f' : (x : A) → C x (f x)} {g' : (x : A) → C x (g x)} →
dependent-homotopy C H f' g' →
dependent-homotopy C K f' g' → UU (l1 ⊔ l3)
dependent-homotopy² {f'} {g'} H' K' =
(x : A) → dependent-identification² (C x) (L x) (H' x) (K' x)