proposition: Proposition rounded_ideal_completion_compact_basis_laws : compact_basis_laws (rounded_ideal_completion B) (rounded_ideal_completion_basis_data B).
proof: Proof. refine (_ ,, _ ,, _). - intros b ; cbn -[way_below] in *. apply principal_ideal_way_below. apply HB. - intro I. 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 ,, _)). intros x q ; cbn in q. exact (is_ideal_lower_set (pr2 I) p q). + intros b₁ b₂. induction b₁ as [ b₁ p₁ ]. induction b₂ as [ b₂ p₂ ]. cbn in b₁, p₁, b₂, p₂. assert (Hb₁ : in_rounded_ideal B b₁ I). { apply p₁. apply HB. } assert (Hb₂ : in_rounded_ideal B b₂ I). { apply p₂. apply HB. } assert (H := is_ideal_top (pr2 I) Hb₁ Hb₂). revert H. use factor_through_squash. { apply propproperty. } intro t. induction t as ( t & q₁ & q₂ & q₃ ). simple refine (hinhpr ((t ,, _) ,, _ ,, _)) ; cbn. * intros x r. exact (is_ideal_lower_set (pr2 I) q₁ r). * intros x r. exact (trans_abstract_basis r q₂). * intros x r. exact (trans_abstract_basis r q₃). - intro I. split. + intros b x p. induction b as [ b q ]. cbn in b, q, p. apply q. exact 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₂ ]]. refine (HI' (b ,, _) x q₁) ; cbn. intros c r. exact (is_ideal_lower_set (pr2 I) q₂ r). 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