Proposition is_lub_sieve_type_union (I : UU) (SI : I → sieve) : is_least_upperbound_lattice bounded_lattice_set_of_sieves SI (sieve_type_union I SI). Proof. split. - intro i. use eq_sieve ; intro x. + intro pq. induction pq as [ p q ]. exact p. + intro p. exact (p ,, hinhpr (i ,, p)). - intros T HT. use eq_sieve ; intro x. + intros pq. induction pq as [ p q ]. revert p. use factor_through_squash_hProp. intros ir. exact (hinhpr ir). + use factor_through_squash_hProp. intros ir. refine (hinhpr ir ,, _). induction ir as [ i r ]. exact (pr2 (eq_sieve_r (HT i) x r)). Qed.
Require Import UniMath.Foundations.All. 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.Distributive. Require Import UniMath.OrderTheory.Lattice.Heyting. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting. Require Import UniMath.OrderTheory.Lattice.Examples.FromPartialOrder.