Here's an exercise from Leinster's Basic Category Theory:
The question that arose are:
(1) I believe the definition of $\mathbf{Ord}$ on maps in $\mathscr B$ is is follows. Given a bijection of finite sets $f:B\to B'$, assign to it the function $\mathbf{Ord}(f):\mathbf{Ord}(B)\to\mathbf{Ord}(B')$ defined as follows. Every element of $\mathbf{Ord}(B)$ is a subset of $B\times B$. For every $(b,\hat b)$ in that subset, assign to it $(f(b),f(\hat b))$. Thus obtained set of pairs is then the image of the element of $\mathbf{Ord}(B)$ we started with under $\mathbf{Ord}(f)$. It is clear that $\mathbf{Ord}(f)$ is a functor as long as the set consisting of all pairs $(f(b),f(\hat b))$ lies in $\mathbf{Ord}(B')$. But it's not obvious to me that this is so. That is, why does the set of all pairs $(f(b),f(\hat b))$ for all $(b,\hat b)$ from the original element of $\mathbf{Ord}(B)$ satisfy all requirements of a total order?
(2) I don't understand the hint "consider identity permutations". Suppose there is a natural transformation $\alpha=(\alpha_B:\mathbf{Sym}(B)\to\mathbf{Ord}(B))_{B\in\mathscr B}$. Let $f:B\to B'$ be an arrow. Naturality says that $$\alpha_{B'}\circ Sym(F)=Ord(f)\circ \alpha_B$$ When applied to the id permutation, this translates to $$\alpha_{B'}(id)=Ord(f)(\alpha_B(id))$$I don't see any way to simplify this further, nor do I see any contradiction.
(3) If one uses that "a total order on a finite set amounts to a way of placing its elements in sequence", then it is clear that $Sym(X)$ has $n!$ elements where $|X|=n$. But the above quote is very informal. How to prove that $Sym(X)$ has $n!$ elements based only on formal definitions?
For (1), it is more intuitive to think of a total order $\leq$ in terms of $x\leq y$. Thus you are defining $f(x)\leq f(y)$ if and only if $x \leq y$. From this rephrasing, it's clear that $B'$ is totally ordered by the proposed relation.
(2) Well, it's only a hint, you still have to figure something out yourself. For a bigger hint, try letting $B=B'$.
(3) I discourage you from worrying about this. Math involves formality, but there's rarely any point in looking for a more formal proof of something you understand perfectly. Your argument fleshes out to the usual: there are $n$ choices for the least element, $n-1$ choices for the second least, and so on. No need to formalize further, although you could certainly give an inductive proof if you really want.