Proposition equalizer_lub_path (D : directed_set (Equalizer_order X Y f g)) : f (equalizer_lub_el D) = g (equalizer_lub_el D). 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.