Definition hProp_lub {D : UU} {f : D → hProp} (Hf : is_directed hProp_PartialOrder f) : lub hProp_PartialOrder f. Proof. use make_lub. - exact (∃ (d : D), f d). - refine (_ ,, _). + exact (λ d x, hinhpr (d ,, x)). + abstract (intros P HP ; use factor_through_squash ; [ apply propproperty | ] ; intro x ; exact (HP (pr1 x) (pr2 x))). 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.