Definition closed_sieves_partial_order : PartialOrder set_of_closed_sieves. Proof. use make_PartialOrder. - exact (λ (S₁ S₂ : closed_sieve), subset_sieve S₁ S₂). - repeat split. + abstract (refine (λ (S₁ S₂ S₃ : closed_sieve), _) ; exact (istrans_subset_sieve S₁ S₂ S₃)). + abstract (refine (λ (S : closed_sieve), _) ; exact (isrefl_subset_sieve S)). + abstract (refine (λ (S₁ S₂ : closed_sieve) p q, _) ; use eq_closed_sieve ; exact (eq_sieve 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.