Sorting algorithms (#572)

In these pull request, I have defined some sorting algorithms. To do so,
I have :
- Defined new concepts in order theory: decidable preorders, decidable
posets, total decidable preorders (I have proved that for every `X
: total-decidable-preorder` and every `x y : X` the type `x \leq y +
\neg (x \= y) \times(y \leq x) ` is inhabited) and total decidable
posets (I have proved that the previous type is a proposition)
- Defined what is a permutation of a standard finite type and what is a
permutation of a vector and of a list
 - Defined the proposition of being sorted for a list and for a vector
- Defined what is means for a function on vectors to be a sort (It is a
permuting vector, and the result is sorted)
 - Defined Quick sort and sort by insertion
 - Proved that sort by insertion is a sort

src/finite-group-theory.lagda.md

@@ -16,9 +16,11 @@ open import finite-group-theory.finite-type-groups public
 open import finite-group-theory.groups-of-order-2 public
 open import finite-group-theory.orbits-permutations public
 open import finite-group-theory.permutations public
+open import finite-group-theory.permutations-standard-finite-types public
 open import finite-group-theory.sign-homomorphism public
 open import finite-group-theory.simpson-delooping-sign-homomorphism public
 open import finite-group-theory.subgroups-finite-groups public
 open import finite-group-theory.tetrahedra-in-3-space public
 open import finite-group-theory.transpositions public
+open import finite-group-theory.transpositions-standard-finite-types public
 ```