mathlib documentation

category_theory.sums.associator

Associator for binary disjoint union of categories. #

The associator functor ((C ⊕ D) ⊕ E) ⥤ (C ⊕ (D ⊕ E)) and its inverse form an equivalence.

def category_theory.sum.associator (C : Type u) [category_theory.category C] (D : Type u) [category_theory.category D] (E : Type u) [category_theory.category E] :
(C D) E C D E

The associator functor (C ⊕ D) ⊕ E ⥤ C ⊕ (D ⊕ E) for sums of categories.

Equations
@[simp]

The inverse associator functor C ⊕ (D ⊕ E) ⥤ (C ⊕ D) ⊕ E for sums of categories.

Equations