# Standard apartness relations

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-09-09.

module foundation.standard-apartness-relations where

Imports
open import foundation.apartness-relations
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.law-of-excluded-middle
open import foundation.logical-equivalences
open import foundation.negated-equality
open import foundation.tight-apartness-relations
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.negation


## Idea

An apartness relation # is said to be standard if the law of excluded middle implies that # is equivalent to negated equality.

## Definition

is-standard-Apartness-Relation :
{l1 l2 : Level} (l3 : Level) {A : UU l1} (R : Apartness-Relation l2 A) →
UU (l1 ⊔ l2 ⊔ lsuc l3)
is-standard-Apartness-Relation {l1} {l2} l3 {A} R =
LEM l3 → (x y : A) → (x ≠ y) ↔ apart-Apartness-Relation R x y


## Properties

### Any tight apartness relation is standard

is-standard-is-tight-Apartness-Relation :
{l1 l2 : Level} {A : UU l1} (R : Apartness-Relation l2 A) →
is-tight-Apartness-Relation R → is-standard-Apartness-Relation l2 R
pr1 (is-standard-is-tight-Apartness-Relation R H lem x y) np =
double-negation-elim-is-decidable
( lem (rel-Apartness-Relation R x y))
( map-neg (H x y) np)
pr2 (is-standard-is-tight-Apartness-Relation R H lem x .x) r refl =
antirefl-Apartness-Relation R x r


## References

[MRR88]
Ray Mines, Fred Richman, and Wim Ruitenburg. A Course in Constructive Algebra. Universitext. Springer New York, 1988. ISBN 978-0-387-96640-3 978-1-4419-8640-5. URL: http://link.springer.com/10.1007/978-1-4419-8640-5, doi:10.1007/978-1-4419-8640-5.