sum C D gives the direct sum of two categories.

inl_ is the functor X ↦ inl X.

inr_ is the functor X ↦ inr X.

The functor exchanging two direct summand categories.

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

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

The sum of two functors.

The sum of two natural transformations.