F o r m a l i z a t i o n i n A g d a o f v a r i o u s n e w t h e o r e m s i n c o n s t r u c t i v e m a t h e m a t i c s. Martin Escardo, 2012, version of 22 Feb 2012. \begin{code} module index where \end{code} Some people formalize proofs to get reassurance. Here I instead formalize my proofs so that I can run them: proofs really are programs, in a very concrete sense. I unavoidably get reassurance too, but this is not what motivated me to write the formal versions of the proofs. You can navigate this set of files by clicking at words or symbols to get to their definitions. The following module investigates the notion of omniscience set. A set X is omniscient iff ∀(p : X → ₂) → (∃ \(x : X) → p x ≡ ₀) ∨ (∀(x : X) → p x ≡ ₁) \begin{code} open import Omniscience \end{code} The omniscience of ℕ is a taboo, known as LPO. See also: \begin{code} open import WLPO \end{code} An example of an omniscient set is ℕ∞, which intuitively is ℕ ∪ { ∞ }, defined in the following module: \begin{code} open import GenericConvergentSequence \end{code} But it is more direct to show that ℕ∞ is searchable, and get omniscience as a corollary: \begin{code} open import Searchable open import ConvergentSequenceSearchable \end{code} An interesting consequence of the omniscience of ℕ∞ is that the following property, an instance of WLPO, holds constructively: ∀(p : ℕ∞ → ₂) → (∀(n : ℕ) → p(under n) ≡ ₁) ∨ ¬(∀(n : ℕ) → p(under n) ≡ ₁). \begin{code} open import ADecidableQuantificationOverTheNaturals \end{code} As a side remark, the following module characterizes ℕ∞ as the final coalgebra of the functor 1+(-), and is followed by an illustrative example: \begin{code} open import CoNaturals open import CoNaturalsExercise \end{code} The following module discusses in what sense ℕ∞ is the generic convergent sequence, and proves that the universe Set is indiscrete, with a certain Rice's Theorem for the universe Set as a corollary: \begin{code} open import TheTopologyOfTheUniverse open import RicesTheoremForTheUniverse \end{code} The following two rogue modules depart from our main philosophy of working strictly within ML type theory with the propositional axiom of extensionality. They disable the termination checker, for the reasons explained in the first module. But to make our point, we also include runnable experiments in the second module: \begin{code} open import CountableTychonoff open import CantorSearchable \end{code} The following modules return to the well-behavedness paradigm. The first one shows that a basic form of discontinuity is a taboo. This, in fact, is used to formulate and prove Rice's Theorem mentioned above: \begin{code} open import BasicDiscontinuityTaboo \end{code} The following modules contain auxiliary definitions and additional results and discussion that we choose not to discuss here: \begin{code} open import Cantor open import CurryHoward open import DecidableAndDetachable open import DiscreteAndSeparated open import Equality open import Exhaustible open import Extensionality open import FailureOfTotalSeparatedness open import FirstProjectionInjective open import Image open import Injection open import Isomorphism open import Naturals open import Sequence open import SetsAndFunctions open import Singleton open import Singular open import Surjection open import Two open import UIP \end{code}