Definition exponential_is_exponential (exp : exponential) : ∏ x y z : X, z ≤ (exponential_map exp x y) <-> (z ∧ x) ≤ y := pr2 exp.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Algebra.Monoids. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.