*** This is obsolete and kept for historical reasons only.
You are being redirected to http://www.cs.bham.ac.uk/~mhe/agda-new/index.html ***

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, 2010--2017.

This is the original version, which will not be further
updated. Type checks in Agda 2.6.0. The new version, still evolving
is available at http://www.cs.bham.ac.uk/~mhe/agda-new/index.html

\begin{code}

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

module index where

\end{code}

You can navigate this set of files by clicking at words or
symbols to get to their definitions.

The module dependency graph: http://www.cs.bham.ac.uk/~mhe/agda/index.ps

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}

\end{code}

This is used to show that the non-continuity of a function ℕ∞ → ℕ is
decidable:

\begin{code}

open import DecidabilityOfNonContinuity

\end{code}

Given countably many searchable sets, one can take the disjoint sum
with a limit point at infinity, and this is again a searchable
sets. This construction is called the squashed sum of the countable
family searchable sets. It can be transfinitely iterated to produce
increasingly complex searchable ordinals.

\begin{code}

open import SquashedSumOld
open import SearchableOrdinals
open import LexicographicSearch
open import ConvergentSequenceInfSearchable

\end{code}

There is a better definition of squashed sum discussed below.

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}

There is a better way of proving that the universe is indiscrete,
discussed below, but implemented in Agda yet.

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 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 shows that the universe is injective:

\begin{code}

open import InjectivityOfTheUniverse

\end{code}

This uses properties of hprop-indexed products, first that it is
isomorphic to any of its factors:

\begin{code}

open import HProp-indexed-product

\end{code}

And, more subtly, that an hprop-indexed product of searchable sets is
itself searchable:

\begin{code}

open import HProp-Tychonoff

\end{code}

The following generalizes the squashed sum, with a simple construction
and proof, using the injectivity of the universe and the
HProp-Tychonoff theorem:

\begin{code}

open import ExtendedSumSearchable

\end{code}

Here we show that the squashed sum is indeed a particular case of the
extended sum:

\begin{code}

open import SquashedSum
open import SquashedAgreement

\end{code}

The following modules contain auxiliary definitions and additional
results and discussion that we choose not to bring 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 FailureOfTotalSeparatednessBis
open import FirstProjectionInjective
open import HSets
open import Injection
open import Isomorphism
open import IsomorphismOld
open import Naturals
open import Ordinals
open import Sequence
open import SetsAndFunctions
open import Retraction
open import Two
open import Embedding
open import Injectivity -- Deliberate clone of InjectivityOfTheUniverse.
open import TheTopologyOfTheUniverseOld -- For the record.
open import HiggsInvolutionTheorem

\end{code}