§
Partial function as span
A partial function
f
:
D
⊆
X
→
Y
f: D \subseteq X \to Y
f
:
D
⊆
X
→
Y
is a span of
Y
←
D
↪
X
Y \leftarrow D \hookrightarrow X
Y
←
D
↪
X
.
What a slick definition!
See that if
Y
=
1
Y = 1
Y
=
1
, then a partial function
X
→
1
X \to 1
X
→
1
carries only the data of
D
↪
X
D \hookrightarrow X
D
↪
X
, giving us
subobjects.