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. 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.
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.