implemented ordered monoids, pregroups, proved unicity of adjoints, "distributivity", identity and contravariance