Proposition preimage_scott_open {X Y : dcpo} (f : scott_continuous_map X Y) {P : Y → hProp} (HP : is_scott_open P) : is_scott_open (λ x, P (f x)). Proof. split. - intros y₁ y₂ p q. use (is_scott_open_upper_set HP p). apply (is_monotone_scott_continuous_map f). exact q. - intros D H. rewrite scott_continuous_map_on_lub in H. assert (H' := is_scott_open_lub_inaccessible HP _ H). revert H'. use factor_through_squash_hProp. exact (λ ip, hinhpr ip). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness.