fact: Definition directed_set_coproduct_with_eq : ((∑ (D' : D → X) (HD : is_directed X D'), let DX := make_directed_set _ D D' HD in (is_least_upperbound (coproduct_PartialOrder X Y) D (inl (⨆ DX))) × (∏ (i : D), D i = inl (D' i))) ∨ (∑ (D' : D → Y) (HD : is_directed Y D'), let DY := make_directed_set _ D D' HD in is_least_upperbound (coproduct_PartialOrder X Y) D (inr (⨆ DY)) × (∏ (i : D), D i = inr (D' i))))%type.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous