mathlib3 documentation

category_theory.sums.associator

Associator for binary disjoint union of categories. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Equations
Instances for category_theory.sum.associator

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

Equations
Instances for category_theory.sum.inverse_associator