Coproduct

definition example theorem proof

The coproduct (sum) of objects $a,b$ in a Category is an object $a+b$ with injections ${\iota }_a:a\to a+b$, ${\iota }_b:b\to a+b$ (DaoFP: $\mathsf{Left},\mathsf{Right}$) such that for every $x$ with $f:a\to x$, $g:b\to x$ there is a unique $[f,g]:a+b\to x$ (Kittenlab: $⟨f,g⟩$; DaoFP: $h$) with ${\iota }_a;[f,g]=f$ and ${\iota }_b;[f,g]=g$. Dual to Product: the product in ${\mathcal{C}}^{\mathrm{op}}$.

Sources: Kittenlab Lecture 8 (“Representatives of functors”, coproducts as representing objects, the “traditional” definition), 9, 11 (“Coproducts of types in Julia”); DaoFP Chapter 4 (“Sum Types”, “Cocartesian Categories”), §9.4 (“Sum as a universal cospan”), §10.2 (“The sum adjunction”); 7 Sketches §6.2.2 (Definition 6.6, Examples 6.7–6.9, Exercises 6.10–6.11), §3.4.3 ($\Sigma$ “unions data”); CTfS §2.4.2 (Definition 2.4.2.1, Lemma 2.4.2.7, Examples 2.4.2.3–2.4.2.12), Definition 4.5.1.23, Examples 4.5.1.19–4.5.1.27

Examples

• $\mathbf{Set}$: the disjoint union $X\bigsqcup Y=\{(x,1)\}\cup \{(y,2)\}$ (7 Sketches §1.2.1); in $\mathbf{FinSet}$, $\{\mathrm{1..}n\}+\{\mathrm{1..}m\}=\{\mathrm{1..}n+m\}$.
• Preorder: the Join $a\vee b$; in the Preorder of Partitions, the join of systems (Generative Effect).
• Graphs and all C-sets: pointwise, $(G+H)(V)=G(V)+H(V)$, $(G+H)(E)=G(E)+H(E)$ (Kittenlab Lecture 8).
• Sum types in programming: Julia Union{Left{S}, Right{T}} — a function out of it is written by dispatch on Left/Right, i.e. by two functions, one per summand; the tagged union TaggedUnion{S,T} is another representing object with “precisely the same external interface” but different performance (Kittenlab Lecture 11). Haskell Either a b with either :: (a -> x) -> (b -> x) -> Either a b -> x; Bool = 1 + 1, Maybe a = 1 + a, enumerations (DaoFP Chapter 4). In logic: disjunction $A\vee B$; a proof is a proof of one side.
• $\mathbb{N}$-ary coproducts are colimits over a Discrete Category with $n$ objects; the empty coproduct is the Initial Object (Kittenlab Lecture 9). Coproducts of monoids, groups, categories, and props exist but are not disjoint unions (7 Sketches §5.2.3).

Examples from Category Theory for Scientists

• Airplane seats (CTfS Examples 2.4.2.3, 2.4.2.8). “A seat in an airplane” is the coproduct of “an economy-class seat” and “a first-class seat”. The universal property says: if we know how economy seats are priced and how first-class seats are priced, and every seat is one or the other, we know how all seats are priced — the induced map $[{\text{price}}_E,{\text{price}}_F]$; likewise the induced map to “an airplane” needs no extra bookkeeping. In an olog the injections are labelled “is” and the coproduct box “an $A$ or a $B$“.
• Disjointness matters (CTfS Example 2.4.2.12). The coproduct of “an animal that can fly” and “an animal that can swim” contains every duck twice, once labelled as a flyer and once as a swimmer; to count ducks once one needs a Pushout over “an animal that can fly and swim” (cf. CTfS Exercise 2.4.2.13 on photons as particles and waves).
• Piecewise curves (CTfS Application 2.4.2.9): functions on $[a,b]$ and $[c,d]$ (say the elastic and plastic regimes of a stress–strain curve) extend uniquely to $[a,b]\bigsqcup [c,d]$; if they must agree at a shared endpoint one again needs a pushout.
• In a preorder the coproduct is the join: in $(\mathbb{N},\mid )$, $9+12=\mathrm{lcm}(9,12)=36$ (CTfS Exercise 4.5.1.29); the coproduct of two preorders puts them side by side with no relations between them, so “apples $\bigsqcup$ oranges” is an unbiased guess at preferences on fruit (CTfS Exercise 4.5.1.20). Coproducts need not exist: in ${\mathbb{R}}^2$ ordered by ”$q$ lies on the ray from $0$ through $p$, beyond $p$”, the points $(1,0)$ and $(0,1)$ have no coproduct (CTfS Example 4.5.1.26).
• Graphs and dynamical systems (CTfS Examples 4.5.1.21–4.5.1.22): the coproduct of two graphs or two discrete dynamical systems is the disjoint union of their tables; “None shall receive maps from $X$ and $Y$ except through me!”

