proposition: Proposition rounded_ideal_completion_basis_laws : dcpo_basis_laws rounded_ideal_completion rounded_ideal_completion_basis_data.
proof: Proof. intro I. split. - split. + assert (H := is_ideal_el (pr2 I)). revert H. use factor_through_squash. { apply propproperty. } intros b. induction b as [ b p ]. refine (hinhpr (b ,, _)). apply principal_ideal_way_below. exact p. + intros b₁ b₂. induction b₁ as [ b₁ p₁ ]. induction b₂ as [ b₂ p₂ ]. cbn -[way_below] in b₁, p₁, b₂, p₂. assert (H := p₁ _ (rounded_ideal_lub_1 I)). revert H. use factor_through_squash. { apply propproperty. } intros c₁. induction c₁ as ( ( c₁ & q₁ ) & s₁ ). assert (H := p₂ _ (rounded_ideal_lub_1 I)). revert H. use factor_through_squash. { apply propproperty. } intros c₂. induction c₂ as ( ( c₂ & q₂ ) & s₂ ). cbn in c₁, q₁, s₁, c₂, q₂, s₂. assert (H := is_ideal_top (pr2 I) q₁ q₂). revert H. use factor_through_squash. { apply propproperty. } intros t. induction t as ( t & r₁ & r₂ & r₃ ). simple refine (hinhpr ((t ,, _) ,, (_ ,, _))) ; cbn -[way_below]. * apply principal_ideal_way_below. exact r₁. * intros x v. refine (trans_abstract_basis _ r₂). use s₁. exact v. * intros x v. refine (trans_abstract_basis _ r₃). use s₂. exact v. - split. + intros b x p. induction b as [ b q ]. cbn -[way_below] in b, q, p. exact (way_below_to_le q x p). + intros I' HI' x p. assert (H := is_ideal_rounded (pr2 I) p). revert H. use factor_through_squash. { apply propproperty. } intros b. induction b as [ b [ q₁ q₂ ]]. assert (H : principal_ideal b ≪ I). { apply principal_ideal_way_below. exact q₂. } exact (HI' (b ,, H) x 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