proposition: Proposition equalizer_lub_path (D : directed_set (Equalizer_order X Y f g)) : f (equalizer_lub_el D) = g (equalizer_lub_el D).
proof: Proof. unfold equalizer_lub_el. rewrite !scott_continuous_map_on_lub. use antisymm_dcpo. - use dcpo_lub_is_least. intro i. use less_than_dcpo_lub ; [ exact i | ]. change ((f {{Equalizer_directed_set D}}) i) with (f (pr1 (D i))). change ((g {{Equalizer_directed_set D}}) i) with (g (pr1 (D i))). rewrite (pr2 (D i)). apply refl_dcpo. - use dcpo_lub_is_least. intro i. use less_than_dcpo_lub ; [ exact i | ]. change ((f {{Equalizer_directed_set D}}) i) with (f (pr1 (D i))). change ((g {{Equalizer_directed_set D}}) i) with (g (pr1 (D i))). rewrite (pr2 (D i)). apply refl_dcpo. 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