Proposition is_sharp_continuous_dcpo {X : dcpo} (CX : continuous_dcpo_struct X) (x : X) : is_sharp x ≃ (∀ (y z : X), y ≪ z ⇒ (y ≪ x ∨ z ⊄ x))%logic. Proof. use weqimplimpl. - intros Hx y z p. assert (H := unary_interpolation CX p). revert H. use factor_through_squash. { apply propproperty. } intro u. induction u as [ u [ q₁ q₂ ]]. assert (H := unary_interpolation CX q₂). revert H. use factor_through_squash. { apply propproperty. } intro v. induction v as [ v [ r₁ r₂ ]]. specialize (Hx u v r₁). revert Hx. use factor_through_squash. { apply propproperty. } intro s. induction s as [ s | s ]. + refine (hinhpr (inl _)). exact (trans_way_below q₁ s). + cbn in s. refine (hinhpr (inr _)). use (invmap (continuous_not_specialization_weq CX z x)). exact (hinhpr (v ,, r₂ ,, s)). - intros Hx y z p. specialize (Hx y z p). revert Hx. use factor_through_squash. { apply propproperty. } intro q. induction q as [ q | q ]. + exact (hinhpr (inl q)). + refine (hinhpr (inr _)). apply dcpo_not_specialization_le. exact q. - apply propproperty. - apply propproperty. 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.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.