Proposition regular_element_islatticeop (H : complete_heyting_algebra) : islatticeop (λ (x y : set_of_regular_elements H), conj_regular_element x y) (λ (x y : set_of_regular_elements H), disj_regular_element x y). Proof. repeat split. - intros x y z ; use eq_regular_element ; cbn. apply cha_min_assoc. - intros x y ; use eq_regular_element ; cbn. apply cha_min_comm. - intros x y z ; use eq_regular_element ; cbn ; cbn in x, y, z. use cha_le_antisymm. + refine (cha_le_trans _ _) ; [ rewrite <- (is_regular_regular_element z) | rewrite <- (is_regular_regular_element x) ]. { apply cha_le_refl. } rewrite !cha_not_not_disj_not. rewrite !cha_conj_not. use cha_not_not_monotone. rewrite cha_max_assoc. apply cha_le_refl. + refine (cha_le_trans _ _) ; [ rewrite <- (is_regular_regular_element x) | rewrite <- (is_regular_regular_element z) ]. { apply cha_le_refl. } rewrite !cha_not_not_disj_not. rewrite !cha_conj_not. use cha_not_not_monotone. rewrite cha_max_assoc. apply cha_le_refl. - intros x y ; use eq_regular_element ; cbn. rewrite cha_max_comm. apply idpath. - intros x y ; use eq_regular_element ; cbn. use cha_le_antisymm. + apply cha_min_le_l. + use cha_min_le_case. { apply cha_le_refl. } rewrite <- cha_conj_not. refine (cha_le_trans _ _). { rewrite <- (is_regular_regular_element x). apply cha_le_refl. } use cha_not_antimonotone. use cha_min_le_l. - intros x y ; use eq_regular_element ; cbn. rewrite cha_max_absorb. rewrite is_regular_regular_element. apply idpath. 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.