proposition: Proposition is_lub_equalizer_lub (D : directed_set (Equalizer_order X Y f g)) : is_least_upperbound (Equalizer_order X Y f g) D (equalizer_lub_el D ,, equalizer_lub_path D).
proof: Proof. split. - intros i. refine (less_than_dcpo_lub (Equalizer_directed_set D) _ i _). apply refl_dcpo. - intros y Hy. use (dcpo_lub_is_least (Equalizer_directed_set D)). intro i. exact (Hy i). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous