Proposition is_regular_glb {H : complete_heyting_algebra} {I : UU} (f : I → regular_element H) : is_regular_element (/\_{ i : I } f i). Proof. use make_is_regular_element. use cha_le_glb. intros i ; cbn. rewrite <- (is_regular_regular_element (f i)). use cha_not_antimonotone. use cha_not_antimonotone. exact (cha_glb_le_pt f 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.