Proposition cha_basis_laws_rounded_ideal_completion : cha_basis_laws cha_basis_data_rounded_ideal_completion. Proof. repeat split. - cbn. intros ? ? ? p q. exact (trans_abstract_basis p q). - intros X. exact (cha_basis_eq (cha_basis_scott_open_cha (rounded_ideal_completion B) (rounded_ideal_completion_basis B)) X). - intros b₁ b₂ p. use scott_open_cha_le. intros I q. cbn in p ; cbn -[way_below] in q ; cbn -[way_below]. refine (trans_way_below _ q). use lt_way_below. exact p. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Examples.IdealCompletion. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting.