Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Sorting.Sorting.
Require Import Beroal.Init.

Definition functor_pres_id (e : Type) (xs : list e)
        : xs = map (@Beroal.Init.id _) xs.

Definition singleton (e : Type) (x : e) := x :: nil.

Check fun (e0 e1 : Type) (f : e0 -> e1) (x : e0)
        => (refl_equal _) : map f (singleton x) = singleton (f x).

Definition flat_map_app (e0 e1 : Type) (f : e0 -> list e1) ys xs
        : flat_map f (xs ++ ys) = flat_map f xs ++ flat_map f ys.

Definition join (e : Type) := @flat_map (list e) _ (@id _).

Definition flat_map_nt_law0 (e0 e1 e2 : Type) (f : e1 -> e2)
        (xs : list e0) (fy : e0 -> list e1)
        : map f (flat_map fy xs) = flat_map (cf (map f) fy) xs.

Definition flat_map_nt_law1 (e0 e1 e2 : Type) (f : e0 -> e1)
        (xs : list e0) (fy : e1 -> list e2)
        : flat_map fy (map f xs) = flat_map (cf fy f) xs.

Definition monad_id_left (e0 e1 : Type) (fy : e0 -> list e1) (x : e0)
        : fy x = flat_map fy (singleton x).

Definition monad_id_right (e : Type) (xs : list e)
        : xs = flat_map (@singleton _) xs.

Definition monad_assoc (e0 e1 e2 : Type)
        (fy : e0 -> list e1) (fz : e1 -> list e2) (xs : list e0)
        : flat_map fz (flat_map fy xs) = flat_map (fun x => flat_map fz (fy x)) xs.

Definition sort_singleton (e : Type) (le0 : relation e)
        (dec : forall x y : e, {le0 x y} + {le0 y x})
        x : sort le0 (singleton x).