```module AnInfiniteOmniscientSet where

-- By Martin Escardo, 2 September 2011.
--
-- This is a formal constructive proof in the sense of ML type theory,
-- written in Agda notation.
--
-- It is based on the author's paper
--
---------------------------------------------------------------
--      Infinite sets that satisfy the principle of omniscience
--      in all varieties of constructive mathematics
---------------------------------------------------------------
--
--      http://www.cs.bham.ac.uk/~mhe/papers/omniscient.pdf
--
--
-- to be presented at the Types'2011 meeting in Bergen, Norway,
-- September 8-11,
--
-- Theorem-3·6 of that paper is proved in the module
-- DrinkerParadox. This module derives the main corollary, the fact
-- that the infinite set ℕ∞, defined in the module
-- GenericConvergentSequence, satisfies the principle of omniscience.
--
----------------------------------------------------------------------
-- You can click at any word or symbol to navigate to the module that
-- defines it in the html rendering of this set of agda modules.
----------------------------------------------------------------------
--
-- The agda files are collected together at
--
--      http://www.cs.bham.ac.uk/~mhe/papers/omniscient.zip

open import Logic
open import Equality
open import Naturals
open import Two
open import Cantor
open import GenericConvergentSequence

Theorem[ℕ∞-is-omniscient] :
------------------------------------
∀(p : ₂ℕ → ₂) → extensional p →
(∃ \(x : ₂ℕ) → x ∈ ℕ∞ ∧ p x ≡ ₀)
∨(∀  (x : ₂ℕ) → x ∈ ℕ∞ → p x ≡ ₁)
------------------------------------
Theorem[ℕ∞-is-omniscient] p extensionality-of-p =
two-equality-cases case₀ case₁
where e : ∃ \(x : ₂ℕ) → x ∈ ℕ∞ ∧
(p x ≡ ₁ → ∀(y : ₂ℕ) → y ∈ ℕ∞ → p y ≡ ₁)
e = Theorem-3·6 p extensionality-of-p

x : ₂ℕ
x = ∃-witness e

m : x ∈ ℕ∞
m = ∧-elim₀(∃-elim e)

case₀ : p x ≡ ₀ → (∃ \(x : ₂ℕ) → x ∈ ℕ∞ ∧ p x ≡ ₀)
∨  (∀  (x : ₂ℕ) → x ∈ ℕ∞ → p x ≡ ₁)
case₀ r = ∨-intro₀(∃-intro x (∧-intro m r))

case₁ : p x ≡ ₁ → (∃ \(x : ₂ℕ) → x ∈ ℕ∞ ∧ p x ≡ ₀)
∨  (∀  (x : ₂ℕ) → x ∈ ℕ∞ → p x ≡ ₁)
case₁ r = ∨-intro₁(∧-elim₁(∃-elim e) r)

```