Definition unit_PartialOrder : PartialOrder unitset. Proof. use make_PartialOrder. - exact (λ _ _, htrue). - repeat split. intros x y p q. apply isapropunit. Defined.
Require Import UniMath.MoreFoundations.All.