Definition Equalizer_order : PartialOrder Eq. Proof. simple refine (_ ,, ((_ ,, _) ,, _)). - exact (λ x y, RX (pr1 x) (pr1 y)). - abstract (exact (λ x y z p q, trans_PartialOrder RX p q)). - abstract (exact (λ x, refl_PartialOrder RX (pr1 x))). - abstract (intros x y p q ; use subtypePath ; [ intro ; apply (pr2 Y) | ] ; exact (antisymm_PartialOrder RX p q)). Defined.
Require Import UniMath.MoreFoundations.All.