Proposition is_scott_open_pr2 (P : scott_open_set (A × B)) (a : A) : is_scott_open (λ b, P (a ,, b)). Proof. split. - intros b₁ b₂ p₁ p₂. use (is_scott_open_upper_set P p₁). split. + apply refl_dcpo. + exact p₂. - intros D Dp. pose (is_scott_open_lub_inaccessible P (prod_directed_set_dcpo (const_directed_set A a D (directed_set_el D)) 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 (pr2 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.