Negated equality

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-09.
Last modified on 2024-02-06.

module foundation.negated-equality where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.negation
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.identity-types
open import foundation-core.propositions

Idea

Two elements x and y are not equal whenever ¬ (x ＝ y) is inhabited.

Definition

nonequal : {l : Level} {A : UU l} → A → A → UU l
nonequal x y = ¬ (x ＝ y)

infix 6 _≠_
_≠_ = nonequal

Properties

Nonequality is a property

module _
  {l : Level} {A : UU l}
  where

  is-prop-nonequal : {x y : A} → is-prop (x ≠ y)
  is-prop-nonequal = is-prop-neg

  nonequal-Prop : (x y : A) → Prop l
  pr1 (nonequal-Prop x y) = x ≠ y
  pr2 (nonequal-Prop x y) = is-prop-nonequal

Nonequality is antireflexive

module _
  {l : Level} {A : UU l}
  where

  is-antireflexive-nonequal : (a : A) → ¬ (a ≠ a)
  is-antireflexive-nonequal a d = d refl

  is-consistent-nonequal : (a b : A) → (a ＝ b) → ¬ (a ≠ b)
  is-consistent-nonequal a b p d = d p

Nonequality is symmetric

module _
  {l : Level} {A : UU l}
  where

  is-symmetric-nonequal : is-symmetric (nonequal {A = A})
  is-symmetric-nonequal a b = map-neg inv

If two functions are nonequal at a point, they are nonequal as functions

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  nonequal-Π : (f g : (x : A) → B x) (a : A) → f a ≠ g a → f ≠ g
  nonequal-Π f g a = map-neg (λ h → htpy-eq h a)

If either component of two pairs are nonequal, the pairs are nonequal

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  nonequal-pr1 : (u v : Σ A B) → pr1 u ≠ pr1 v → u ≠ v
  nonequal-pr1 u v = map-neg (ap pr1)

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  nonequal-product-pr2 : (u v : A × B) → pr2 u ≠ pr2 v → u ≠ v
  nonequal-product-pr2 u v = map-neg (ap pr2)

If there is a reflexive relation that does not relate a and b, then they are nonequal

module _
  {l1 l2 : Level} {A : UU l1}
  where

  nonequal-reflexive-relation :
    (R : Relation l2 A) → is-reflexive R → (a b : A) → ¬ (R a b) → a ≠ b
  nonequal-reflexive-relation R is-refl-R a .a r refl = r (is-refl-R a)

If there is any family on A that is inhabited over one term but not the other, then they are nonequal

module _
  {l1 l2 : Level} {A : UU l1}
  where

  nonequal-leibniz : (B : A → UU l2) → (a b : A) → B a → ¬ (B b) → a ≠ b
  nonequal-leibniz B a .a a' b' refl = b' a'

  nonequal-leibniz' : (B : A → UU l2) → (a b : A) → ¬ (B a) → B b → a ≠ b
  nonequal-leibniz' B a .a a' b' refl = a' b'

See also

Recent changes