Is there an existing axiomization of an "Elementary theory of the double category of spans?"
Among other nice things a category could be then defined as a monad inside the theory of spans.
I think I want something like the Elementary theory of the category of Sets or Elementary theory of the category of categories.
I've heard vague references to an Elementary theory of the category of relations which should be similar although personally I would prefer a more double category like presentation. I guess much of the difference is spans are a little more "constructive" than relations?
As I understand things many of the same things you can do with Span you can do with Prof (the category of profunctors) so axiomizations of the category of profunctors ought to be useful as well.
I'm not sure where to start with searching for axiomizations of Span or related categories like Rel and Prof.