Commuting triangles of maps

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2023-02-18.
Last modified on 2023-09-12.

module foundation-core.commuting-triangles-of-maps where
Imports
open import foundation.universe-levels

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

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)

Recent changes