This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Dependent homotopies

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)