Definition directed_complete_poset_discrete_partial_order : directed_complete_poset (discrete_partial_order A). Proof. intros I D HD. assert (h := is_directed_el HD). revert h. use factor_through_squash. { apply isaprop_lub. } intro i. use make_lub. - exact (D i). - split. + intros j ; cbn. assert (h := is_directed_top HD i j). revert h. use factor_through_squash. { apply setproperty. } cbn. intros k. induction k as [ k [ p q ]]. rewrite p, q. apply idpath. + intros a p ; cbn in *. apply p. 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. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.