# Decidable equality

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

Created on 2022-01-27.

module foundation.decidable-equality where

Imports
open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.double-negation
open import foundation.injective-maps
open import foundation.negation
open import foundation.sections
open import foundation.sets
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.cartesian-product-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.propositions
open import foundation-core.retracts-of-types
open import foundation-core.transport-along-identifications


## Definition

A type A is said to have decidable equality if 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-product' :
{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-product' 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-product :
{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-product d e =
has-decidable-equality-product' (λ 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 (eq-pair-eq-fiber 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

Hedberg's theorem asserts that types with decidable equality are sets.

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-has-element
( λ d →
is-prop-Π
( λ x →
is-prop-Π
( λ y →
is-prop-coproduct
( 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 dΣ x =
has-decidable-equality-equiv'
( equiv-fiber-pr1 B x)
( has-decidable-equality-Σ dΣ
( λ 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 dΣ dB =
has-decidable-equality-equiv'
( equiv-total-fiber (map-section-family b))
( has-decidable-equality-Σ dΣ
( λ t →
has-decidable-equality-is-prop
( is-prop-map-is-injective
( is-set-has-decidable-equality dΣ)
( is-injective-map-section-family 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-coproduct :
has-decidable-equality A → has-decidable-equality B →
has-decidable-equality (A + B)
has-decidable-equality-coproduct d e (inl x) (inl y) =
is-decidable-iff (ap inl) is-injective-inl (d x y)
has-decidable-equality-coproduct d e (inl x) (inr y) =
inr neq-inl-inr
has-decidable-equality-coproduct d e (inr x) (inl y) =
inr neq-inr-inl
has-decidable-equality-coproduct 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))