Standard apartness relations

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

Created on 2022-09-09.
Last modified on 2024-05-23.

module foundation.standard-apartness-relations where
open import foundation.apartness-relations
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import
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


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


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


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 =
    ( 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


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:, doi:10.1007/978-1-4419-8640-5.

Recent changes