Definition Equalizer_pointed_PartialOrder : pointed_PartialOrder Eq. Proof. use make_pointed_PartialOrder. - exact (Equalizer_order RX Y f g). - refine (⊥_{RX} ,, _). abstract (rewrite (strict_function_on_point Hf) ; rewrite (strict_function_on_point Hg) ; apply idpath). - intros x. apply pointed_PartialOrder_min_point. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.