Proposition rounded_ideal_completion_compact_basis_laws : compact_basis_laws (rounded_ideal_completion B) (rounded_ideal_completion_basis_data B). 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.
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.