Span

A span in a Category $\mathcal{C}$ is a diagram

Typically, we want to think about a span as a categorified, proof-relevant Relation.

Properties

• A span can be viewed as a Linear Polynomial Functor $X\leftarrow R\xrightarrow{mathrm{id}{ifx..lse\par i}}R\to Y$.