Chuangjie Xu, 2012.

This is an Agda formalization Theorem 8.2 of the extended version
of Escardo's paper "Infinite sets that satisfy the principle of
omniscience in all varieties of constructive mathematics".

The theorem says that, for any p : ℕ∞ → ₂, the proposition
∀(n : ℕ) → p(under n) ≡ ₁ is decidable.

\begin{code}

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

open import CurryHoward
open import Equality
open import Naturals
open import Two
open import Cantor
open import GenericConvergentSequence
open import ConvergentSequenceSearchable
open import DecidableAndDetachable
open import SetsAndFunctions
open import DiscreteAndSeparated

Lemma-8·1 : ∀(p : ℕ∞ → ₂) →

(∃ \(x : ℕ∞) → x ≠ ∞ ∧ p x ≡ ₀)
∨ (∀(n : ℕ) → p (under n) ≡ ₁)

Lemma-8·1 p = ∨-elim claim₀ claim₁ claim₂
where
claim₀ : (∃ \(y : ℕ∞) → p y ≠ p (Succ y))
→ (∃ \(x : ℕ∞) → x ≠ ∞ ∧ p x ≡ ₀)
∨ (∀(n : ℕ) → p (under n) ≡ ₁)
claim₀ e = ∨-intro₀ (two-equality-cases case₀ case₁)
where
x : ℕ∞
x = ∃-witness e
ne : p x ≠ p (Succ x)
ne = ∃-elim e
case₀ : p x ≡ ₀ → ∃ \(x : ℕ∞) → x ≠ ∞ ∧ p x ≡ ₀
case₀ r = ∃-intro x (∧-intro s r)
where
s : x ≠ ∞
s t = ne (cong p (Lemma[x≡z→y≡z→x≡y]
t (trans (cong Succ t) Succ-∞-is-∞)))
case₁ : p x ≡ ₁ → ∃ \(x : ℕ∞) → x ≠ ∞ ∧ p x ≡ ₀
case₁ r = ∃-intro (Succ x) (∧-intro s s')
where
s : Succ x ≠ ∞
s t = ne (cong p (Lemma[x≡z→y≡z→x≡y]
(Succ-mono (Lemma[x≡z→y≡z→x≡y] t Succ-∞-is-∞)) t))
s' : p (Succ x) ≡ ₀
s' = Lemma[b≠₁→b≡₀] (λ t → ne (Lemma[x≡z→y≡z→x≡y] r t))

claim₁ : (∀(y : ℕ∞) → p y ≡ p (Succ y)) →
(∃ \(x : ℕ∞) → x ≠ ∞ ∧ p x ≡ ₀) ∨
(∀(n : ℕ) → p (under n) ≡ ₁)
claim₁ f = two-equality-cases case₀ case₁
where
case₀ : p Zero ≡ ₀ →
(∃ \(x : ℕ∞) → x ≠ ∞ ∧ p x ≡ ₀) ∨
(∀(n : ℕ) → p (under n) ≡ ₁)
case₀ r = ∨-intro₀(∃-intro Zero (∧-intro s r))
where
s : Zero ≠ ∞
s t = ∞-is-not-ℕ 0 (sym t)
case₁ : p Zero ≡ ₁ →
(∃ \(x : ℕ∞) → x ≠ ∞ ∧ p x ≡ ₀) ∨
(∀(n : ℕ) → p (under n) ≡ ₁)
case₁ r = ∨-intro₁ by-induction
where
by-induction : ∀(n : ℕ) → p (under n) ≡ ₁
by-induction 0 = r
by-induction (succ n) = trans (sym(f(under n))) (by-induction n)

claim₂ : (∃ \(y : ℕ∞) → p y ≠ p (Succ y)) ∨
(∀ (y : ℕ∞) → p y ≡ p (Succ y))
claim₂ = g(ℕ∞-is-omniscient q)
where
fact : ∀(y : ℕ∞) → p y ≠ p (Succ y) ∨ ¬(p y ≠ p (Succ y))
fact y = negation-preserves-decidability(₂-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 = ∃-witness f
g : (∃ \(y : ℕ∞) → q y ≡ ₀) ∨ (∀(y : ℕ∞) → q y ≡ ₁)
→ (∃ \(y : ℕ∞) → p y ≠ p (Succ y)) ∨ (∀(y : ℕ∞) → p y ≡ p (Succ y))
g(in₀(y , r)) = in₀(∃-intro y (∧-elim₀ (∃-elim f y) r))
g(in₁ h ) = in₁(λ y → discrete-is-separated
₂-discrete
(p y) (p (Succ y))
(∧-elim₁ (∃-elim f y) (h y)))

Theorem-8·2 : ∀(p : ℕ∞ → ₂) → decidable (∀(n : ℕ) → p(under n) ≡ ₁)
Theorem-8·2 p = ∨-elim claim₀ claim₁ (Lemma-8·1 p)
where
claim₀ : (∃ \(x : ℕ∞) → x ≠ ∞ ∧ p x ≡ ₀) →
decidable (∀(n : ℕ) → p(under n) ≡ ₁)
claim₀ e = ∨-intro₁ c₁
where
x : ℕ∞
x = ∃-witness e
c₀ : ¬(∀(n : ℕ) → x ≠ under n)
c₀ = λ g → ∧-elim₀(∃-elim e) (not-ℕ-is-∞ g)
c₁ : ¬(∀(n : ℕ) → p(under n) ≡ ₁)
c₁ g = c₀ d
where
d : ∀(n : ℕ) → x ≠ under n
d n r = Lemma[b≡₀→b≠₁] (∧-elim₁(∃-elim e)) (trans (cong p r) (g n))
claim₁ : (∀(n : ℕ) → p (under n) ≡ ₁) →
decidable (∀(n : ℕ) → p(under n) ≡ ₁)
claim₁ f = ∨-intro₀ f

\end{code}