proposition: Proposition irrefl_intrinsic_apartness (x : X) : ¬(x # x).
proof: Proof. use factor_through_squash. { apply isapropempty. } intros p. induction p as [ p | p ]. - apply (irrefl_dcpo_not_specialization x). exact p. - apply (irrefl_dcpo_not_specialization x). exact p. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Basis.Continuous