Library UniMath.OrderTheory.Lattice.Heyting
Require Import UniMath.Foundations.Preamble.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.OrderTheory.Lattice.Lattice.
Require Import UniMath.OrderTheory.Lattice.Bounded.
Section Def.
Context {X : hSet} (L : lattice X).
Local Notation "x ≤ y" := (Lle L x y).
Local Notation "x ∧ y" := (Lmin L x y).
An exponential is a binary operation on X satisfying this law
Definition exponential : UU :=
∑ exponential_map : X -> X -> X,
∏ x y z : X, z ≤ (exponential_map x y) <-> (z ∧ x) ≤ y.
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.
Definition exponential_map (exp : exponential) : X -> X -> X := pr1 exp.
Coercion exponential_map : exponential >-> Funclass.
Definition exponential_is_exponential (exp : exponential) :
∏ x y z : X, z ≤ (exponential_map exp x y) <-> (z ∧ x) ≤ y := pr2 exp.
End Def.
∑ exponential_map : X -> X -> X,
∏ x y z : X, z ≤ (exponential_map x y) <-> (z ∧ x) ≤ y.
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.
Definition exponential_map (exp : exponential) : X -> X -> X := pr1 exp.
Coercion exponential_map : exponential >-> Funclass.
Definition exponential_is_exponential (exp : exponential) :
∏ x y z : X, z ≤ (exponential_map exp x y) <-> (z ∧ x) ≤ y := pr2 exp.
End Def.