Definition sieve_exponential (S₁ S₂ : sieve) : sieve. Proof. use make_sieve. - exact (λ x, subset_sieve (sieve_intersection S₁ (lower_elements_sieve x)) S₂). - abstract (intros x y p q z r ; cbn in * ; apply q ; refine (pr1 r ,, _) ; exact (istrans_posetRelation _ _ _ _ (pr2 r) p)). 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.