Documentation

Mathlib.CategoryTheory.Sums.Basic

Binary disjoint unions of categories #

We define the category instance on C ⊕ D when C and D are categories.

We define:

We further define sums of functors and natural transformations, written F.sum G and α.sum β.

@[simp]
@[simp]

The functor exchanging two direct summand categories.

Instances For

    swap gives an equivalence between C ⊕ D and D ⊕ C.

    Instances For

      The double swap on C ⊕ D is naturally isomorphic to the identity functor.

      Instances For