Commuting triangles of homotopies

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-02-18.

module foundation.commuting-triangles-of-homotopies where

Imports
open import foundation.commuting-triangles-of-identifications
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.function-types
open import foundation-core.homotopies


Idea

A triangle of homotopies of dependent functions

      top
f ----> g
\     /
left \   / right
∨ ∨
h


is said to commute if there is a homotopy left ~ top ∙h right.

Definitions

Coherences of commuting triangles of homotopies

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

coherence-triangle-homotopies :
(left : f ~ h) (right : g ~ h) (top : f ~ g) → UU (l1 ⊔ l2)
coherence-triangle-homotopies left right top = left ~ top ∙h right

coherence-triangle-homotopies' :
(left : f ~ h) (right : g ~ h) (top : f ~ g) → UU (l1 ⊔ l2)
coherence-triangle-homotopies' left right top = top ∙h right ~ left


Properties

Left whiskering commuting triangles of homotopies with respect to concatenation of homotopies

Consider a commuting triangle of homotopies

        top
f ----> g
\     /
left \   / right
∨ ∨
h


where f g h : (x : A) → B x, and consider a homotopy H : i ~ f for a fourth dependent function i : (x : A) → B x. Then the triangle of homotopies

           H ∙h top
i --------> g
\       /
H ∙h left \     / right
\   /
∨ ∨
h


commutes.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
{f g h i : (x : A) → B x} (H : i ~ f)
(left : f ~ h) (right : g ~ h) (top : f ~ g)
where

left-whisker-concat-coherence-triangle-homotopies :
(T : coherence-triangle-homotopies left right top) →
coherence-triangle-homotopies (H ∙h left) right (H ∙h top)
left-whisker-concat-coherence-triangle-homotopies T x =
left-whisker-concat-coherence-triangle-identifications
( H x)
( left x)
( right x)
( top x)
( T x)


Right whiskering triangles of homotopies with respect to concatenation of homotopies

Consider a commuting triangle of homotopies

        top
f ----> g
\     /
left \   / right
∨ ∨
h


where f g h : (x : A) → B x, and consider a homotopy H : h ~ i for a fourth dependent function i : (x : A) → B x. Then the triangle of homotopies

              top
f --------> g
\       /
left ∙h H \     / right ∙h H
\   /
∨ ∨
i


commutes.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
{f g h : (x : A) → B x}
(left : f ~ h) (right : g ~ h) (top : f ~ g)
where

right-whisker-concat-coherence-triangle-homotopies :
coherence-triangle-homotopies left right top →
{i : (x : A) → B x} (H : h ~ i) →
coherence-triangle-homotopies (left ∙h H) (right ∙h H) top
right-whisker-concat-coherence-triangle-homotopies T H x =
right-whisker-concat-coherence-triangle-identifications
( left x)
( right x)
( top x)
( H x)
( T x)


Left whiskering of commuting triangles of homotopies with respect to composition

Consider a commuting triangle of homotopies

        top
f ----> g
\     /
left \   / right
∨ ∨
h


where f, g, and h are maps A → B. Furthermore, consider a map i : B → X. Then we obtain a commuting triangle of homotopies

           i ·l top
i ∘ f --------> i ∘ g
\       /
i ·l left \     / i ·l right
\   /
∨ ∨
i ∘ h.


This notion of whiskering should be compared to whiskering higher homotopies with respect to composition.

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (i : B → X)
{f g h : A → B} (left : f ~ h) (right : g ~ h) (top : f ~ g)
where

left-whisker-comp-coherence-triangle-homotopies :
(T : coherence-triangle-homotopies left right top) →
coherence-triangle-homotopies (i ·l left) (i ·l right) (i ·l top)
left-whisker-comp-coherence-triangle-homotopies T x =
map-coherence-triangle-identifications i (left x) (right x) (top x) (T x)


Right whiskering commuting triangles of homotopies with respect to composition

Consider a commuting triangle of homotopies

        top
f ----> g
\     /
left \   / right
∨ ∨
h


where f, g, and h are maps A → B. Furthermore, consider a map i : X → A. Then we obtain a commuting triangle of homotopies

           top ·r i
f ∘ i --------> g ∘ i
\       /
left ·r i \     / right ·r i
\   /
∨ ∨
h ∘ i.


This notion of whiskering should be compared to whiskering higher homotopies with respect to composition.

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
{f g h : A → B} (left : f ~ h) (right : g ~ h) (top : f ~ g)
where

right-whisker-comp-coherence-triangle-homotopies :
(T : coherence-triangle-homotopies left right top) (i : X → A) →
coherence-triangle-homotopies (left ·r i) (right ·r i) (top ·r i)
right-whisker-comp-coherence-triangle-homotopies T i = T ∘ i