Chuangjie Xu, 2012.

This is an Agda formalization of Theorem 8.2 of the extended version
of [1].

The theorem says that, for any p : ββ β π, the proposition
(n : β) β p (ΞΉ n) οΌ β is decidable where ΞΉ : β β β is the inclusion.

[1] Martin Escardo. Infinite sets that satisfy the principle of
omniscience in all varieties of constructive mathematics, Journal
of Symbolic Logic, volume 78, number 3, September 2013, pages
764-784.

https://doi.org/10.2178/jsl.7803040

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt

module TypeTopology.ADecidableQuantificationOverTheNaturals (fe : funext π€β π€β) where

open import CoNaturals.Type
open import MLTT.Two-Properties
open import Notation.CanonicalMap
open import NotionsOfDecidability.Complemented
open import NotionsOfDecidability.Decidable
open import TypeTopology.GenericConvergentSequenceCompactness fe
open import UF.DiscreteAndSeparated

Lemma-8Β·1 : (p : ββ β π) β (Ξ£ x κ ββ , (x β  β) Γ (p x οΌ β))
+ ((n : β) β p (ΞΉ n) οΌ β)
Lemma-8Β·1 p = cases claimβ claimβ claimβ
where
claimβ : (Ξ£ y κ ββ , p y β  p (Succ y))
β (Ξ£ x κ ββ , (x β  β) Γ (p x οΌ β)) + ((n : β) β p (ΞΉ n) οΌ β)
claimβ e = inl (π-equality-cases caseβ caseβ)
where
x : ββ
x = prβ e

ne : p x β  p (Succ x)
ne = prβ e

caseβ : p x οΌ β β Ξ£ x κ ββ , (x β  β) Γ (p x οΌ β)
caseβ r = x , (s , r)
where
s : x β  β
s t = ne (ap p (t β (Succ-β-is-β fe)β»ΒΉ β (ap Succ t)β»ΒΉ))

