Documentation

Mathlib.CategoryTheory.Sums.Associator

Associator for binary disjoint union of categories. #

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.

Instances For

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

    Instances For

      The equivalence of categories expressing associativity of sums of categories.

      Instances For