Proposition islatticeop_scott_open_set : @islatticeop (set_of_scott_open_set D) scott_open_set_intersection scott_open_set_bin_union. Proof. repeat split. - intros P₁ P₂ P₃ ; use eq_scott_open_set ; intro x ; cbn. + intros p. induction p as [ [ p₁ p₂ ] p₃ ]. exact (p₁ ,, p₂ ,, p₃). + intros p. induction p as [ p₁ [ p₂ p₃ ]]. exact ((p₁ ,, p₂) ,, p₃). - intros P₁ P₂ ; use eq_scott_open_set ; intro x ; cbn. + intros p. exact (pr2 p ,, pr1 p). + intros p. exact (pr2 p ,, pr1 p). - intros P₁ P₂ P₃ ; use eq_scott_open_set ; intro x. + use factor_through_squash_hProp. intro p. induction p as [ p | p ]. * revert p. use factor_through_squash_hProp. intro p. induction p as [ p | p ]. ** use hdisj_in1. exact p. ** use hdisj_in2. use hdisj_in1. exact p. * do 2 use hdisj_in2. exact p. + use factor_through_squash_hProp. intro p. induction p as [ p | p ]. * do 2 use hdisj_in1. exact p. * revert p. use factor_through_squash_hProp. intro p. induction p as [ p | p ]. ** use hdisj_in1. use hdisj_in2. exact p. ** use hdisj_in2. exact p. - intros P₁ P₂ ; use eq_scott_open_set ; intro x. + use factor_through_squash_hProp. intro p. induction p as [ p | p ]. * use hdisj_in2. exact p. * use hdisj_in1. exact p. + use factor_through_squash_hProp. intro p. induction p as [ p | p ]. * use hdisj_in2. exact p. * use hdisj_in1. exact p. - intros P₁ P₂ ; use eq_scott_open_set ; intro x. + intro p. induction p as [ p q ]. exact p. + intro p. refine (p ,, _). use hdisj_in1. exact p. - intros P₁ P₂ ; use eq_scott_open_set ; intro x. + use factor_through_squash_hProp. intros p. induction p as [ p | p ]. * exact p. * exact (pr1 p). + intro p. use hdisj_in1. 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.