Andrej, You can say that finite sets and injective functions is (up-to equivalence) the free symmetric monoidal category with an initial unit, on one generator. I think this is quite well known. I first learnt it from Marcelo Fiore, a long time ago, and we referred to it in our paper Comparing Operational Models of Name-Passing Process Calculi Information and Computation vol 204. 2006. I've also seen John Power refer to the result, e.g. in Semantics for Local Computational Effects MFPS XXII. ENTCS vol 158. 2006. I am intrigued about what you will use the category for. Sam On 4 Dec 2008, at 09:11, Andrej Bauer wrote:
The category of finite sets and functions may be characterized (up to equivalence) as the category with finite coproducts freely generated from one object. Is there a similar nice characterization for the category of finite sets and _injective_ functions?
Best regards,
Andrej