Proposition isPartialOrder_discrete_hrel : isPartialOrder discrete_hrel. Proof. refine ((_ ,, _) ,, _). - intros x y z p q. exact (p @ q). - exact (λ x, idpath _). - exact (λ x y p q, p). Qed.
Require Import UniMath.MoreFoundations.All.