Definition Equalizer_directed_set (D : directed_set (Equalizer_order X Y f g)) : directed_set X. Proof. use make_directed_set. - exact D. - exact (λ i, pr1 (D i)). - abstract (refine (directed_set_el D ,, _) ; intros i j ; assert (k := directed_set_top D i j) ; revert k ; use factor_through_squash ; [ apply propproperty | ] ; intros k ; induction k as [ k [ H₁ H₂ ]] ; exact (hinhpr (k ,, (H₁ ,, H₂)))). Defined.
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.