# Dependent binary homotopies

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-26.

module foundation.dependent-binary-homotopies where

Imports
open import foundation.binary-homotopies
open import foundation.universe-levels

open import foundation-core.dependent-identifications


## Idea

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

  f' : (x : A) (y : B x) → D x y (f x y)
g' : (x : A) (y : B x) → D x y (g x y)


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

## Definitions

### Dependent homotopies

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
(D : (x : A) (y : B x) (z : C x y) → UU l4)
{f g : (x : A) (y : B x) → C x y} (H : binary-htpy f g)
where

dependent-binary-homotopy :
((x : A) (y : B x) → D x y (f x y)) →
((x : A) (y : B x) → D x y (g x y)) → UU (l1 ⊔ l2 ⊔ l4)
dependent-binary-homotopy f' g' =
(x : A) (y : B x) →
dependent-identification (D x y) (H x y) (f' x y) (g' x y)


### The reflexive dependent binary homotopy

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

refl-dependent-binary-homotopy :
{f' : (x : A) (y : B x) → D x y (f x y)} →
dependent-binary-homotopy D (refl-binary-htpy f) f' f'
refl-dependent-binary-homotopy {f'} = refl-binary-htpy f'