Martin Escardo, December 2012, based on earlier work, circa 2010.

Searchable ordinals via squashed sums (without using the Cantor space).

We can define plenty of searchable sets by transfinitely iterating
squashed sums. These are countable sums with an added limit point at
infinity (see the module SquashedSum).

\begin{code}

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

open import UF-FunExt

module SearchableOrdinals (fe :  U V  funext U V) where

open import SpartanMLTT
open import SquashedSum fe
open import SearchableTypes

\end{code}

We use ordinal encodings, or ordinal expressions, that are slightly
different from the traditional "Brouwer ordinals".

\begin{code}

data OE : U₀ ̇ where
 One  : OE
 Add  : OE  OE  OE
 Mul  : OE  OE  OE
 Sum1 : (  OE)  OE

\end{code}

The empty ordinal is excluded because it is not searchable. It is
merely exhaustible or omniscient (see the module Searchable for a
partial discussion of this). The reason why including the empty
ordinal causes insurmountable problems is discussed in research papers.

The interpretation function is the following, with values on topped
ordinals, where an ordinal is a type equipped with a
subsingleton-valued, well-founded, transitive and extensional relation
(and such a type is automatically a set). "Topped" means that there is
a top element in the order

This version of the function is from 1st July 2018 (the original
version considered only the underlying set of the ordinal and didn't
construct the order as this was work in progress):

\begin{code}

open import Ordinals fe

ord : OE  Ordᵀ
ord      One  = 𝟙º
ord (Add α β) = ord α  ord β
ord (Mul α β) = ord α ׺  ord β
ord (Sum1 α)  = ∑¹ \(i : )  ord(α i)

sord : (α : OE)  usearchable(ord α)
sord       One = 𝟙-usearchable
sord (Add α β) = +usearchable (ord α) (ord β) (sord α) (sord β)
sord (Mul α β) = ×usearchable (ord α) (ord β) (sord α) (sord β)
sord (Sum1 α)  = ∑¹-usearchable (ord  α)  n  sord (α n))

\end{code}

Classically, the squashed sum is the ordinal sum plus 1, and we have a
semantics with this interpretation, which gives ordinals with discrete
underlying sets. Moreover, there is a function maps the underlying set
of the discrete version to the underlying set of the above version.

\begin{code}

ord' : OE  Ordᵀ
ord'        One = 𝟙º
ord' (Add α β) = ord' α  ord' β
ord' (Mul α β) = ord' α ׺  ord' β
ord' (Sum1 α)  = ∑₁ \(i : )  ord'(α i)

dord' : (α : OE)  udiscrete(ord' α)
dord'      One  = 𝟙-udiscrete
dord' (Add α β) = +udiscrete (ord' α) (ord' β) (dord' α) (dord' β)
dord' (Mul α β) = ×udiscrete (ord' α) (ord' β) (dord' α) (dord' β)
dord' (Sum1 α)  = ∑₁-udiscrete (ord'  α)  n  dord' (α n))

{-
ord'-ord : (α : OE) → ⟪ ord' α ⟫ → ⟪ ord α ⟫
ord'-ord One = id
ord'-ord (Add α β) c = {!!}
ord'-ord (Mul α β) = {!!}
ord'-ord (Sum-plus-One α) = {!!}
-}

\end{code}

Brouwer ordinal codes can be mapped to searchable ordinal codes, so
that the meaning is not necessarily preserved, but so that it is
bigger or equal, because sums dominate suprema.

\begin{code}

open import OrdinalCodes

brouwer-to-oe : B  OE
brouwer-to-oe    Z  = One
brouwer-to-oe (S α) = Add One (brouwer-to-oe α)
brouwer-to-oe (L α) = Sum1 i  brouwer-to-oe(α i))

\end{code}

The following is a relatively "small" example: an upper bound of the
ordinal ε₀ (because sums dominate suprema):

\begin{code}

ε₀-upper-bound : Ordᵀ
ε₀-upper-bound = ord(brouwer-to-oe B-ε₀)

searchable-ε₀-ub : usearchable ε₀-upper-bound
searchable-ε₀-ub = sord(brouwer-to-oe B-ε₀)

\end{code}

We can go much higher using the work of many people, including Hancock
and Setzer.