nLab span


This entry is about the notion of spans/correspondences which generalizes that of relations. For spans in vector spaces or modules, see linear span.



Set theory

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Category theory

2-Category theory



In set theory

In set theory, a span or correspondence between sets AA and BB is a set CC with a function R:CA×BR:C \to A \times B to the product set A×BA \times B. A span between a set AA and AA itself is a directed pseudograph, which is used to define categories in set theory.

In dependent type theory

In dependent type theory, there is a distinction between a span, a multivalued partial function, and a correspondence:

  • A span between types AA and BB is a type CC with families of elements x:Cg(x):Ax:C \vdash g(x):A and x:Ch(x):Bx:C \vdash h(x):B

  • A multivalued partial function from type AA to type BB is a type family x:AP(x)x:A \vdash P(x) with a family of elements x:A,p:P(x)f(x,p):Bx:A, p:P(x) \vdash f(x, p):B

  • A correspondence between types AA and BB is a type family x:A,y:BR(x,y)x:A, y:B \vdash R(x, y).

However, from any one of the above structures, one could get the other two structures, provided one has identity types and dependent pair types in the dependent type theory. Given a type family x:AP(x)x:A \vdash P(x), let z: x:AP(x)π 1(z):Az:\sum_{x:A} P(x) \vdash \pi_1(z):A and z: x:AP(x)π 2(z):P(π 1(z))z:\sum_{x:A} P(x) \vdash \pi_2(z):P(\pi_1(z)) be the dependent pair projections for the dependent pair type x:AP(x)\sum_{x:A} P(x).

  • From every span one could get a multivalued partial function by defining the type family x:AP(x)x:A \vdash P(x) as P(x) y:Cg(y)= AxP(x) \coloneqq \sum_{y:C} g(y) =_A x and the family of elements x:A,p:P(x)f(x,p):Bx:A, p:P(x) \vdash f(x, p):B as f(x,p)h(π 1(x))f(x, p) \coloneqq h(\pi_1(x)).

  • From every multivalued partial function one could get a span by defining the type CC as C x:AP(x)C \coloneqq \sum_{x:A} P(x) and the family of elements x:Cg(x):Ax:C \vdash g(x):A as g(x)π 1(x)g(x) \coloneqq \pi_1(x).

  • From every multivalued partial function one could get a correspondence by defining the type family x:A,y:BR(x,y)x:A, y:B \vdash R(x, y) as R(x,y) p:P(x)f(x,p)= ByR(x, y) \coloneqq \sum_{p:P(x)} f(x, p) =_B y.

  • From every correspondence one could get a multivalued partial function by defining the type family x:AP(x)x:A \vdash P(x) as P(x) y:BR(x,y)P(x) \coloneqq \sum_{y:B} R(x, y), and the family of elements x:A,p:P(x)h(x,p):Bx:A, p:P(x) \vdash h(x, p):B as h(x,p)π 1(p)h(x, p) \coloneqq \pi_1(p)

  • From every span one could get a correspondence by defining the type family x:A,y:BR(x,y)x:A, y:B \vdash R(x, y) as R(x,y) z:C(g(z)= Ax)×(h(z)= By)R(x, y) \coloneqq \sum_{z:C} (g(z) =_A x) \times (h(z) =_B y).

  • From every correspondence one could get a span by defining the type CC as C x:A y:BR(x,y)C \coloneqq \sum_{x:A} \sum_{y:B} R(x, y), the family of elements z:Cg(z):Az:C \vdash g(z):A as g(z)π 1(z)g(z) \coloneqq \pi_1(z), and the function z:Ch(z):Bz:C \vdash h(z):B as h(z)π 1(π 2(z))h(z) \coloneqq \pi_1(\pi_2(z))

Given types AA, BB, and CC and spans (D,x:Dg D(x):A,x:Dh D(x):B)(D, x:D \vdash g_D(x):A, x:D \vdash h_D(x):B) between AA and BB and (E,y:Eg E(y):B,y:Eh E(y):C)(E, y:E \vdash g_E(y):B, y:E \vdash h_E(y):C) between BB and CC, there is a span

(ED,z:EDg ED(z):A,z:EDh ED(z):C)(E \circ D, z:E \circ D \vdash g_{E \circ D}(z):A, z:E \circ D \vdash h_{E \circ D}(z):C)

