Tom de Jong, 1 November 2021.

We show that π classifies decidable subsets.

We start by defining the type Ξ©α΅ π€ of decidable propositions in a type
universe π€ and we show that π β Ξ©α΅ π€ (for any universe π€).

\begin{code}

{-# OPTIONS --safe --without-K #-}

module NotionsOfDecidability.DecidableClassifier where

open import MLTT.Spartan

open import MLTT.Plus-Properties
open import MLTT.Two-Properties
open import UF.Subsingletons
open import UF.SubtypeClassifier

open import NotionsOfDecidability.Decidable
open import NotionsOfDecidability.Complemented

boolean-value' : {A : π€ Μ }
β is-decidable A
β Ξ£ b κ π , (b οΌ β β Β¬ A)
Γ (b οΌ β β   A)
boolean-value' {π€} {A} (inl a ) = (β , Ο , Ο)
where
Ο : β οΌ β β Β¬ A
Ο = (Ξ» p β π-elim (one-is-not-zero p))
, (Ξ» na β π-elim (na a))
Ο : β οΌ β β A
Ο = (Ξ» _ β a) , (Ξ» _ β refl)
boolean-value' {π€} {A} (inr na) = β , Ο , Ο
where
Ο : β οΌ β β Β¬ A
Ο = (Ξ» _ β na) , (Ξ» _ β refl)
Ο : β οΌ β β A
Ο = (Ξ» p β π-elim (zero-is-not-one p))
, (Ξ» a β π-elim (na a))

private
Ξ©α΅ : (π€ : Universe) β π€ βΊ Μ
Ξ©α΅ π€ = Ξ£ P κ Ξ© π€ , is-decidable (P holds)

β¨ (P , i) , Ξ΄ β© = P

open import UF.Equiv
open import UF.Subsingletons-FunExt
open import UF.FunExt
open import UF.Lower-FunExt

module _
{π€ : Universe}
(fe : funext π€ π€)
(pe : propext π€)
where

β P οΌ Q
to-Ξ©α΅-equality ((P , i) , Ξ΄) ((Q , j) , Ξ΅) Ξ± Ξ² =
to-subtype-οΌ Ο (to-subtype-οΌ Ο (pe i j Ξ± Ξ²))
where
Ο : (P : Ξ© π€) β is-prop (is-decidable (P holds))
Ο P = decidability-of-prop-is-prop (lower-funext π€ π€ fe) (holds-is-prop P)
Ο : (X : π€ Μ )β is-prop (is-prop X)
Ο _ = being-prop-is-prop fe

π-is-the-type-of-decidable-propositions : π β Ξ©α΅ π€
π-is-the-type-of-decidable-propositions = qinveq f (g , Ξ· , Ξ΅)
where
f : π β Ξ©α΅ π€
f β = ((π , π-is-prop) , inr π-elim)
f β = ((π , π-is-prop) , inl β)
g : Ξ©α΅ π€ β π
g (P , Ξ΄) = prβ (boolean-value' Ξ΄)
Ξ· : g β f βΌ id
Ξ· β = refl
Ξ· β = refl
Ξ΅ : f β g βΌ id
Ξ΅ P = π-equality-cases Ξ΅β Ξ΅β
where
lemma : (g P οΌ β β Β¬ β¨ P β©)
Γ (g P οΌ β β   β¨ P β©)
lemma = prβ (boolean-value' (prβ P))
Ξ΅β : g P οΌ β
β (f β g) P οΌ P
Ξ΅β e = to-Ξ©α΅-equality (f (g P)) P
(Ξ» (q : β¨ f (g P) β©) β π-elim (transport (Ξ» b β β¨ f b β©) e q))
(Ξ» (p : β¨ P β©) β π-elim (lr-implication (prβ lemma) e p))
Ξ΅β : g P οΌ β
β (f β g) P οΌ P
Ξ΅β e = to-Ξ©α΅-equality (f (g P)) P
(Ξ» _ β lr-implication (prβ lemma) e)
(Ξ» _ β transportβ»ΒΉ (Ξ» (b : π) β β¨ f b β©) e β)

\end{code}

The promised result now follows promptly using two general lemmas on
equivalences.

(Note that one direction of the equivalence Ξ Ξ£-distr-β is sometimes known as
"type-theoretic axiom of choice".)

\begin{code}

open import UF.Powerset
open import UF.EquivalenceExamples

is-complemented-subset : {X : π€ Μ } β (X β Ξ© π£) β π€ β π£ Μ
is-complemented-subset {π€} {π£} {X} A = (x : X) β is-decidable (x β A)

module _
(fe  : funext π€ (π£ βΊ))
(fe' : funext π£ π£)
(pe : propext π£)
where

π-classifies-decidable-subsets : {X : π€ Μ }
β (X β π)
β (Ξ£ A κ (X β Ξ© π£) , is-complemented-subset A)
π-classifies-decidable-subsets {X} =
(X β π)                                      ββ¨ Ξ³          β©
(Ξ£ A κ (X β Ξ© π£) , is-complemented-subset A) β
where
Ξ³ = βcong' fe (lower-funext π€ (π£ βΊ) fe)
(π-is-the-type-of-decidable-propositions fe' pe)

π-classifies-decidable-subsets-values :
{X : π€ Μ }
(A : X β Ξ© π£)
(Ξ΄ : is-complemented-subset A)
(x : X)
β ((β π-classifies-decidable-subsets ββ»ΒΉ (A , Ξ΄) x οΌ β) β Β¬ (x β A))
Γ ((β π-classifies-decidable-subsets ββ»ΒΉ (A , Ξ΄) x οΌ β) β   (x β A))
π-classifies-decidable-subsets-values {X} A Ξ΄ x = Ξ³
where
Ο : (Ξ£ A κ (X β Ξ© π£) , is-complemented-subset A) β (X β π)
Ο = β π-classifies-decidable-subsets ββ»ΒΉ
Ξ³ : (Ο (A , Ξ΄) x οΌ β β Β¬ (x β A))
Γ (Ο (A , Ξ΄) x οΌ β β   (x β A))
Ξ³ = prβ (boolean-value' (Ξ΄ x))

\end{code}

Added by Tom de Jong, November 2021.

\begin{code}

decidable-β : {X : π€ Μ } {Y : π₯ Μ }
β X β Y
β is-decidable X
β is-decidable Y
decidable-β {π€} {π₯} {X} {Y} (f , g) (inl  x) = inl (f x)
decidable-β {π€} {π₯} {X} {Y} (f , g) (inr nx) = inr (nx β g)

decidable-cong : {X : π€ Μ } {Y : π₯ Μ }
β X β Y
β is-decidable X
β is-decidable Y
decidable-cong e = decidable-β (β e β , β e ββ»ΒΉ)

\end{code}

Added by Tom de Jong in January 2022.

\begin{code}

all-types-are-Β¬Β¬-decidable : (X : π€ Μ ) β Β¬Β¬ (is-decidable X)
all-types-are-Β¬Β¬-decidable X h = claimβ claimβ
where
claimβ : Β¬ X
claimβ x = h (inl x)
claimβ : Β¬Β¬ X
claimβ nx = h (inr nx)

Β¬Β¬-stable-if-decidable : (X : π€ Μ ) β is-decidable X β Β¬Β¬-stable X
Β¬Β¬-stable-if-decidable X (inl  x) = Ξ» _ β x
Β¬Β¬-stable-if-decidable X (inr nx) = Ξ» h β π-elim (h nx)

\end{code}