Commuting squares of morphisms in set-magmoids

Content created by Fredrik Bakke.

Created on 2023-11-01.
Last modified on 2024-04-25.

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

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

Idea

A square of morphisms

  x ------> y
  |         |
  |         |
  ∨         ∨
  z ------> w

in a set-magmoid C is said to commute if there is an identification between both composites:

  bottom ∘ left ＝ right ∘ top.

Definitions

coherence-square-hom-Set-Magmoid :
  {l1 l2 : Level} (C : Set-Magmoid l1 l2)
  {x y z w : obj-Set-Magmoid C}
  (top : hom-Set-Magmoid C x y)
  (left : hom-Set-Magmoid C x z)
  (right : hom-Set-Magmoid C y w)
  (bottom : hom-Set-Magmoid C z w) →
  UU l2
coherence-square-hom-Set-Magmoid C top left right bottom =
  ( comp-hom-Set-Magmoid C bottom left) ＝
  ( comp-hom-Set-Magmoid C right top)

Recent changes