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