Proposition is_glb_glb_regular_element {H : complete_heyting_algebra} {I : UU} (f : I → regular_element H) : is_greatest_lowerbound_lattice (regular_element_lattice H) f (glb_regular_element f). Proof. split. - intros i ; use eq_regular_element. exact (cha_glb_le_pt (λ j, (f j : H)) i). - intros x Hx ; use eq_regular_element ; cbn ; cbn in x. use (@cha_le_glb H I (λ j, (f j : H)) x). intros i ; cbn. exact (maponpaths pr1 (Hx i)). 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.