proposition: Proposition reflect_apartness {X Y : dcpo} (f : scott_continuous_map X Y) {x y : X} : f x # f y → x # y.
proof: Proof. use factor_through_squash_hProp. intro p. induction p as [ p | p ]. - revert p. use factor_through_squash_hProp. intros ( P & HP & HPfx & HPfy ). use hdisj_in1. use hinhpr. simple refine (_ ,, _ ,, _ ,, _). + exact (λ x, P(f x)). + exact (preimage_scott_open f HP). + exact HPfx. + exact HPfy. - revert p. use factor_through_squash_hProp. intros ( P & HP & HPfx & HPfy ). use hdisj_in2. use hinhpr. simple refine (_ ,, _ ,, _ ,, _). + exact (λ x, P(f x)). + exact (preimage_scott_open f HP). + exact HPfx. + exact HPfy. 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