proposition: Proposition lub_of_ideals (D : directed_set (funset_dcpo B hProp_dcpo)) (HD : ∏ (d : D), is_ideal (D d)) : is_ideal (⨆ D).
proof: Proof. simple refine (_ ,, _ ,, _). - assert (H := directed_set_el D). revert H. use factor_through_squash. { apply propproperty. } intro d. assert (H := is_ideal_el (HD d)). revert H. use factor_through_squash. { apply propproperty. } intro b. induction b as [ b p ]. exact (hinhpr (b ,, hinhpr (d ,, p))). - intros a₁ a₂. use factor_through_squash. { apply propproperty. } intros Ha₁ ; cbn in Ha₁. induction Ha₁ as [ d₁ p₁ ]. use factor_through_squash. { apply propproperty. } intros Ha₂ ; cbn in Ha₂. induction Ha₂ as [ d₂ p₂ ]. assert (H := directed_set_top D d₁ d₂). revert H. use factor_through_squash. { apply propproperty. } intro H ; cbn in H. induction H as [ dt [ H₁ H₂ ]]. assert (H := is_ideal_top (HD dt) (H₁ a₁ p₁) (H₂ a₂ p₂)). revert H. use factor_through_squash. { apply propproperty. } intros H. induction H as ( b & q₁ & q₂ & q₃ ). exact (hinhpr (b ,, hinhpr (dt ,, q₁) ,, q₂ ,, q₃)). - intros a b. use factor_through_squash. { apply propproperty. } intros H q ; cbn in H. induction H as [ d p ] ; cbn. refine (hinhpr (d ,, _)). exact (is_ideal_lower_set (HD d) p q). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Basis.Algebraic UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.CompactBasis UniMath.OrderTheory.DCPOs.Elements.Maximal UniMath.OrderTheory.DCPOs.Examples.Products UniMath.OrderTheory.DCPOs.Examples.SubDCPO UniMath.OrderTheory.DCPOs.Examples.Propositions