Unary Containers and pertinent Constructions


(* ---                                                                                -*)
This file contains a formalisation of Unitary container types. We aslo present some basic constructions on containers such as : sums, products, and compositions, as well as their extensions to container morphisms.