Proposition irrefl_intrinsic_apartness (x : X) : ¬(x # x). 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.
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.Basis.Continuous.