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


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


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

infix 6 _≠_
_≠_ = nonequal


Nonequality is a property

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

  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}

  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}

  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}

  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}

  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}

  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}

  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}

  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