Proposition lub_regular_element_eq {H : complete_heyting_algebra} (I : UU) (f : I → regular_element H) : lub_regular_element I f = not_not_regular_element (\/_{ i : I } f i). Proof. use eq_regular_element. use cha_le_antisymm. - cbn -[lub_regular_element]. use cha_to_le_exp. refine (cha_le_trans _ (cha_exp_eval (¬ (\/_{ i } f i)) _)). use cha_and_monotone_l. refine (lub_regular_element_le f (not_not_regular_element (\/_{ i : I } f i)) _). intro i ; cbn. refine (cha_le_trans (cha_not_not _) _). use cha_not_not_monotone. exact (cha_le_lub_pt f i). - use cha_le_glb. intro i. induction i as [ x p ] ; cbn. rewrite <- (is_regular_regular_element x). use cha_not_not_monotone. use cha_lub_le. intro i ; cbn. use from_le_regular_element_lattice. apply p. 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.