Commuting triangles of morphisms in precategories

Content created by Egbert Rijke, Fernando Chu and Fredrik Bakke.

Created on 2024-08-29.
Last modified on 2024-08-29.

module category-theory.commuting-triangles-of-morphisms-in-precategories where
Imports 
open import category-theory.commuting-triangles-of-morphisms-in-set-magmoids
open import category-theory.precategories

open import foundation.identity-types
open import foundation.universe-levels

Idea

A triangle of morphisms

        top
     x ----> y
      \     /
  left \   / right
        ∨ ∨
         z

in a precategory C is said to commute if there is an identification between:

  left ＝ right ∘ top.

Such a identification is called the coherence of the commuting triangle.

Definitions

coherence-triangle-hom-Precategory :
  {l1 l2 : Level} (C : Precategory l1 l2)
  {x y z : obj-Precategory C}
  (top : hom-Precategory C x y)
  (left : hom-Precategory C x z)
  (right : hom-Precategory C y z) →
  UU l2
coherence-triangle-hom-Precategory C =
  coherence-triangle-hom-Set-Magmoid (set-magmoid-Precategory C)

Recent changes