Proposition prod_is_scott_open (PA : scott_open_set A) (PB : scott_open_set B) : is_scott_open (λ (x : (A × B)%dcpo), PA (pr1 x) ∧ PB (pr2 x)). Proof. split. - intros ( a₁ & b₁ ) ( a₂ & b₂ ) ( p₁ & p₂ ) ( q₁ & q₂ ). exact (is_scott_open_upper_set PA p₁ q₁ ,, is_scott_open_upper_set PB p₂ q₂). - intros D ( p & q ). rewrite prod_dcpo_lub in p, q. cbn in p, q. assert (H₁ := is_scott_open_lub_inaccessible PA (directed_set_comp π₁ D) p). assert (H₂ := is_scott_open_lub_inaccessible PB (directed_set_comp π₂ D) q). revert H₁. use factor_through_squash_hProp. intros ( i₁ & H₁ ) ; cbn in i₁, H₁. revert H₂. use factor_through_squash_hProp. intros ( i₂ & H₂ ) ; cbn in i₂, H₂. assert (H₃ := directed_set_top D i₁ i₂). revert H₃. use factor_through_squash_hProp. intros ( k & r₁ & r₂ ) ; cbn in k, r₁, r₂. refine (hinhpr (k ,, _ ,, _)). + exact (is_scott_open_upper_set PA H₁ (pr1 r₁)). + exact (is_scott_open_upper_set PB H₂ (pr2 r₂)). 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.