Commuting triangles of morphisms of arrows

Content created by Fredrik Bakke.

Created on 2024-03-22.
Last modified on 2024-04-17.

module foundation.commuting-triangles-of-morphisms-arrows where
Imports 
open import foundation.homotopies-morphisms-arrows
open import foundation.morphisms-arrows
open import foundation.universe-levels

Idea

Consider a triangle of morphisms of arrows

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

then we can ask that the triangle commutes

by asking for a homotopy of morphisms of arrows

  left ~ right ∘ top.

This is equivalent to asking for a commuting prism of maps, given the square faces in the diagram

        f
  ∙ ---------> ∙
  |\           |\
  | \          | \
  |  \         |  \
  |   ∨        |   ∨
  |    ∙ --- g ---> ∙
  |   /        |   /
  |  /         |  /
  | /          | /
  ∨∨           ∨∨
  ∙ ---------> ∙.
        h

Definition

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : UU l1} {A' : UU l2} {B : UU l3} {B' : UU l4} {C : UU l5} {C' : UU l6}
  (f : A → A') (g : B → B') (h : C → C')
  (left : hom-arrow f h) (right : hom-arrow g h) (top : hom-arrow f g)
  where

  coherence-triangle-hom-arrow : UU (l1 ⊔ l2 ⊔ l5 ⊔ l6)
  coherence-triangle-hom-arrow =
    htpy-hom-arrow f h left (comp-hom-arrow f g h right top)

  coherence-triangle-hom-arrow' : UU (l1 ⊔ l2 ⊔ l5 ⊔ l6)
  coherence-triangle-hom-arrow' =
    htpy-hom-arrow f h (comp-hom-arrow f g h right top) left

Recent changes