proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness