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.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Algebra.Monoids. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.