proposition: Proposition is_scott_open_pr1 (P : scott_open_set (A × B)%dcpo) (b : B) : is_scott_open (λ a, P (a ,, b)).
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Elements.Maximal