-- By Martin Escardo, 2 September 2011.
-- (Rewritten December 2011 to define ℕ∞ as a type.)
--
-- 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-new.zip

module AnInfiniteOmniscientSet where

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


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

       u : ℕ∞
       u = ∃-witness e

       case₀ : p u ≡ ₀ →   (∃ \(u : ℕ∞) → p u ≡ ₀)
                        ∨  (∀  (u : ℕ∞) → p u ≡ ₁)
       case₀ r = ∨-intro₀(∃-intro u r)

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