Definition sieve_intersection (S₁ S₂ : sieve) : sieve. Proof. use make_sieve. - exact (λ x, S₁ x ∧ S₂ x). - abstract (intros x y p q ; induction q as [ q₁ q₂ ] ; exact (sieve_downwards_closed S₁ p q₁ ,, sieve_downwards_closed S₂ p q₂)). Defined.
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.