Proposition lub_of_ideals (D : directed_set (funset_dcpo B hProp_dcpo)) (HD : ∏ (d : D), is_ideal (D d)) : is_ideal (⨆ D). 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. 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.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Algebraic. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.CompactBasis. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal. Require Import UniMath.OrderTheory.DCPOs.Examples.Products. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO. Require Import UniMath.OrderTheory.DCPOs.Examples.Propositions.