Three descriptions (Kittenlab Lecture 8, DaoFP §9.4, §10.2)

1. Representability: $a+b$ is a representing object of the functor $\mathrm{Hom}(a,-)\times \mathrm{Hom}(b,-):\mathcal{C}\to \mathbf{Set}$; “a map out of the coproduct is equivalent to a map out of each summand”. By the Yoneda Lemma representing objects are unique up to isomorphism, justifying “the coproduct”. Feeding ${\mathrm{id}}_{a+b}$ into the isomorphism $\mathrm{Hom}(a+b,-)\cong \mathrm{Hom}(a,-)\times \mathrm{Hom}(b,-)$ recovers the injections ${\iota }_a,{\iota }_b$, and universality (1 above) follows.
2. Universal cocone: $[2,\mathcal{C}](D,{\Delta }_x)\cong \mathcal{C}(a+b,x)$ where $D:2\to \mathcal{C}$ picks $a,b$ — “sum as a universal Cospan”: a Colimit of a two-object discrete diagram; an Initial Object in the category of cocones.
3. Adjunction: $(+)⊣\Delta$ with unit the pair of injections (Diagonal Functor).

Properties (DaoFP Chapter 4)

• Functoriality: $f+g:=[f;\iota ,g;\iota ]$ makes $+$ a Bifunctor (bimap for Either).
• $a+0\cong a$ (“something plus zero”), $1+0\cong 1$, commutativity $a+b\cong b+a$ (via $[{\iota }_b,{\iota }_a]$), associativity — a category with finite coproducts is cocartesian and $(\mathcal{C},+,0)$ is a Symmetric Monoidal Category. Bicartesian categories have both; in a Bicartesian Closed Category products distribute over sums.
• $\mathcal{C}(a+b,x)\cong \mathcal{C}(a,x)\times \mathcal{C}(b,x)$: the contravariant hom-functor turns sums into products (DaoFP §10.7: hom preserves colimits).
• A Pushout is a coproduct with part of the two objects “equalized by fiat” (Kittenlab Lecture 9); coequalizers “squish” (Lecture 11: “if coproducts allow you to add objects, coequalizers allow you to squish them”).

JuliaLeanHaskell

Docs: FinSets · Limits & colimits — Kittenlab Lecture 8, Lecture 9, Lecture 11

# Kittenlab Lecture 11: coproducts of Julia types are tagged unions; functions out are by dispatch
struct Left{T};  val::T end
struct Right{T}; val::T end
const Coproduct{S,T} = Union{Left{S}, Right{T}}
foo(l::Left{Int}) = l.val^2                 # one function per summand: the universal property
foo(r::Right{String}) = length(r.val)
(foo(Left(4)), foo(Right("hello")))         # (16, 5)

Catlab version (run in a fresh Julia session — Catlab exports its own compose, id, FinFunction, …):

# Catlab
using Catlab
C = coproduct(FinSet(2), FinSet(3))
apex(C)                                     # FinSet(5)
ι1, ι2 = legs(C)
f = FinFunction([1, 2], 2); g = FinFunction([2, 2, 1], 2)
h = copair(C, f, g)                         # [f, g] : FinSet(5) → FinSet(2)
compose(ι1, h) == f && compose(ι2, h) == g  # true

#check CategoryTheory.Limits.coprod         -- X ⨿ Y with coprod.inl, coprod.inr, coprod.desc
#check CategoryTheory.Limits.coprod.desc    -- [f, g]
#check CategoryTheory.Limits.Types.binaryCoproductIso   -- X ⨿ Y ≅ X ⊕ Y in Type
example (A B X : Type) (f : A → X) (g : B → X) : A ⊕ B → X := Sum.elim f g

-- DaoFP Chapter 4: sum types
data Either a b = Left a | Right b
 
either' :: (a -> x) -> (b -> x) -> (Either a b -> x)     -- the universal [f, g]
either' f _ (Left a)  = f a
either' _ g (Right b) = g b
 
-- functoriality
bimapE :: (a -> a') -> (b -> b') -> Either a b -> Either a' b'
bimapE f _ (Left a)  = Left (f a)
bimapE _ g (Right b) = Right (g b)
 
-- Bool = 1 + 1, Maybe a = 1 + a
data Maybe' a = Nothing' | Just' a