Permutation

A permutation of a type $X$ is an Equivalence $X\simeq X$.

If $X$ is Finite, then the Cardinality of $X\simeq X$ is the Factorial $|X|!$.