Proposition bounded_lattice_laws_set_of_sieves : bounded_latticeop lattice_set_of_sieves empty_sieve full_sieve. Proof. repeat split. - intros S. use eq_sieve ; intro x. + use factor_through_squash_hProp. intros p. induction p as [ p | p ]. * apply fromempty. exact p. * exact p. + intro p. exact (hinhpr (inr p)). - intros S. use eq_sieve ; intro x ; cbn. + intros pq. exact (pr2 pq). + intros p. exact (tt ,, p). 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.