Definition PartialOrder_boolset : PartialOrder boolset. Proof. use make_PartialOrder. - exact (λ b₁ b₂, if b₁ then if b₂ then htrue else hfalse else htrue). - repeat split. + abstract (intros b₁ b₂ b₃ p q ; induction b₁, b₂, b₃ ; induction p ; induction q ; apply tt). + abstract (intros b ; induction b ; exact tt). + abstract (intros b₁ b₂ p q ; induction b₁, b₂ ; induction p ; induction q ; apply idpath). Defined.
Require Import UniMath.MoreFoundations.All.