Commuting triangles of maps

{-# OPTIONS --safe #-}
module foundation-core.commuting-triangles-of-maps where

open import foundation-core.functions
open import foundation-core.homotopies
open import foundation-core.universe-levels

Idea

A triangle of maps

 A ----> B
  \     /
   \   /
    V V
     X

is said to commute if there is a homotopy between the map on the left and the composite map.

Definition

Commuting triangles of maps

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  where

  coherence-triangle-maps :
    (left : A → X) (right : B → X) (top : A → B) → UU (l1 ⊔ l2)
  coherence-triangle-maps left right top = left ~ (right ∘ top)

  coherence-triangle-maps' :
    (left : A → X) (right : B → X) (top : A → B) → UU (l1 ⊔ l2)
  coherence-triangle-maps' left right top = (right ∘ top) ~ left

Concatenation of commuting triangles of maps

module _
  {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : A → X) (g : B → X) (h : C → X) (i : A → B) (j : B → C)
  where

  concat-coherence-triangle-maps :
    coherence-triangle-maps f g i →
    coherence-triangle-maps g h j →
    coherence-triangle-maps f h (j ∘ i)
  concat-coherence-triangle-maps H K =
    H ∙h (K ·r i)