The basic way to define a partial map $X\rightharpoonup Y$ in a category is as a span $X\hookleftarrow U\to Y$ in which the first map (the support) is mono and we call the second evaluation. These are composed using pullbacks (inverse images).
In order to form unions of partial maps, for example as semantics for recursion, the unions of supports must agree with colimits of evaluations.
Who first formulated the conditions below?
Is there any systematic investigation of them in other categories besides pretoposes?
(1) For the initial object $\emptyset$ to be the least subobject, all maps $\emptyset\to X$ must be mono. This is true in $\mathbf{Set}$ and various categories of spaces, but fails for rings, unless we fix the characteristic.
(2) For filtered colimits and directed unions to agree, we require:
- the maps in the diagram to be mono;
- the maps in the colimiting cocone to be mono;
- for any other cocone consisting of monos, the colimit mediator must also be mono.
Again this happens for $\mathbf{Set}$ but the last part fails for its opposite. We may simply require filtered colimits of monos to be preserves by pullbacks, but this doesn't generalise to factorisation systems.
(3) The situation for binary colimits and unions is more complicated. In order that two partial functions have a join, they must agree on their intersection.
One part of this actually has a name, the amalgamation lemma. In a pretopos, the pushout of a pair of monos is another pair of monos and the square is also a pullback. This also happens in $\mathbf{Set}^{\mathsf{op}}$.
The other part holds in a pretopos but fails in $\mathbf{Set}^{\mathsf{op}}$. It is this: if $A$, $B$, $E$ and $C$ form a pullback and $A$, $B$, $D$ and $C$ form a pushout, with all these maps mono, then the mediator $d:D\to E$ is also mono.
My own context is Sections 4 and 9 of my draft paper on well founded coalgebras, where I replace monos with factorisation systems.
