Proposition conj_lub_regular_element {H : complete_heyting_algebra} {I : UU} (f : I → regular_element H) (y : regular_element H) : (lub_regular_element I f ∧ y) ≤ lub_regular_element I (λ i, conj_regular_element (f i) y). Proof. rewrite !lub_regular_element_eq ; cbn. rewrite <- (is_regular_regular_element y). rewrite <- cha_not_not_conj. rewrite is_regular_regular_element. use cha_not_not_monotone. rewrite (cha_min_comm _ y). rewrite cha_frobenius. use cha_lub_le. intro i. use cha_le_lub. - exact i. - cbn. rewrite (cha_min_comm y (f i)). 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.