Proposition is_scott_open_union {D : dcpo} {I : UU} (P : I → scott_open_set D) : is_scott_open (⋃ P). Proof. split. - intros x y p q. revert p. use factor_through_squash_hProp. intros i. induction i as [ i Hi ]. refine (hinhpr (i ,, _)). exact (is_scott_open_upper_set (P i) Hi q). - intros A. use factor_through_squash_hProp. intros i. induction i as [ i Hi ]. refine (factor_through_squash_hProp _ _ (is_scott_open_lub_inaccessible (P i) A Hi)). intros j. induction j as [ a Ha ]. refine (hinhpr (a ,, _)). exact (hinhpr (i ,, Ha)). Qed.
Require Import UniMath.MoreFoundations.All. 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.Basis.Continuous.