caseβ : p x οΌ β β Ξ£ x κ ββ , (x β  β) Γ (p x οΌ β)
caseβ r = (Succ x) , (s , s')
where
s : Succ x β  β
s t = ne (ap p (Succ-lc (t β (Succ-β-is-β fe)β»ΒΉ) β t β»ΒΉ))

s' : p (Succ x) οΌ β
s' = different-from-β-equal-β (Ξ» t β ne (r β t β»ΒΉ))

claimβ : ((y : ββ) β p y οΌ p (Succ y)) β
(Ξ£ x κ ββ , (x β  β) Γ (p x οΌ β)) + ((n : β) β p (ΞΉ n) οΌ β)
claimβ f = π-equality-cases caseβ caseβ
where
caseβ : p Zero οΌ β β
(Ξ£ x κ ββ , (x β  β) Γ (p x οΌ β)) + ((n : β) β p (ΞΉ n) οΌ β)
caseβ r = inl (Zero , (s , r))
where
s : Zero β  β
s t = β-is-not-finite 0 (t β»ΒΉ)

caseβ : p Zero οΌ β β
(Ξ£ x κ ββ , (x β  β) Γ (p x οΌ β)) + ((n : β) β p (ΞΉ n) οΌ β)
caseβ r = inr by-induction
where
by-induction : (n : β) β p (ΞΉ n) οΌ β
by-induction 0 = r
by-induction (succ n) = (f (ΞΉ n))β»ΒΉ β by-induction n

claimβ : (Ξ£ y κ ββ , p y β  p (Succ y)) + ((y : ββ) β p y οΌ p (Succ y))
claimβ = g (ββ-compact q)
where
fact : (y : ββ) β (p y β  p (Succ y)) + Β¬ (p y β  p (Succ y))
fact y = Β¬-preserves-decidability (π-is-discrete (p y) (p (Succ y)))

f : Ξ£ q κ (ββ β π), ((y : ββ) β (q y οΌ β β p y β  p (Succ y))
Γ (q y οΌ β β Β¬ (p y β  p (Succ y))))
f = characteristic-function fact

q : ββ β π
q = prβ f

g : (Ξ£ y κ ββ , q y οΌ β) + ((y : ββ) β q y οΌ β)
β (Ξ£ y κ ββ , p y β  p (Succ y)) + ((y : ββ) β p y οΌ p (Succ y))
g (inl (y , r)) = inl (y , (prβ (prβ f y) r))
g (inr h ) = inr (Ξ» y β discrete-is-Β¬Β¬-separated
π-is-discrete
(p y) (p (Succ y))
(prβ (prβ f y) (h y)))

\end{code}

TODO. The name of the following fact is that of the reference [1]
above. It deserves a better name, or at least a better synonym.

\begin{code}

abstract
Theorem-8Β·2 : (p : ββ β π) β is-decidable ((n : β) β p (ΞΉ n) οΌ β)
Theorem-8Β·2 p = cases claimβ claimβ (Lemma-8Β·1 p)
where
claimβ : (Ξ£ x κ ββ , (x β  β) Γ (p x οΌ β))
β is-decidable ((n : β) β p (ΞΉ n) οΌ β)
claimβ e = inr cβ
where
x : ββ
x = prβ e

cβ : Β¬ ((n : β) β x β  ΞΉ n)
cβ = Ξ» g β prβ (prβ e) (not-finite-is-β fe g)

cβ : Β¬ ((n : β) β p (ΞΉ n) οΌ β)
cβ g = cβ d
where
d : (n : β) β x β  ΞΉ n
d n r = equal-β-different-from-β (prβ (prβ e)) (ap p r β g n)

claimβ : ((n : β) β p (ΞΉ n) οΌ β) β is-decidable ((n : β) β p (ΞΉ n) οΌ β)
claimβ f = inl f

\end{code}

Some examples:

\begin{code}

module examples where

to-β : {A : π€ Μ } β is-decidable A β β
to-β (inl _) = 0
to-β (inr _) = 1

\end{code}

0 means that (n : β) β p (ΞΉ n) οΌ β
1 means that Β¬ ((n : β) β p (ΞΉ n) οΌ β)

\begin{code}

eval : (ββ β π) β β
eval p = to-β (Theorem-8Β·2 p)

pβ : ββ β π
pβ _ = β

pβ : ββ β π
pβ _ = β

\end{code}

If the first boolean is less than or equal to the second
then it has value β; otherwise, it has value β.

\begin{code}

_<=_ : π β π β π
β <= y = β
β <= β = β
β <= β = β

\end{code}

If the two booleans are equal then it has value β;
otherwise, it has value β.

\begin{code}

_==_ : π β π β π
β == β = β
β == β = β
β == β = β
β == β = β

pβ : ββ β π
pβ (Ξ± , _) = Ξ± 10 <= Ξ± 1

pβ : ββ β π
pβ (Ξ± , _) = Ξ± 0 <= Ξ± 1

pβ : ββ β π
pβ (Ξ± , _) = Ξ± 5 == Ξ± 100

to-something : (p : ββ β π)
β is-decidable ((n : β) β p (ΞΉ n) οΌ β) β (p (ΞΉ 17) οΌ β) + β
to-something p (inl f) = inl (f 17)
to-something p (inr _) = inr 1070

eval1 : (p : ββ β π) β (p (ΞΉ 17) οΌ β) + β
eval1 p = to-something p (Theorem-8Β·2 p)

\end{code}

Despite the fact that we use function extensionality, eval pi
evaluates to a numeral for i=0,...,4.

Added by Martin Escardo 5th September 2024. The following version is
more convenient in practice.

\begin{code}

abstract
Theorem-8Β·2' : (A : ββ β π€ Μ )
β is-complemented A
β is-decidable ((n : β) β A (ΞΉ n))
Theorem-8Β·2' {π€} A Ξ΄ = IV
where
p : ββ β π
p = complement β characteristic-map A Ξ΄

I : is-decidable ((n : β) β p (ΞΉ n) οΌ β)
I = Theorem-8Β·2 p

II : ((n : β) β p (ΞΉ n) οΌ β) β (n : β) β A (ΞΉ n)
II b n = characteristic-map-propertyβ A Ξ΄ (ΞΉ n) (complementβ (b n))

III : ((n : β) β A (ΞΉ n)) β (n : β) β p (ΞΉ n) οΌ β
III a n = complementβ-back (characteristic-map-propertyβ-back A Ξ΄ (ΞΉ n) (a n))

IV : is-decidable ((n : β) β A (ΞΉ n))
IV = map-decidable II III I

\end{code}