Commuting squares of morphisms in large precategories

Content created by Fredrik Bakke.

Created on 2023-09-27.
Last modified on 2024-04-25.

module category-theory.commuting-squares-of-morphisms-in-large-precategories where
Imports 
open import category-theory.large-precategories

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

Idea

A square of morphisms

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

in a large precategory C is said to commute if there is an identification between both composites.

Definitions

coherence-square-hom-Large-Precategory :
  {l1 l2 l3 l4 : Level}
  {α : Level → Level}
  {β : Level → Level → Level}
  (C : Large-Precategory α β)
  {x : obj-Large-Precategory C l1}
  {y : obj-Large-Precategory C l2}
  {z : obj-Large-Precategory C l3}
  {w : obj-Large-Precategory C l4}
  (top : hom-Large-Precategory C x y)
  (left : hom-Large-Precategory C x z)
  (right : hom-Large-Precategory C y w)
  (bottom : hom-Large-Precategory C z w) →
  UU (β l1 l4)
coherence-square-hom-Large-Precategory C top left right bottom =
  ( comp-hom-Large-Precategory C bottom left) ＝
  ( comp-hom-Large-Precategory C right top)

Recent changes