Proposition bounded_latticeop_scott_open_set : bounded_latticeop lattice_scott_open_set (false_scott_open_set D) (true_scott_open_set D). Proof. repeat split. - intros P ; use eq_scott_open_set ; intro x. + use factor_through_squash_hProp. intros p. induction p as [ p | p ]. * apply fromempty. exact p. * exact p. + intro p. use hdisj_in2. exact p. - intros P ; use eq_scott_open_set ; intro x. + intro p. exact (pr2 p). + intro p. exact (tt ,, 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.