fact: Definition make_exponential (exponential_map : X -> X -> X) (prop : ∏ x y z : X, z ≤ (exponential_map x y) <-> (z ∧ x) ≤ y) : exponential := tpair _ exponential_map prop.
imports: UniMath.Foundations.Preamble UniMath.Algebra.Monoids UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded