Proposition cha_basis_laws_scott_open_cha : cha_basis_laws cha_basis_data_scott_open_cha. Proof. repeat split ; cbn -[way_below]. - intros b₁ b₂ b₃ p q. exact (trans_way_below p q). - intros X. use eq_scott_open_set. + intros x p. assert (Hx : X (⨆ directed_set_from_basis B x)). { rewrite (approximating_basis_lub B x). exact p. } pose proof (is_scott_open_lub_inaccessible X (directed_set_from_basis B x) Hx) as q. revert q. use factor_through_squash_hProp. intros b. induction b as [ [ b q₁ ] q₂ ]. cbn in q₂ ; unfold basis_below_map in q₂ ; cbn in q₂. use hinhpr. simple refine ((_ ,, _) ,, _). * exact b. * use bounded_lattice_scott_open_set_le ; cbn -[way_below]. intros y r. refine (is_scott_open_upper_set X q₂ _). use way_below_to_le. exact r. * cbn -[way_below]. exact q₁. + intros x. use factor_through_squash_hProp. cbn -[way_below]. intro b. induction b as [ [ b p ] q ]. exact (from_bounded_lattice_scott_open_set_le p q). - intros b₁ b₂ p. use scott_open_cha_le ; cbn -[way_below]. intros x q. exact (trans_way_below p q). 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.