Recently I've been trying to understand spans better, in particular how they relate to relations, as both may be thought of as "multivalued functions between sets" (see Bruni and Gadducci - Some algebraic laws for spans (and their connections with multirelations) for a precise comparison between them).
One of the things I'd like to understand is whether we can define "functional" and "total" spans, similar to relations. Regarding the latter, recall the following pair of definitions:
Definition. A relation $R$ from a set $A$ to another set $B$ is functional if it satisfies the following equivalent conditions
- For each $a\in A$, the set $R(a)$ contains at most one element.
- We have $R\circ R^{\dagger}\subset1_B$.
Here $R^\dagger$ is the inverse relation of $R$ (the one where $a\sim_{R^\dagger}b$ iff $b\sim_Ra$) and $1_B$ is the identity relation of $B$ (the one where $b\sim_{1_B}b'$ iff $b=b'$).
Definition. A relation $R$ from a set $A$ to another set $B$ is total if it satisfies the following equivalent conditions
- For each $a\in A$, the set $R(a)$ contains at least one element.
- We have $1_A\subset R^{\dagger}\circ R$.
Here $R^\dagger$ is the inverse relaton of $R$ (the one where $a\sim_{R^\dagger}b$ iff $b\sim_Ra$) and $1_B$ is the identity relation of $B$ (the one where $b\sim_{1_B}b'$ iff $b=b'$).
Lastly, a relation that is both functional and total is actually an internal adjunction in the 2-category $\mathsf{Rel}$, and in fact all such adjunctions arise in this way.
So, following these definitions and given a span $\lambda=(A\xleftarrow{f}S\xrightarrow{g}B)$, it is natural to wonder what data morphisms of spans \begin{gather*} \lambda\circ\lambda^{\dagger} \to 1_B,\\ 1_A \to \lambda^{\dagger}\circ\lambda \end{gather*} carry, where now $1_A$ and $\lambda^\dagger$ are defined by $1_A=(A\xleftarrow{\mathrm{id}_A}A\xrightarrow{\mathrm{id}_A}A)$ and $\lambda^{\dagger}=(B\xleftarrow{g}S\xrightarrow{f}A)$. Unwinding the definitions, we see that:
- A morphism $\lambda\circ\lambda^{\dagger} \to 1_B$ consists of a map of sets $\phi$ from $$S\times_{A}S=\{(s_1,s_2)\ |\ f(s_1)=f(s_2)\}$$ to $B$ such that, for each $(s_1,s_2)\in S\times_{A}S$, we have $\phi(s_1,s_2)=b=g(s_1)=g(s_2)$.
- A morphism $1_A \to \lambda^{\dagger}\circ\lambda$ consists of a map of sets $\psi$ from $A$ to $$S\times_{B}S=\{(s_1,s_2)\ |\ g(s_1)=g(s_2)\}$$ such that, for each $a\in A$, if $\psi(a)=(s_1,s_2)$, then $a=f(s_1)=f(s_2)$.
Two special cases are clear: if $f$ is injective, then a map as in Item 1 above must be $g$, and if $g$ is injective, then the map in Item 2 is a left-inverse to $f$, implying that it is injective as well.
Question. Is there, however, a better way to think/view these morphisms in the general case? For instance:
- Every span $\lambda=(A\xleftarrow{f}S\xrightarrow{g}B)$ induces a relation from $A$ to $B$ via $a\mapsto g(f^{-1}(a))$, but it doesn't seem like the relation will necessarily be functional if we have a morphism as in Item 1 above, and the same goes for it being total.
- Moreover, whereas "functional" and "total" are a property of relations, since there is at most one morphism of the form $R\circ R^\dagger\subset1_B$ and one of the form $1_A\subset R^\dagger\circ R$, in the case of spans there may be multiple such morphisms.
- A span with maps $\lambda\circ\lambda^{\dagger} \to 1_B$ and $1_A \to \lambda^{\dagger}\circ\lambda$ satisfying the triangle identities is the same as an adjunction internal to the bicategory $\mathsf{Span}$. Is there a known characterisation of these?
Lastly, regarding question 3, the internal equivalences in $\mathsf{Span}$ are known to be just "spans representable by functions", having the form $A\xleftarrow{\mathrm{id}_A}A\xrightarrow{f}B$, so we know at least some examples of adjunctions in $\mathsf{Span}$. (By the way, what are the isomorphisms in $\mathsf{Span}$? I feel like since fibre products are defined up to isomorphism it doesn't make sense to speak about those (or there are just none?), since they involve equalities of the form $\lambda\circ\lambda^{\dagger} =1_B$ and $1_A=\lambda^{\dagger}\circ\lambda$; is this correct?)