Proposition rounded_ideal_completion_basis_laws : dcpo_basis_laws rounded_ideal_completion rounded_ideal_completion_basis_data. 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.
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.