Definition make_closed_sieve (S : sieve) (H : is_closed_sieve S) : closed_sieve := S ,, H. Coercion closed_sieve_to_sieve (S : closed_sieve) : sieve. Proof. exact (pr1 S). 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.