Definition PartialOrder_filter_le (X : UU) : PartialOrder (make_hSet (PreFilter _) (isasetPreFilter X)). Proof. simple refine (make_PartialOrder _ _). - intros F G. simple refine (make_hProp _ _). + apply (filter_le F G). + apply impred_isaprop ; intros A. apply isapropimpl. apply propproperty. - repeat split. + intros F G H ; simpl. apply istrans_filter_le. + intros A ; simpl. apply isrefl_filter_le. + intros F G ; simpl. apply isantisymm_filter_le. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.