scratch
§
Partial Function as Span
created 2022-09-28
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.
❦