Antisymmetric Relation

A Relation R : A → A → Ω : 𝑅 → 𝐴 𝐴 → Ω R:A\to A\to\Omega is antisymmetric if for all x , y : A : 𝑥 𝑦 𝐴 x,y:A ,

R⁢(x,y)∧R⁢(y,x)⇒x=y⇒𝑅𝑥𝑦𝑅𝑦𝑥𝑥𝑦R(x,y)\land R(y,x)\Rightarrow x=y

. This is a sort of Univalence condition for R 𝑅 R ; if R 𝑅 R is Reflexive and A 𝐴 A is a H-Set, then R 𝑅 R is an Identity System on A 𝐴 A .

We can define this abstractly in an Allegory as R ∩ R † ≤ id 𝑅 superscript 𝑅 † id R\cap R^{\dagger}\leq\mathrm{id} .