Proposition is_scott_open_pr1 (P : scott_open_set (A × B)%dcpo) (b : B) : is_scott_open (λ a, P (a ,, b)). Proof. split. - intros a₁ a₂ p₁ p₂. use (is_scott_open_upper_set P p₁). split. + exact p₂. + apply refl_dcpo. - intros D Dp. pose (is_scott_open_lub_inaccessible P (prod_directed_set_dcpo D (const_directed_set B b D (directed_set_el D)))) as p. rewrite prod_dcpo_lub' in p. rewrite const_lub in p. assert (H := p Dp). revert H. use factor_through_squash_hProp. intros ( i & H ) ; cbn in i, H. refine (hinhpr (pr1 i ,, _)). exact H. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. 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.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal.