Decidable equality

module foundation.decidable-equality where
Imports
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.double-negation
open import foundation.negation
open import foundation.sections
open import foundation.unit-type

open import foundation-core.cartesian-product-types
open import foundation-core.dependent-pair-types
open import foundation-core.empty-types
open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.retractions
open import foundation-core.sets
open import foundation-core.type-arithmetic-dependent-pair-types
open import foundation-core.universe-levels

Definition

A type A is said to have decidable equality if Id x y is a decidable type for every x y : A.

has-decidable-equality : {l : Level} (A : UU l)  UU l
has-decidable-equality A = (x y : A)  is-decidable (x  y)

Examples

Any proposition has decidable equality

abstract
  has-decidable-equality-is-prop :
    {l1 : Level} {A : UU l1}  is-prop A  has-decidable-equality A
  has-decidable-equality-is-prop H x y = inl (eq-is-prop H)

The empty type has decidable equality

has-decidable-equality-empty : has-decidable-equality empty
has-decidable-equality-empty ()

The unit type has decidable equality

has-decidable-equality-unit :
  has-decidable-equality unit
has-decidable-equality-unit star star = inl refl

Properties

A product of types with decidable equality has decidable equality

has-decidable-equality-prod' :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  (f : B  has-decidable-equality A) (g : A  has-decidable-equality B) 
  has-decidable-equality (A × B)
has-decidable-equality-prod' f g (pair x y) (pair x' y') with
  f y x x' | g x y y'
... | inl refl | inl refl = inl refl
... | inl refl | inr nq = inr  r  nq (ap pr2 r))
... | inr np | inl refl = inr  r  np (ap pr1 r))
... | inr np | inr nq = inr  r  np (ap pr1 r))

has-decidable-equality-prod :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  has-decidable-equality A  has-decidable-equality B 
  has-decidable-equality (A × B)
has-decidable-equality-prod d e =
  has-decidable-equality-prod'  y  d)  x  e)

Decidability of equality of the factors of a cartesian product

If A × B has decidable equality and B has an element, then A has decidable equality; and vice versa.

has-decidable-equality-left-factor :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  has-decidable-equality (A × B)  B  has-decidable-equality A
has-decidable-equality-left-factor d b x y with d (pair x b) (pair y b)
... | inl p = inl (ap pr1 p)
... | inr np = inr  q  np (ap  z  pair z b) q))

has-decidable-equality-right-factor :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  has-decidable-equality (A × B)  A  has-decidable-equality B
has-decidable-equality-right-factor d a x y with d (pair a x) (pair a y)
... | inl p = inl (ap pr2 p)
... | inr np = inr  q  np (ap (pair a) q))

Types with decidable equality are closed under retracts

abstract
  has-decidable-equality-retract-of :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} 
    A retract-of B  has-decidable-equality B  has-decidable-equality A
  has-decidable-equality-retract-of (pair i (pair r H)) d x y =
    is-decidable-retract-of
      ( retract-eq (pair i (pair r H)) x y)
      ( d (i x) (i y))

Types with decidable equality are closed under equivalences

abstract
  has-decidable-equality-equiv :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B) 
    has-decidable-equality B  has-decidable-equality A
  has-decidable-equality-equiv e dB x y =
    is-decidable-equiv (equiv-ap e x y) (dB (map-equiv e x) (map-equiv e y))

abstract
  has-decidable-equality-equiv' :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B) 
    has-decidable-equality A  has-decidable-equality B
  has-decidable-equality-equiv' e = has-decidable-equality-equiv (inv-equiv e)

Hedberg's theorem

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

  Eq-has-decidable-equality' :
    (x y : A)  is-decidable (x  y)  UU lzero
  Eq-has-decidable-equality' x y (inl p) = unit
  Eq-has-decidable-equality' x y (inr f) = empty

  Eq-has-decidable-equality :
    (d : has-decidable-equality A)  A  A  UU lzero
  Eq-has-decidable-equality d x y = Eq-has-decidable-equality' x y (d x y)

  abstract
    is-prop-Eq-has-decidable-equality' :
      (x y : A) (t : is-decidable (x  y)) 
      is-prop (Eq-has-decidable-equality' x y t)
    is-prop-Eq-has-decidable-equality' x y (inl p) = is-prop-unit
    is-prop-Eq-has-decidable-equality' x y (inr f) = is-prop-empty

  abstract
    is-prop-Eq-has-decidable-equality :
      (d : has-decidable-equality A)
      {x y : A}  is-prop (Eq-has-decidable-equality d x y)
    is-prop-Eq-has-decidable-equality d {x} {y} =
      is-prop-Eq-has-decidable-equality' x y (d x y)

  abstract
    refl-Eq-has-decidable-equality :
      (d : has-decidable-equality A) (x : A) 
      Eq-has-decidable-equality d x x
    refl-Eq-has-decidable-equality d x with d x x
    ... | inl α = star
    ... | inr f = f refl

  abstract
    Eq-has-decidable-equality-eq :
      (d : has-decidable-equality A) {x y : A} 
      x  y  Eq-has-decidable-equality d x y
    Eq-has-decidable-equality-eq d {x} {.x} refl =
      refl-Eq-has-decidable-equality d x

  abstract
    eq-Eq-has-decidable-equality' :
      (x y : A) (t : is-decidable (x  y)) 
      Eq-has-decidable-equality' x y t  x  y
    eq-Eq-has-decidable-equality' x y (inl p) t = p
    eq-Eq-has-decidable-equality' x y (inr f) t = ex-falso t

  abstract
    eq-Eq-has-decidable-equality :
      (d : has-decidable-equality A) {x y : A} 
      Eq-has-decidable-equality d x y  x  y
    eq-Eq-has-decidable-equality d {x} {y} =
      eq-Eq-has-decidable-equality' x y (d x y)

  abstract
    is-set-has-decidable-equality : has-decidable-equality A  is-set A
    is-set-has-decidable-equality d =
      is-set-prop-in-id
        ( λ x y  Eq-has-decidable-equality d x y)
        ( λ x y  is-prop-Eq-has-decidable-equality d)
        ( λ x  refl-Eq-has-decidable-equality d x)
        ( λ x y  eq-Eq-has-decidable-equality d)

Having decidable equality is a property

abstract
  is-prop-has-decidable-equality :
    {l1 : Level} {X : UU l1}  is-prop (has-decidable-equality X)
  is-prop-has-decidable-equality {l1} {X} =
    is-prop-is-inhabited
      ( λ d 
        is-prop-Π
        ( λ x 
          is-prop-Π
          ( λ y 
            is-prop-coprod
            ( intro-double-negation)
            ( is-set-has-decidable-equality d x y)
            ( is-prop-neg))))

has-decidable-equality-Prop :
  {l1 : Level} (X : UU l1)  Prop l1
pr1 (has-decidable-equality-Prop X) = has-decidable-equality X
pr2 (has-decidable-equality-Prop X) = is-prop-has-decidable-equality

Types with decidable equality are closed under dependent pair types

abstract
  has-decidable-equality-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    has-decidable-equality A  ((x : A)  has-decidable-equality (B x)) 
    has-decidable-equality (Σ A B)
  has-decidable-equality-Σ dA dB (pair x y) (pair x' y') with dA x x'
  ... | inr np = inr  r  np (ap pr1 r))
  ... | inl p =
    is-decidable-iff eq-pair-Σ' pair-eq-Σ
      ( is-decidable-equiv
        ( left-unit-law-Σ-is-contr
          ( is-proof-irrelevant-is-prop
            ( is-set-has-decidable-equality dA x x') p)
          ( p))
        ( dB x' (tr _ p y) y'))

A family of types over a type with decidable equality and decidable total space is a family of types with decidable equality

abstract
  has-decidable-equality-fiber-has-decidable-equality-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    has-decidable-equality A  has-decidable-equality (Σ A B) 
    (x : A)  has-decidable-equality (B x)
  has-decidable-equality-fiber-has-decidable-equality-Σ {B = B} dA  x =
    has-decidable-equality-equiv'
      ( equiv-fib-pr1 B x)
      ( has-decidable-equality-Σ 
        ( λ t 
          has-decidable-equality-is-prop
            ( is-set-has-decidable-equality dA (pr1 t) x)))

If B is a family of types with decidable equality, the total space has decidable equality, and B has a section, then the base type has decidable equality

abstract
  has-decidable-equality-base-has-decidable-equality-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (b : (x : A)  B x) 
    has-decidable-equality (Σ A B)  ((x : A)  has-decidable-equality (B x)) 
    has-decidable-equality A
  has-decidable-equality-base-has-decidable-equality-Σ b  dB =
    has-decidable-equality-equiv'
      ( equiv-total-fib (map-section b))
      ( has-decidable-equality-Σ 
        ( λ t 
          has-decidable-equality-is-prop
            ( is-prop-map-is-injective
              ( is-set-has-decidable-equality )
              ( is-injective-map-section b)
              ( t))))

If A and B have decidable equality, then so does their coproduct

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

  has-decidable-equality-coprod :
    has-decidable-equality A  has-decidable-equality B 
    has-decidable-equality (A + B)
  has-decidable-equality-coprod d e (inl x) (inl y) =
    is-decidable-iff (ap inl) is-injective-inl (d x y)
  has-decidable-equality-coprod d e (inl x) (inr y) =
    inr neq-inl-inr
  has-decidable-equality-coprod d e (inr x) (inl y) =
    inr neq-inr-inl
  has-decidable-equality-coprod d e (inr x) (inr y) =
    is-decidable-iff (ap inr) is-injective-inr (e x y)

  has-decidable-equality-left-summand :
    has-decidable-equality (A + B)  has-decidable-equality A
  has-decidable-equality-left-summand d x y =
    is-decidable-iff is-injective-inl (ap inl) (d (inl x) (inl y))

  has-decidable-equality-right-summand :
    has-decidable-equality (A + B)  has-decidable-equality B
  has-decidable-equality-right-summand d x y =
    is-decidable-iff is-injective-inr (ap inr) (d (inr x) (inr y))