associativity — Mathlib

English

Coherence condition for associator and related natural isomorphisms in products; the pentagon diagram commutes.

Русский

Условие когерентности для ассоциатора и связанных естественных изомормических отображений в произведениях; пентагоновые диаграммы коммутируют.

LaTeX

$$$\text{Pentagon coherence for }\text{associator}$$$

Lean4

/-- The equivalence of categories expressing associativity of products of categories.
-/
@[simps]
def associativity : (C × D) × E ≌ C × D × E
    where
  functor := associator C D E
  inverse := inverseAssociator C D E
  unitIso := Iso.refl _
  counitIso := Iso.refl _

Похожие утверждения