Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’m very sorry for not responding earlier.
Here the monad takes a category to the free symmetric monoidal category generated by . The objects of are finite tuples of objects of , say ; a morphism from to consists of a bijection (so ) together with morphisms for . Hopefully it is clear how morphisms compose. The construction is akin to a wreath product from group theory.
When applied to the terminal category , this construction is the category (or rather groupoid) of finite permutations . Objects of may be identified with natural numbers (we identify with the unique -tuple of objects of ), and morphisms just amount to bijections , i.e., permutations of . This category is equivalent to the category of finite sets and bijections between them.
Let me know if other points need clarification.
1 to 2 of 2