Definition closed_sieve_min_el : min_el closed_sieves_poset. Proof. simple refine (_ ,, _). - exact (closed_sieve_type_intersection closed_sieve (idfun closed_sieve)). - abstract (intros S x H ; cbn in * ; exact (H 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.