defined by

ED x:D y:Eh D(x)= Bg E(y)E \circ D \coloneqq \sum_{x:D} \sum_{y:E} h_D(x) =_B g_E(y)
z:EDg ED(z)g D(π 1(z))z:E \circ D \vdash g_{E \circ D}(z) \coloneqq g_D(\pi_1(z))
z:EDh ED(z)h E(π 1(π 2(π 1(z))(z)))z:E \circ D \vdash h_{E \circ D}(z) \coloneqq h_E(\pi_1(\pi_2(\pi_1(z))(z)))

Given types AA, BB, and CC and correspondences x:A,y:BR(x,y)x:A, y:B \vdash R(x, y) and y:B,z:CS(y,z)y:B, z:C \vdash S(y, z), there is a correspondence x:A,z:C(SR)(x,z)x:A, z:C \vdash (S \circ R)(x, z) defined by

(SR)(x,z) y:BR(x,y)×S(y,z)(S \circ R)(x, z) \coloneqq \sum_{y:B} R(x, y) \times S(y, z)

In category theory

In any category CC, a span, or roof, or correspondence, from an object xx to an object yy is a diagram of the form

s f g x y \array{ && s \\ & {}^{f}\swarrow && \searrow^{g} \\ x &&&& y }

where ss is some other object of the category. (The word “correspondence” is also sometimes used for a profunctor.)

This diagram is also called a ‘span’ because it looks like a little bridge; ‘roof’ is similar. The term ‘correspondence’ is prevalent in geometry and related areas; it comes about because a correspondence is a generalisation of a binary relation.

Note that a span with f=1f = 1 is just a morphism from xx to yy, while a span with g=1g = 1 is a morphism from yy to xx. So, a span can be thought of as a generalization of a morphism in which there is no longer any asymmetry between source and target.

A span in the opposite category C opC^op is called a co-span in CC.

A span that has a cocone is called a coquadrable span.

Categories of spans

If the category CC has pullbacks, we can compose spans. Namely, given a span from xx to yy and a span from yy to zz:

s t f g h i x y z \array{ && s &&&& t \\ & {}^{f}\swarrow && \searrow^{g} & & {}^{h}\swarrow && \searrow^{i} \\ x &&&& y &&&& z }

we can take a pullback in the middle:

s× yt p s p t s t f g h i x y z \array{ &&&& s \times_y t \\& && {}^{p_s}\swarrow && \searrow^{p_t} \\ && s &&&& t \\ & {}^{f}\swarrow && \searrow^{g} & & {}^{h}\swarrow && \searrow^{i} \\ x &&&& y &&&& z }

and obtain a span from xx to zz:

s× yt fp s ip t x z \array{ && s \times_y t \\ & {}^{f p_s}\swarrow && \searrow^{i p_t} \\ x &&&& z }

This way of composing spans lets us define a bicategory Span(C)(C) with:

  • objects of CC as objects
  • spans as morphisms
  • maps between spans as 2-morphisms

This is a weak 2-category: it has a nontrivial associator: composition of spans is not strictly associative, because pullbacks are defined only up to canonical isomorphism. A naturally defined strict 2-category which is equivalent to Span(C)Span(C) is the strict 2-category of linear polynomial functors between slice categories of CC.

(Note that we must choose a specific pullback when defining the composite of a pair of morphisms in Span(C)Span(C), if we want to obtain a bicategory as traditionally defined; this requires the axiom of choice. Otherwise we obtain a bicategory with ‘composites of morphisms defined only up to canonical iso-2-morphism’; such a structure can be modeled by an anabicategory or an opetopic bicategory?.)

By including functions as well, instead of a bicategory we obtain a pseudo-double category?.


The 1-category of spans

Let CC be a category with pullbacks and let Span 1(C):=(Span(C)) 1Span_1(C) := (Span(C))_{\sim 1} be the 1-category of objects of CC and isomorphism classes of spans between them as morphisms.


Next assume that CC is a cartesian monoidal category. Then clearly Span 1(C)Span_1(C) naturally becomes a monoidal category itself, but more: then

Universal property of the bicategory of spans

We discuss the universal property that characterizes 2-categories of spans.

