Proposition regular_element_is_exponential {H : complete_heyting_algebra} (x y z : regular_element H) : Lle (regular_element_lattice H) z (impl_regular_element x y) <-> Lle (regular_element_lattice H) (conj_regular_element z x) y. Proof. split. - intro p. apply from_le_regular_element_lattice in p. use to_le_regular_element_lattice. cbn. refine (cha_le_trans _ _). { exact (cha_and_monotone_l p). } refine (cha_le_trans _ _). { apply conj_lub_regular_element. } refine (cha_le_trans _ _). { use (lub_regular_element_pt_le _ (λ _, y)). cbn. intro i. induction i as [ w Hw ] ; cbn. exact Hw. } use lub_regular_element_le. intro i ; cbn. apply cha_le_refl. - intro p. apply from_le_regular_element_lattice in p. use to_le_regular_element_lattice. cbn ; cbn in p. use cha_le_glb. intros i ; induction i as [ w q ] ; cbn. refine (cha_le_trans _ (cha_min_le_r z w)). assert ((z ∧ w) = z) as ->. { exact (maponpaths pr1 (q (z ,, p))). } apply cha_le_refl. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting. Require Import UniMath.OrderTheory.Lattice.DerivedLawsCompleteHeyting.