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--
   Continuously evolving.

   September 2017. This version removes CurryHoward.lagda, so that we
   use the symbols Σ and + rather than ∃ and ∨. This is to be
   compatible with univalent logic. We also make our development more
   compatible with the philosophy of univalent mathematics and tried
   to streamline it a bit. The original version remains at
   http://www.cs.bham.ac.uk/~mhe/agda/ for the record and to avoid
   broken incoming links.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

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-new/manual.pdf

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 (and under
classical logic) 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) ≡ ₁).

where

  under : ℕ → ℕ∞

is the embedding. (The name for the embedding comes from the fact that
in published papers we used an underlined symbol n to denote the copy
of n : ℕ in ℕ∞.)

\begin{code}

open import ADecidableQuantificationOverTheNaturals

\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 SquashedSum
open import SearchableOrdinals
open import LexicographicSearch
open import ConvergentSequenceInfSearchable

\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 U of types is
indiscrete, with a certain Rice's Theorem for the universe U 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 shows that the universe is injective:

\begin{code}

open import InjectivityOfTheUniverse

\end{code}

This uses properties of products indexed by univalent propositions,
first that it is isomorphic to any of its factors:

\begin{code}

open import Prop-indexed-product

\end{code}

And, more subtly, that a product of searchable sets indexed by a
univalent proposition is itself searchable:

\begin{code}

open import Prop-Tychonoff

\end{code}

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

\begin{code}

open import ExtendedSumSearchable

\end{code}

The following modules contain auxiliary definitions and additional
results and discussion that we choose not to bring here:

\begin{code}

open import SpartanMLTT 
open import DecidableAndDetachable 
open import DiscreteAndSeparated 
open import Exhaustible 
open import FailureOfTotalSeparatedness 
open import FirstProjectionInjective 
open import Sets
open import Injection 
open import Equivalence
open import Naturals 
open import OrdinalCodes
open import Sequence 
open import Retraction
open import Two 
open import Embedding
open import InjectivityOfTheUniverse
open import HiggsInvolutionTheorem

\end{code}