For CC be a category with pullbacks, write

  1. Span 2(C)(Span(C)) 2Span_2(C) \coloneqq (Span(C))_{\sim2} for the weak 2-category of objects of CC, spans as morphisms, and maps between spans as 2-morphisms,

  2. η C:CSpan 2(C)\eta_C: C \rightarrow Span_2(C) for the functor given by:

Now let

  1. KK be any bicategory

  2. F,G:CKF, G \,\colon\, C \rightarrow K be functors such that every map in CC is sent to a map in KK possessing a right adjoint and satisfying the Beck-Chevalley Condition for any commutative square in KK,

  3. α:FG\alpha \,\colon\, F \rightarrow G be a natural transformation.



(universal property of the bicategory of spans)
The following holds:

  1. η C\eta_C is universal among such functors FF, i.e. FF as above factors as F=F^η CF = \hat{F} \circ \eta_C for a functor F^:Span 2(C)K\hat{F} \,\colon\, Span_2(C) \rightarrow K which is unique up to isomorphism.

  2. There exists a unique lax natural transformation: α^:F^G^\hat{\alpha} \,\colon\, \hat{F} \rightarrow \hat{G} such that α^η C=α\hat{\alpha} \eta_C = \alpha.

  3. Let x,yx, y be objects in CC and f:xyf: x \rightarrow y be a morphism in CC. If (α x,α y)(\alpha_x, \alpha_y) induce a pseudo-map of adjoints F(f)(Ff) *G(f)(Gf) *F(f) \dashv (Ff)^* \rightarrow G(f) \dashv (Gf)^*, then α^\hat{\alpha} is a pseudonatural transformation

Furthermore, if we denote PbkPbk as the 2-category of categories with pullbacks, pullback-preserving functors, and equifibered natural transformations and BiCatBiCat as the tricategory of bicategories, Span():PbkBiCatSpan(-): Pbk \rightarrow BiCat is well-defined as a functor.

This is due to Hermida 1999.

Limits and colimits

Since a category of spans/correspondences Corr(𝒞)Corr(\mathcal{C}) is evidently equivalent to its opposite category, it follows that to the extent that limits exists they are also colimits and vice versa.

If the underlying category 𝒞\mathcal{C} is an extensive category, then the coproduct/product in Corr(𝒞)Corr(\mathcal{C}) is given by the disjoint union in 𝒞\mathcal{C}. (See also this MO discussion).

More generally, every van Kampen colimit in 𝒞\mathcal{C} is a (co)limit in Corr(𝒞)Corr(\mathcal{C}) — and conversely, this property characterizes van Kampen colimits. (Sobocinski-Heindel 11).

Relation to relations

Correspondences may be seen as generalizations of relations. A relation is a correspondence which is (-1)-truncated as a morphism into the cartesian product. See at relation and at Rel for more on this.


A category of correspondences is a refinement of a category Rel of relations. See there for more.


The terminology “span” appears on page 533 of:

The Span(C)Span(C) construction was introduced by Jean Bénabou (as an example of a bicategory) in

  • Jean Bénabou, Introduction to Bicategories, Lecture Notes in Mathematics 47, Springer (1967), pp.1-77. (doi)

Bénabou cites an article by Yoneda (1954) for introducing the concept of span (in the category of categories).

An exposition discussing the role of spans in quantum theory:

The relationship between spans and bimodules is briefly discussed in

The relation to van Kampen colimits is discussed in

The universal property of categories of spans is due to

and further discussed in:

  • R. Dawson, Robert Paré, Dorette Pronk, Universal properties of Span, Theory and Appl. of Categories 13, 2004, No. 4, 61-85, TAC, MR2005m:18002

  • R. Dawson, Robert Paré, Dorette Pronk, The span construction, Theory Appl. Categ. 24 (2010), No. 13, 302–377, TAC MR2720187

  • Charles Walker?, Universal properties of bicategories of polynomials, Journal of Pure and Applied Algebra 223.9 (2019): 3722-3777.

  • Charles Walker?, Bicategories of spans as generic bicategories, arXiv:2002.10334 (2020).

The structure of a monoidal tricategory on spans in 2-categories is discussed in

Generally, an (∞,n)-category of spans is indicated in section 3.2 of

Last revised on May 14, 2024 at 22:42:15. See the history of this page for a list of all contributions to it.