Prove that Permutation' n is isomorphic to Fin (n !)

[Taneb]

There are exactly n ! permutations on n elements. We should prove this. It would be useful for, for example, finite group theory.

I had a bit of a go, but I found I was missing a remove-cong function for proving the isomorphism holds.

[jamesmckinna]

You might also want to look at this talk by Patrik Jansson which I heard last week.

[JacquesCarette]

I had done Lehmer codes, up to (but not including) composition. I could never quite figure out Split. Scoured the internet, asked on forums - nothing. So: yay to Patrik!

I should point out to him that it's not just symmetric monoidal category, it's a symmetric rig groupoid!

[jamesmckinna]

(re: groupoids) I had meant to, after his talk, but it got lost in the wash of other discussion. But yes. he tells me there's a version (of the view) which is also indexed by the semantics, but I've yet to see the details.