Standard apartness relations
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-09-09.
Last modified on 2023-09-11.
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.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
Recent changes
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).