Commuting triangles of pointed maps

Content created by Egbert Rijke.

Created on 2024-03-13.

module structured-types.commuting-triangles-of-pointed-maps where

Imports
open import foundation.universe-levels

open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types
open import structured-types.whiskering-pointed-homotopies-composition


Idea

Consider a triangle of pointed maps

           top
A ------> B
\       /
left \     / right
\   /
∨ ∨
C


Such a triangle is said to be a commuting triangle of pointed maps if there is a pointed homotopy

  left ~∗ right ∘∗ top.


Such a homotopy is referred to as the coherence of the commuting triangle of pointed maps.

Definitions

Coherences of commuting triangles of pointed maps

module _
{l1 l2 l3 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3}
(left : A →∗ C) (right : B →∗ C) (top : A →∗ B)
where

coherence-triangle-pointed-maps : UU (l1 ⊔ l3)
coherence-triangle-pointed-maps =
left ~∗ right ∘∗ top

coherence-triangle-pointed-maps' : UU (l1 ⊔ l3)
coherence-triangle-pointed-maps' =
right ∘∗ top ~∗ left


Properties

Left whiskering of coherences of commuting triangles of pointed maps

Consider a commuting triangle of pointed maps

           top
A ------> B
\       /
left \     / right
\   /
∨ ∨
C


and consider a pointed map f : C →∗ X. The left whiskering is a coherence of the triangle of pointed maps

              top
A ------> B
\       /
f ∘∗ left \     / f ∘∗ right
\   /
∨ ∨
X


In other words, left whiskering of coherences of commuting triangles of pointed maps is an operation

  (left ~∗ right ∘∗ top) → (f ∘∗ left ~∗ (f ∘∗ right) ∘∗ top).

module _
{l1 l2 l3 l4 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3}
{X : Pointed-Type l4} (f : C →∗ X)
(left : A →∗ C) (right : B →∗ C) (top : A →∗ B)
where

left-whisker-coherence-triangle-pointed-maps :
coherence-triangle-pointed-maps left right top →
coherence-triangle-pointed-maps (f ∘∗ left) (f ∘∗ right) top
left-whisker-coherence-triangle-pointed-maps H =
concat-pointed-htpy
( left-whisker-comp-pointed-htpy f left (right ∘∗ top) H)
( inv-pointed-htpy
( associative-comp-pointed-map f right top))