adding a collection of defintions. everyone seems to have one of these, and no one shares. this is mostly built from the danlicagda course notes, but with some changes, unficications, additions, and hottifications.
A work up of permutations on just simple lists. This differs from other
permutation definitions that I've seen in two nice ways.

First, there are no postulates. I start from a definition of a type and
prove all the properties that I want as theorems. This is in contrast to
other definitions that take relatively harmless things like reflexivity,
symmetry, and transitivity---as well as more suspect things---as axioms on
an abstract definition.

Second, the definition itself is well founded. This in contrast to a
definition that's based on something more immediately from the standard
algebraic notion that the permutation group is generated by shifts and
rotations. That definition is true, but does not translate easily into a
constructive setting becasuse it's not clear that anything is getting
smaller. The definition I give here does obviously get smaller in its
recursive calls, and therefore passes a termination checker.

The trade off is that it's only clear what one argument to the recursive
call in the definition is---the other is buried under two sigmas. This
often makes it hard to use straight forward induction (recursion) to prove
theorems (write functions) using this definition, and some more interesting
strategy is needed. This is not true in general, however, and really
depends on the exact structure of the theorem being considered.
module decl