{--
Various date-stamps put in when I remembered: \begin{verbatim} Sat Jul 19 10:16:58 BST 1997, Mon Jul 21 10:18:26 BST 1997, [1999-03-11 14:45:04] \end{verbatim} Originally written by Peter Hancock and Anton Setzer, updated by me, Peter Hancock.
This file contains constructions of ordinals up to $\Gamma_0$ using Martin-L\"of type theory with a somewhat non-standard sequence of universes.
This file is changing, as I try to repair its deficiencies, and improve its structure. Among the deficiencies, I cannot yet adequately miniaturise the lens constructions with the current definitions. Instead, the file has at the moment a grotesque hack, by which the notion of lens is built in among the ground types.
\tableofcontents
\section{ The problem }
What do we mean by a construction of an ordinal in a type theory? This is a proof expressed as a term of a certain type in a conservative extension of the type theory, by what I shall call an ordinal notation system.
It would be rather too ambitious to attempt to capture mathematically in its full generality the notion of an ordinal notation system. (In general, a notation system may have a non-trivial type structure.) For present purposes, an ordinal notation system consists of constants and rules formalising a transition system in which the branching is at most countable. I call a state $s$ of the transition system an ordinal notation if it is in the intersection of every state predicate which is progressive with respect to the transition structure. This implies that its tree of predecessors is wellfounded, with ordinal height $|s|$ (`notated' by $s$) in the second number class. The kind of proof I am calling the construction of an ordinal has the (large) type: \newcommand{\Pred}{\mbox{Pred}}\newcommand{\Prog}{\mbox{Prog}}% \[ (P : \Pred, pP : \Prog (P)) -> P(s) \] where $s$ is a state; the ordinal that is constructed is $|s|$.
The next section says more precisely what is meant by an ordinal notation system, and by its adjunction to a host type theory.
\subsection{ Ordinal notations }
An ordinal notation system consists of some constants and rules for a transition system that one adds (conservatively) to a host type theory. I shall use the example of a Sch\"utte-Feferman style notation system based on Veblen's derivative operation.
\newcommand{\OT}{\ensuremath{\mbox{\AE}}} %\newcommand{\w}{\ensuremath{\mathop{\uparrow}}} %\newcommand{\V}{\ensuremath{\mathop{\Uparrow}}} \ABBREVS
There should be a type $\OT$ (for arithmetic expressions), which are typically first order terms with respect to function constants with finite arity. For example: $0$ (constant); $(\WOP)$ (binary, infix, left associative); $(\VEB)$ (binary, infix, right associative) . \begin{center}\noABBREVS \begin{tabular}{l|l} expression & intended interpretation \\ \hline $0 : \OT$ & $0$ \\ $a \WOP b : \OT$, for $a, b : \OT$ & $a + \omega^b$ \\ $a \VEB b : \OT$, for $a, b : \OT$ & $\phi_a b$ \\ \end{tabular} \end{center} (Here $\phi_a b$ is the Veblen hierarchy with initial function $\phi_0 a = \epsilon_a$. I start with the $\epsilon$ numbers rather than (as is more usual) powers of $\omega$ to minimise overlap between the functions $a + \omega^b$ and $\phi_a b$.)
We have for each $a : \OT$ a pair consisting of first a datatype $C(a)$ which is either the empty type, some standard singleton, or the type of natural numbers, and second for each $i : C(a)$ an expression $a[i]$ . We may think of $(\OT,C)$ as family of sets of `selectors'. The set $C(a)$ is the set of selectors of immediate ordinal predecessors of $a$.
More formally, we add the following new rules to the type system: \begin{itemize}
\item First formation rule: $\OT$ is a type.
\item Constructors for $\OT$, appropriate to the scope of the notation system.
\item Second formation rule: if $a : \OT$ , then $C(a)$ is a type.
\item Constructors for $C(a)$, where $a : \OT$. We have \begin{itemize}
\item $0 : C(x)$ where $x$ has the form $a \WOP b$ , or $ a \VEB b$
\item If $n : C(x)$ then $n^+ : C(x)$ , where $x$ has the form $a \VEB b$ or $a \WOP (b \VEB c)$ or $a \WOP (b \WOP c)$.
\end{itemize} We also need to add recursion over these types to the host type system, with the values of recursively defined functions restricted to perhaps ground types.
If the types are `already there', as they are in our case, then we may simply add equations between sets \begin{center} \begin{tabular}{l} $C(0) = \SET{}$, \\ $C(a \WOP 0) = \SET { \_ } $, \\ $C(a \WOP (b \WOP c)) = C(a \WOP (b \VEB c)) = C(a \VEB b) = \Nat $ \end{tabular} \end{center}
The family $(\OT,C)$ is a family of types which are at most countable, and it plays the role of a universe of ground types in what follows.
\item Elimination rule: if $ a : \OT$ and $i : C(a)$ then $a[i] : \OT$.
\item Computation rules for expressions $a[i]$ which are not of constructor form. For example we may take the following: \begin{center} \noABBREVS \renewcommand{\S}{\hspace{1em}} \begin{tabular}{l|l}%{l@{\S$\rightarrow$\S}l} redex & contractum \\ \hline % $0[i]$ & evil \\ $(a \WOP 0)[\_]$ & $a$ \\ % $(a \WOP (b \WOP 0))[0]$ & $a$ \\ % $(a \WOP (b \WOP 0))[n^+]$ & $(\gamma[n]) \WOP b $ \\ $(a \WOP (b \WOP 0))[n]$ & $a (\WOP b)^n $ \\ $(a \WOP b)[n] $ & $a \WOP (b [n]) $ \\ % $(0 \VEB 0)[0] $ & $ 0 $ \\ % $(0 \VEB 0)[n^+] $ & $ (0 \WOP \gamma[n]) $ \\ $(0 \VEB 0)[n] $ & $ (0 \WOP )^n 0 $ \\ % $(0 \VEB (b \WOP 0))[0] $ & $ (0 \VEB b) \WOP 0 $ \\ % $(0 \VEB (b \WOP 0))[n^+] $ & $ (0 \WOP \gamma[n]) $ \\ $(0 \VEB (b \WOP 0))[n] $ & $ (0 \WOP)^n ((0 \VEB b) \WOP 0) $ \\ % % $((a \WOP 0) \VEB 0)[0] $ & $ 0 $ \\ % $((a \WOP 0) \VEB 0)[n^+] $ & $ (a \VEB \gamma[n]) $ \\ $((a \WOP 0) \VEB 0)[n] $ & $ (a \VEB)^n 0 $ \\ % $((a \WOP 0) \VEB (b \WOP 0))[0] $ & $ ((a \WOP 0) \VEB b) \WOP 0 $ \\ % $((a \WOP 0) \VEB (b \WOP 0))[n^+] $ & $ (a \VEB \gamma[n]) $ \\ $((a \WOP 0) \VEB (b \WOP 0))[n] $ & $ (a \VEB)^n (((a \WOP 0) \VEB b) \WOP 0) $ \\ % $(a \VEB 0)[n] $ & $ (a[n]) \VEB 0 $ \\ $(a \VEB (b \WOP 0))[n] $ & $ (a[n]) \VEB ((a \VEB b) \WOP 0) $ \\ $(a \VEB b)[n] $ & $ a \VEB (b[n]) $ \end{tabular} \end{center} \end{itemize}
The use of iterative exponents in the table above is shorthand for expressions involving the recursor over $\Nat$. Row order is significant in the table, in that each successive row has an implicit ``\dots and none of the above''.
%What is special about $0$, $1$ and $\omega$ is that these are the only %countable ordinals closed under both $+$ and $\sum$.
In general, a transition system may have states that are not wellfounded, as well as states that are wellfounded, but cannot be proved so inside a particular type theory.
\subsection{ A simpler notation system }
There are a lot of different forms of expression in the definition of the transition structure of the previous section. This makes proofs of the simplest lemma quite large, as there will be a case for each such form. When one writes out a few such proofs, one gets the strong feeling that the case structure is irrelevant. So long as one has expressions with the right predecessor structure, it does not matter how one gets them.
For this not very well explained reason, in this file, we simply defined the ordinal notation system to be closed under three constructors: \begin{center} \begin{tabular}[t]{l} $0 : \OT$ \\ $S : \OT -> \OT$ \\ $L : (\Nat -> \OT) -> \OT$ \end{tabular} \end{center} At least there is just one kind of limit.
\subsection{ Comparision of expressions }
Given any transitive transition system, one can define a relation $\alpha \preceq \beta$ between a wellfounded state $\alpha$, and an arbitrary state $\beta$, by recursion on the proof that $\alpha$ is accessible. \[ \alpha \preceq \beta = (\prod i : C(\alpha) \sum j : C(\beta)) \alpha[i] \preceq \beta[j] \] This requires a universe which is closed under the quantifier combination $ (\prod i : C(\alpha) \sum j : C(\beta)) $.
--}
{--
\section{ Preliminaries }
--}
{-- the function space construction at type level. --}
PI = \ A B -> ( a : A )-> B a
: ( A : Type, B : ( a : A )-> Type )-> Type,
ARROW
= \ A B -> PI A (\ a -> B)
: ( A : Type, B : Type )-> Type,
{-- when the domains are the same as the range, I call it an operation --}
OP = \ A -> ARROW A A
: ( A : Type )-> Type,
OP2 = \ A -> ARROW A (OP A)
: ( A : Type )-> Type,
OP3 = \ A -> ARROW A (OP2 A)
: ( A : Type )-> Type,
{--
the (usually suppressed) decoding of sets as types.
It helps to make it explicit..maybe.
--}
Lift = \ A -> A
: ( A : Set )-> Type,
{-- two kinds of `subset'. --}
Pow = \ A -> ARROW A Set
: ( A : Type )-> Type,
Fam = \ A -> sig { U : Set, T : ARROW (Lift U) A }
: ( A : Type )-> Type,
{-- the quantifiers over sets. --}
Pi = \ A B -> ( x : A )-> B x
: PI Set (\ A -> Pow (Pow (Lift A))),
Sigma= \ A B -> sig { p0 : A , p1 : B p0 }
: ( A : Set )-> Pow (Pow (Lift A)),
Arrow
= \ A B -> ( x : A )-> B
: OP2 Set,
{--
I call a function an operation when the argument and value
types are the same
--}
op = \ A -> Arrow A A
: OP Set,
op2 = \ A -> Arrow A (op A)
: OP Set,
op3 = \ A -> Arrow A (op2 A)
: OP Set,
id = \ A x -> x
: PI Set op,
{--
Conjunction. It is extremely convenient to have access to types of pairs. For example, we want to pack and unpack proofs of progressivity, which have three components.
--}
And = \ A B -> data { $pr( a : A, b : B ) }
: OP2 Set,
And3 = \ A B C -> And (And A B) C
: OP3 Set,
mk3 = \ A a B b C c -> $pr ($pr a b) c
: ( A : Set, a : A, B : Set, b : B, C : Set, c : C )-> And3 A B C,
{- Unfortunately, no way to avoid this plumbing. --}
p3_1 = \ A B C x -> case x of {
$pr x' c -> case x' of {
$pr a b -> a}}
: ( A : Set, B : Set, C : Set, x : And3 A B C)-> A,
p3_2 = \ A B C x -> case x of {
$pr x' c -> case x' of {
$pr a b -> b}}
: ( A : Set, B : Set, C : Set, x : And3 A B C)-> B,
p3_3 = \ A B C x -> case x of {
$pr x' c -> case x' of {
$pr a b -> c}}
: ( A : Set, B : Set, C : Set, x : And3 A B C)-> C,
{--
\section{ The natural numbers }
It is convenient to introduce first the empty set and the standard singleton.
--}
Zero = data {} : Set, One = data { $0 } : Set,
{-- The natural numbers, and countable sequences. --}
N = data { $0, $S ( pd : N ) }
: Set,
{-- types of sequences, large and then small. --}
SEQ = \ A -> ARROW (Lift N) A
: ( A : Type )-> Type,
LIMOP
= \ A -> ARROW (SEQ A) A
: ( A : Type )-> Type,
Seq = \ A -> Arrow N A
: OP Set,
Prodn = \ X -> Pi N X
: LIMOP Set,
Limop
= \ A -> Arrow (Seq A) A
: OP Set,
{--
Iteration of operations on a set.
First we define a certain kind of tail-recursive iteration. (It can be reduced to ordinary iteration on op A.)
The function $It_T$ returns the sequence of finite iterates of the function given as its argument.
--}
It_official
= \ m A f a ->
let {
g = \ n -> case n of { $0 -> a, $S n' -> f (g n') }
: Seq A }
in g m
: ( n : N, A : Set )-> op (op A),
Rec_official
= \ m P f a ->
let {
g = \ n -> case n of { $0 -> a, $S n' -> f n' (g n') }
: (n : N)-> P n }
in g m
: ( n : N,
P : (n : N)-> Set,
step : (n : N, x_ : P n) -> P ($S n),
base : P $0 )-> P n,
It_T
= \ A f ->
let {
g = \ n ->
case n of { $0 -> \ x -> x,
$S n' -> \ x -> g n' (f x) }
: Seq (op A) }
in g
: ( A : Set, f : op A )-> Seq (op A),
{--
The basic kind of iteration is not tail-recursive, but ``lazy''. The function is used only in the proof of the culminating theorem .
--}
It = \ A f a ->
let {
g = \ n -> case n of { $0 -> a, $S n' -> f (g n') }
: Seq A }
in g
: ( A : Set, f : op A, a : A )-> Seq A,
It''' = \ A f a n -> It_official n A f a
: ( A : Set, f : op A, a : A )-> Seq A,
{-- We can define tail iteration in terms of head iteration. --}
It_T2
= \ A f -> It (op A) (\ g x -> g (f x)) (\ x -> x)
: ( A : Set, f : op A )-> Seq (op A),
It_T2'
= \ A f n -> It_official n (op A) (\ g x -> g (f x)) (\ x -> x)
: ( A : Set, f : op A )-> Seq (op A),
{--
\section{ Ordinals }
As discussed somewhere above, we use the `real' ordinals, rather than the ordinal notation system.
--}
OT = data { $0, $S ( a' : OT ), $L ( s : Seq OT ) }
: Set,
C = \ a -> case a of { $0 -> Zero, $S a' -> One, $L f -> N }
: ( a : OT )-> Set,
pd = \ a i -> case a of { $0 -> case i of {}, $S a' -> a', $L f -> f i }
: ( a : OT, i : C a )-> OT,
opOT = op OT
: Set,
{--
Define the notation system, just in case I want to try using that.
--}
On = data { $0, $gen ( a : On, b : On ), $veb ( a : On, b : On )}
: Set,
Cn = \ a -> case a of {
$0 -> Zero,
$gen a1 b -> case b of {
$0 -> One,
$gen a2 b1 -> N,
$veb a2 b1 -> N},
$veb a1 b -> N}
: Pow On,
pdn = \a i->case a of {
$0 -> case i of {},
$gen a1 b -> case b of {
$0 -> a1,
$gen a2 b1 -> case b1 of {
$0 -> It On (\x->$gen x a2) a1 i,
$gen a3 b2 -> $gen a1 (pdn b i),
$veb a3 b2 -> $gen a1 (pdn b i)},
$veb a2 b1 -> $gen a1 (pdn b i)},
$veb a1 b -> case a1 of {
$0 -> let { e (a : On) = $gen $0 a : On }
in case b of {
$0 -> It On e $0 i,
$gen a2 b1 -> case b1 of {
$0 -> It On e ($gen ($veb a1 a2) $0) i,
$gen a3 b2 -> $veb a1 (pdn b i),
$veb a3 b2 -> $veb a1 (pdn b i)},
$veb a2 b1 -> $veb a1 (pdn b i)},
$gen a2 b1 -> [],
$veb a2 b1 -> []}}
: ( a : On, i : Cn a )-> On,
{-- Some less barbarous notation than the dollars. --}
zeroOT
= $0
: OT,
succOT
= \ a -> $S a
: opOT,
oneOT
= succOT zeroOT
: OT,
limOT
= \ f -> $L f
: Limop OT,
{-- Identity function, composition, and pointwise limits. --}
IdOT = \ a -> a
: opOT,
CompOT
= \ f g a -> f (g a)
: op2 opOT,
pwlimOT
= \ sf a -> limOT (\ n -> sf n a)
: Limop opOT,
{-- Omega-iteration of an OT function, tail recursive style. --}
omItOT_T
= \ f -> pwlimOT (It_T OT f)
: op opOT,
{-- variant: better version of tail iteration --}
omItOT_T2
= \ f -> pwlimOT (It_T2 OT f)
: op opOT,
{--
\section{ Ordinal arithmetic }
We define the functions $\alpha + \omega^\beta$ and $\phi_\alpha \beta$ so that they satisfy the computational equations of our original system of expressions.
\subsection{ $\alpha + \omega^\beta$ }
A mutually recursive definition of the first arithmetic operator $\alpha + \omega^\beta$, together with the iterates $\alpha + (\omega^\beta)\times n$.
The following definitions, which are apparently equivalent, cannot be substituted for the definitions below The proof checker half is highly intensional, with effects which are sometimes puzzling.
\begin{verbatim} ---------------------------------------- | pw = \ a b -> | case b of { | $0 -> $S a, | $S b' -> $L (It OT (\ a' -> pw a' b) a), | $L f -> $L (\ n -> pw a (f n)) } | : op2 OT ,
| pwm = \ a b -> It OT (\a'->pw a' b) a | : ( a : OT, b : OT )-> Seq OT , +++++++++++++++++++++++++++++++++++++++++ \end{verbatim}
Nevertheless, it may be possible to find a way round this, so as to use the definition above, which is simpler, rather than the monstrosity that follows.
--}
pwdef
= let {
pw = pwdef.pw
: op2 OT,
pwm = pwdef.pwm
: ( a : OT, b : OT )-> Seq OT }
in struct {
pw = \ a b ->
case b of {
$0 -> $S a,
$S b' -> $L (pwm a b'),
$L f -> $L (\ n -> pw a (f n)) },
pwm = \ a b -> It OT ( \ x -> pw x b ) a
}
: sig { pw : op2 OT, pwm : ( a : OT, b : OT )-> Seq OT },
{-- # case m of { $0 -> a, $S n' -> pw (pwm a b n') b } -}
{-- $pw(a,b) = a + {\omega}^b$. --}
pw = pwdef.pw
: op2 OT,
{-- $ pwm(a,b,n) = a + (\omega^b)*n $. --}
pwm = pwdef.pwm
: ( a : OT, b : OT )-> Seq OT,
{-- $ exp(a) = \omega^a$. --}
exp = pw zeroOT
: opOT,
{--
\subsection{ $\phi_\alpha \beta$ }
--}
{--
Enumf standas for enumerator of fixed points. It is a lousy name.
If the argument of $f$ of enumf is a closure operation, then the value is a normal function enumerating the fixed points of f.
The following is in my opinion the correct version of enumfOT. (It is not the one we had originally.)
--}
enumfOT
= \ f a ->
case a of {
$0 -> f $0,
$S b' -> f ($S (enumfOT f b')),
$L g -> $L (\ n -> enumfOT f (g n)) }
: op opOT,
{-- The derivative of a function. --}
deriv
= \ f -> enumfOT (omItOT_T f)
: op opOT,
{-- The derivative of a sequence of functions. --}
derivl
= \ sf -> enumfOT (pwlimOT sf)
: Limop opOT,
{-- Variant: better tail iteration. --}
deriv2
= \ f -> enumfOT (omItOT_T2 f)
: op opOT,
{-- the Veblen hierarchy --}
phi = \ a ->
case a of {
$0 -> deriv exp,
$S a' -> deriv (phi a'),
$L f -> enumfOT (pwlimOT (\ n -> phi (f n))) }
: op2 OT,
{-- variant: better tail iteration --}
phi2 = \ a ->
case a of {
$0 -> deriv2 exp,
$S a' -> deriv2 (phi a'),
$L f -> enumfOT (pwlimOT (\ n -> phi (f n))) }
: op2 OT,
{--
\section{ Universe constructions }
--}
{-- Type of families of sets --}
FSet = Fam Set
: Type,
{-- Empty family of sets. (Not used.) --}
EmptyF
= struct { U = data { }, T = \ a -> case a of { } }
: FSet,
{--
A next-universe operator.
This is becoming distinctly bloated. Not everything is necessary.
We define the closure of a given family of `ground' sets under various type constructors that are used in the proofs of wellfoundedness.
--}
NextU
= \ Ground ->
let {
UG = Ground.U
: Set,
TG = Ground.T
: Pow UG,
{-- a fixed point --}
X = let {
UX = X.U
: Set,
TX = X.T
: Pow UX }
in struct {
U = data {
$ot,
$set,
$el ( u : UG ),
$all ( a : UX, b : ( x : TX a )-> UX ),
$any ( a : UX, b : ( x : TX a )-> UX ),
$ar ( a : UX, b : UX ),
$and ( a : UX, b : UX ),
$seq ( a : UX ),
$prodn ( b : Seq UX ),
$prodseq
( b : ( sa : Seq OT )-> UX ),
$b ( b : ( a : OT )-> UX, a : OT ),
$prodot
( b : ( a : OT )-> UX ) },
T = \ a ->
case a of {
$ot -> OT,
$set -> UG,
$el u -> TG u,
$all a b -> Pi (TX a) (\ x -> TX (b x)),
$any a b -> Sigma (TX a) (\ x -> TX (b x)),
$ar a b -> Arrow (TX a) (TX b),
$and a b -> And (TX a) (TX b),
$seq a -> Seq (TX a),
$prodn b -> Pi N (\ n -> TX (b n)),
$prodseq b
-> ( sa : Seq OT )-> TX (b sa),
$b p a -> Pi (C a) (\ i -> TX (p (pd a i))),
$prodot b -> ( a : OT )-> TX (b a) } }
: FSet }
in X
: OP FSet,
{--
\section{ Miniaturisation }
--}
{--
I suspect most of this serves no purpose, and is done elsewhere.
But here we are concerned with miniaturisation.
We express the basic notions of the theory of lenses relative to a universe.
--}
minitheory
= \ FS ->
theory {
U = (NextU FS).U
: Set,
T = (NextU FS).T
: Pow U,
{-- various forms of pi --}
arrow = \ a b -> $all a ( \ x -> b )
: ( a : U, b : U )-> U,
seq = \ a -> $seq a
: op U,
prodn = \ f -> $prodn f
: ( f : Seq U )-> U,
prodot
= \ f -> $all $ot f
: ( f : ( a : OT )-> U )-> U,
prodseq
= \ f -> $all ($seq $ot) f
: ( f : ( a : Seq OT )-> U )-> U,
pow = \ A -> ( a : A )-> U
: ( A : Set )-> Set,
powOT = pow OT : Set,
{-- inclusion of predicates --}
subsetg (A : U)
= \ X Y -> $all A (\ a -> arrow (X a) (Y a))
: ( X : pow (T A) )-> pow (pow (T A)),
subset
= \ X Y -> subsetg $ot X Y
: ( X : pow OT )-> pow powOT,
{-- every function on $\OT$ determines a predicate transformer --}
substg ( A : U)
= \ f X a -> X (f a)
: ( f : op (T A) )-> op (pow (T A)),
subst = \ f X a -> X (f a)
: ( f : op OT )-> op powOT,
preservedg ( A : U )
= \ X f -> subsetg A X (substg A f X)
: ( X : pow (T A) )-> pow (op (T A)),
preservedOT
= \ X f -> subset X (subst f X)
: ( X : pow OT )-> pow opOT,
closed
= \ X -> subsetg (seq $ot)
(\ f ->prodn (\ n ->X (f n)))
(\ f -> X (limOT f))
: pow powOT,
and = \ a b -> $and a b
: op2 U,
and3 = \ a b c -> and (and a b) c
: ( a : U )-> op2 U,
prog = \ X -> and3 (X zeroOT) (preservedOT X succOT) (closed X)
: pow powOT,
{--
Given a predicate transformer, the property of a predicate that if it is progressive, then its transform is too. (This is an instance of preserving progressivity.)
--}
preservedprog
= \ F X -> arrow (prog X) (prog (F X))
: ( F : op powOT)-> pow powOT,
Prog = \ X -> T (prog X)
: ( X : pow OT )-> Set,
{--
\begin{verbatim} --------------- Prog = \ X -> sig { z : T (X zeroOT), s : T (preservedOT X succOT), l : T (closed X) } : ( X : pow OT )-> Set, Wf = \ a -> ( X : pow OT, pX : Prog X )-> T (X a) : ( a : OT )-> Set } +++++++++++++++++ \end{verbatim}
--}
{-- The intersection of all progressive sets. --}
Wf = \ a -> ( X : pow OT )-> T (arrow (prog X ) (X a))
: ( a : OT )-> Set }
: ( FS : FSet )-> Theory,
{--
The relativised form of transfinite induction: given a universe of `small' sets, we form the intersection of all progressive predicates whose values are small sets.
This is the only export from the theory mini!
--}
wf = \ FS -> (minitheory FS).Wf
: ( FS : FSet )-> Pow OT,
{--
\section{ Theory of lenses }
--}
lenstheory
= \ UT ->
theory {
U = (NextU UT).U
: Set,
T = (NextU UT).T
: Pow U,
{-- 4 different forms of Pi --}
arrow = \ a b -> $ar a b
: op2 U,
prodn = \ f -> $prodn f
: ( f : Seq U )-> U,
prodot
= \ f -> $prodot f
: ( f : ( a : OT )-> U )-> U,
prodseq
= \ f -> $prodseq f
: ( f : ( a : Seq OT )-> U )-> U,
{-- now predicates on a set --}
pow = \ A -> ( a : A )-> U
: OP Set,
{-- inclusion of predicates --}
subsetOT
= \ X Y -> prodot (\ a -> arrow (X a) (Y a))
: ( X : pow OT )-> pow (pow OT),
{-- transformation of a predicate by composition with a function --}
{-- perhaps the arguments should be swapped? --}
subst = \ f X a -> X (f a)
: ( f : op OT )-> op (pow OT),
{-- predicate of a predicate that it is closed under a function --}
preservedOT
= \ X f -> subsetOT X (subst f X)
: ( X : pow OT )-> pow (op OT),
{-- lemma about closure under finite iterates should go here. --}
{--
predicate of a predicate that it is closed under
limits of arbitrary sequences
--}
closed
= \ X ->
prodseq
(\ f -> arrow (prodn (\ n -> X (f n))) (X (limOT f)))
: pow (pow OT),
{-- lemma about closure under omega iteration should go here. --}
{-- ************************************************8 --}
lift = \ a -> T a
: ( a : U )-> Set,
fam = \ A -> Sigma U (\ u -> ( x : lift u )-> A)
: OP Set,
Lift = lift
: Pow U,
Pow = pow
: OP Set,
ProdOT
= prodot
: Pow (Pow OT),
OP = op
: ( A : Set )-> Set,
Arrow = \ a b -> Lift (arrow a b)
: ( a : U, b : U )-> Set,
Holds = \ X a -> Lift (X a)
: ( X : Pow OT, a : OT )-> Set,
SubsetOT
= \ X Y -> Lift (subsetOT X Y)
: ( X : Pow OT, Y : Pow OT )-> Set,
PreservedOT
= \ X f -> Lift (preservedOT X f)
: ( X : pow OT, f : op OT )-> Set,
Closed
= \ X -> Lift (closed X)
: ( X : pow OT )-> Set,
{-- This is head iteration of miniature predicate transformers --}
itPT
= It (pow OT)
: ( F : op (pow OT), X : pow OT )-> Seq (pow OT),
{-- this is tail iteration of MPTs. It is not yet used. --}
itPT_T
= \ F X n -> It_T (pow OT) F n X
: ( F : op (pow OT), X : pow OT )-> Seq (pow OT),
{--
The content of the lemma is that a predicate which is closed
under a function is closed also under all finite iterates of that
function.
--}
PresOTlemma_T
= \ X f p n ->
case n of {
$0 -> \ a xa -> xa,
$S n' -> \ a xa -> PresOTlemma_T X f p n' (f a) (p a xa) }
: ( X : Pow OT, f : opOT, p : PreservedOT X f, n : N )
-> PreservedOT X (It_T OT f n),
{-- variant: use better definition of tail iteration. --}
PresOTlemma_T2
= \ X f p n ->
case n of {
$0 -> \ a xa -> xa,
$S n' -> \ a xa -> PresOTlemma_T2 X f p n' (f a) (p a xa) }
: ( X : Pow OT, f : op OT, p : PreservedOT X f, n : N )
-> PreservedOT X (It_T2 OT f n),
{-- variant: for lazy iteration. --}
PresOTlemma
= \ X f p n a x ->
case n of {
$0 -> x,
$S pd -> p (It OT f a pd) (PresOTlemma X f p pd a x)}
: ( X : Pow OT, f : op OT, p : PreservedOT X f, n : N )
-> PreservedOT X (\x->It OT f x n),
{--
A miniature version of progressivity. Conjunctive!
This seems to mean we need `and' in the universe.
But: we should be able to expand it out, with some
tedium.
And we need quantification over Seq OT -- well, actually, over $C(a)$.
We need, for each $ a : \OT $ , two `quantifiers': $\lambda \, X . \, (\prod i : C(a) )X(a[i])$ and $\lambda \, X . \, X(a)$.
--}
Prog = \ X ->
sig {
z : Holds X zeroOT,
s : PreservedOT X succOT,
l : Closed X }
: ( X : pow OT )-> Set,
preservesprog
= \ F -> ( X : Pow OT, p : Prog X )-> Prog (F X)
: ( F : OP (Pow OT) )-> Set,
{--
The property of a predicate transformer that it preserves progressivity is closed under composition. This is unused.
--}
compprog
= \ F pF G pG X pX -> pF (G X) (pG X pX)
: ( F : OP (Pow OT),
pF : preservesprog F,
G : OP (Pow OT),
pG : preservesprog G )
-> preservesprog (\ X -> F (G X)),
{--
If a predicate transformer preserves progressivity, then so do all its finite iterates. This is really the same proof as something above.
--}
iterprog
= \ F pF X pX n ->
case n of {
$0 -> pX,
$S n' -> pF (itPT F X n') (iterprog F pF X pX n') }
: ( F : OP (Pow OT),
pF : preservesprog F,
X : Pow OT,
pX : Prog X,
n : N )
-> Prog (itPT F X n),
{--
The intersection of a sequence of progressive predicates
is progressive.
--}
Prodprog
= \ Xs pXs ->
struct {
z = \ n -> (pXs n).z,
s = \ a pa n -> (pXs n).s a (pa n),
l = \ as pas n -> (pXs n).l as (\ k -> pas k n) }
: ( Xs : Seq (Pow OT),
pXs : ( n : N )-> Prog (Xs n) )
-> Prog (\ a -> prodn (\ n -> Xs n a)),
{--
A miniature version of a lens.
But we need sig! Perhaps it is enough to have sig over OT? This means we
--}
Lens = \ f ->
sig {
F : OP (Pow OT),
pF : preservesprog F,
dr : ( X : Pow OT, pX : Prog X )
-> SubsetOT (F X) (subst f X) }
: ( f : opOT )-> Set,
{--
A closure lens for $f$ is a lens for the identity, whose range is
closed under $f$.
--}
ClLens
= \ f ->
sig {
F : OP (Pow OT),
pF : preservesprog F,
dr : ( X : Pow OT, pX : Prog X )-> SubsetOT (F X) X,
cl : ( X : Pow OT, pX : Prog X )-> PreservedOT (F X) f }
: ( f : opOT )-> Set,
Idlens
= struct {
F = \ X -> X,
pF = \ X pX -> pX,
dr = \ X pX a x -> x }
: Lens IdOT,
{--
Lens composition. Notice the order reversal.
This is unused. It could be used in the lemmas about iterates.
--}
Complens
= \ f g lf lg ->
struct {
F = \ X ->
lg.F (lf.F X),
pF = \ X pX ->
lg.pF (lf.F X) (lf.pF X pX),
dr = \ X pX a x ->
lf.dr X pX (g a) (lg.dr (lf.F X) (lf.pF X pX) a x) }
: ( f : opOT, g : opOT, lf : Lens f, lg : Lens g )
-> Lens (CompOT f g),
{--
Given a lens for each of a sequence, get a lens for the limit.
Here we need closure of the universe of predicates under
countable intersection.
--}
Prodlens
= \ sf sl ->
struct {
F = \ X a -> prodn (\ n -> (sl n).F X a),
pF = \ X pX ->
struct {
z = \ n ->
((sl n).pF X pX).z,
s = \ a pa n ->
((sl n).pF X pX).s a (pa n),
l = \ as pas n ->
((sl n).pF X pX).l as (\ k -> pas k n) },
dr = \ X pX a x ->
pX.l (\ n -> sf n a)
(\ n -> (sl n).dr X pX a (x n)) }
: ( sf : Seq opOT, sl : ( n : N )-> Lens (sf n) )
-> Lens (pwlimOT sf),
{--
From a lens for a function $f$, we can get a closure lens for $f$: that
is, a lens for the identity which is everywhere closed under $f$.
Here we need closure of the universe of predicates under countable intersection,
and formation of sequences by iteration.
--}
MkCllens
= \ f l ->
struct {
F = \ X a -> prodn (\ n -> itPT l.F X n a),
pF = \ X pX ->
Prodprog (itPT l.F X) (iterprog l.F l.pF X pX),
dr = \ X pX a x -> x $0,
cl = \ X pX a x n ->
l.dr (itPT l.F X n) (iterprog l.F l.pF X pX n) a
(x ($S n)) }
: ( f : opOT, l : Lens f )-> ClLens f,
{--
From a closure lens for $f$, we get a closure lens
for $f^\omega$.
--}
omItCllens_T
= \ f l ->
struct {
F = l.F,
pF = l.pF,
dr = l.dr,
cl = \ X pX a x ->
(l.pF X pX).l (\ n -> It_T OT f n a)
(\ n -> PresOTlemma_T (l.F X) f (l.cl X pX) n a x) }
: ( f : opOT, l : ClLens f )-> ClLens (omItOT_T f),
{-- variant: Head recursive --}
omItCllens_H
= \ f l ->
struct {
F = l.F,
pF = l.pF,
dr = l.dr,
cl = \ X pX a x ->
(l.pF X pX).l (\ n -> It_T2 OT f n a)
(\ n -> PresOTlemma_T2 (l.F X) f (l.cl X pX) n a x) }
: ( f : opOT, l : ClLens f )-> ClLens (omItOT_T2 f),
{--
Given a closure lens for a function $f$, we can get a
lens for the function $\alpha \mapsto (f (.) (+1))^\alpha(f(0))$.
It should be pointed out that there is no recursion here.
--}
Mkenumflens
= \ f l ->
struct {
F = \ X a -> l.F X (enumfOT f a),
pF = \ X pX ->
struct {
z = l.cl X pX zeroOT (l.pF X pX).z,
s = \ a pa ->
l.cl X pX (succOT (enumfOT f a))
((l.pF X pX).s (enumfOT f a) pa),
l = \ as pas ->
(l.pF X pX).l (\ n -> enumfOT f (as n)) pas },
dr = \ X pX a x -> l.dr X pX (enumfOT f a) x }
: ( f : opOT, l : ClLens f )-> Lens (enumfOT f),
{-- The construction on lenses corresponding to enumfOT --}
enumflens
= \ f l -> Mkenumflens f (MkCllens f l)
: ( f : opOT, l : Lens f )-> Lens (enumfOT f),
Succlens_T
= \ f l ->
Mkenumflens (omItOT_T f) (omItCllens_T f (MkCllens f l))
: ( f : opOT, l : Lens f )-> Lens (deriv f),
{-- This is unused. --}
Succlens_H
= \ f l ->
Mkenumflens (omItOT_T2 f) (omItCllens_H f (MkCllens f l))
: ( f : opOT, l : Lens f )-> Lens (deriv2 f),
Limlens
= \ sf l -> enumflens (pwlimOT sf) (Prodlens sf l)
: ( sf : Seq opOT, l : ( n : N )-> Lens (sf n) )
-> Lens (derivl sf),
{--
If $X$ is closed under $(+\omega^b)$
then it is closed under $(+(\omega^b \times n))$
--}
expLensLemma
= \ X b ->
PresOTlemma X (\a ->pw a b)
: ( X : Pow OT,
b : OT,
pb : T (preservedOT X (\ a -> pw a b)),
n : N )
-> T (preservedOT X (\ a -> pwm a b n)),
{--
The Gentzen lens. Here we need closure of the universe
of predicates under (lifted) arrow, and universal quantification.
Even the universal quantification is very restricted.
--}
expLens
= struct {
F = \ X b -> preservedOT X (\ a -> pw a b),
pF = \ X pX ->
struct {
z = pX.s,
s = \ b pb a pa ->
pX.l (pwm a b)
(\ n -> expLensLemma X b pb n a pa),
l = \ f pf a pa ->
pX.l (\ n -> pw a (f n)) (\ n -> pf n a pa) },
dr = \ X pX a x -> x zeroOT pX.z }
: Lens exp,
{--
The intersection of all progressive small predicates.
Note that this is not a small set.
--}
TI = \ a -> ( X : Pow OT, pX : Prog X )-> Holds X a
: ( a : OT )-> Set,
{--
If we have a lens for a function, then we have
transfinite induction up to its first value (at least).
--}
LenstoTI
= \ f l X pX -> l.dr X pX zeroOT (l.pF X pX).z
: ( f : opOT, l : Lens f )-> TI (f zeroOT) }
: ( UT : FSet )-> Theory,
{--
\section{ Veblen step }
It should almost be possible now to sort out the hack here.
There are several universes to get clear about.
There is the universe over which we construct predicate transformers. For the Gentzen construction, we need the universe to be closed under the predicate transformer $ X \mapsto X \subseteq X (.) (\WOP a) $.
For the Veblen construction, we need the universe to be closed under (to put it loosely) products of certain sequences of functions; more exactly, we need it to be closed under the predicate transformer $ B(X, \alpha) = \prod i : C(\alpha)X(\alpha[i])$.
We get these two predicate transformers if we assume
There is the universe in which we express the notion of lens, which consists of a particularly simple kind of `geometric' formula. (I have no real idea whether `geometric' is appropriate.) Here one has schemas with the general shape: \[ \begin{array}{l} \Phi : \Pow{S} -> \Pow{S} \\ B(X) \subseteq X => \Phi(X) \subseteq \Psi(X) \end{array} \] where $\Phi$ and $\Psi$ are predicate transformers, and $X$ is a universally quantified predicate variable. This is a language in which we express properties of predicate transformers of a very specific kind. This is the language in which the theory of lenses is conducted.
--}
veblentheory
= \ FS ->
theory {
{--
#
U = FS.U
: Set,
T = FS.T : ( X : U )-> Set,
--}
{-- Horrible hack, to get lenses `small'. --}
FSbig = struct { U = OT, T = \ a -> (lenstheory FS).Lens (phi a) }
: FSet,
FSbig'
= NextU FSbig
: FSet,
Ubig = FSbig'.U
: Set,
Tbig = FSbig'.T
: ( X : Ubig )-> Set,
lenscode
= \ a -> $el a
: ( a : OT )-> Ubig,
lenscode
= \ a -> [(lenstheory FS).Lens (phi a)]
: ( a : OT )-> Ubig,
Lensin
= \ a -> Tbig (lenscode a)
: ( a : OT )-> Set,
{--
#
zerocase
= (lenstheory FS).expLens
: Lensin zeroOT,
--}
zerocase
= (lenstheory FS).Succlens_T exp (lenstheory FS).expLens
: Lensin zeroOT,
succcase
= \ a pa -> (lenstheory FS).Succlens_T (phi a) pa
: ( a : OT, pa : Lensin a )
-> Lensin (succOT a),
limcase
= \ as pas -> (lenstheory FS).Limlens (\ n -> phi (as n)) pas
: ( as : Seq OT, pas : ( n : N )-> Lensin (as n) )
-> Lensin ($L as),
lensgen
= \ a p ->
p lenscode
(mk3 ((lenstheory FS).Lens (deriv exp)) zerocase
((a:OT, pa:Lensin a)->Lensin (succOT a)) succcase
((as:Seq OT, pas:(n:N)->Lensin (as n))
->Lensin ($L as)) limcase )
{-- (struct { z = zerocase, s = succcase, l = limcase }) --}
: ( a : OT, p : wf FSbig a )-> Lensin a,
{--
\begin{verbatim} ---------------------- lensgen = \ a p -> p lenscode (struct { z = zerocase, s = succcase, l = limcase }) : ( a : OT, p : ti FSbig a )-> Lensin a, ++++++++++++++++++++++ \end{verbatim}
--}
tishift
= \ a p X pX ->
(lenstheory FS).LenstoTI (phi a) (lensgen a p) X
(case pX of {
$pr a1 b -> case a1 of {
$pr a2 b1 -> struct {
z=a2,
s=b1,
l=b}}})
: ( a : OT, p : wf FSbig a )-> wf FS (phi a zeroOT),
{--
\begin{verbatim} ------------------- tishift = \ a p X pX -> (lenstheory FS).LenstoTI (phi a) (lensgen a p) X (struct { z = pX.z, s = pX.s, l = pX.l }) : ( a : OT, p : ti FSbig a )-> ti FS (phi a zeroOT), ++++++++++++++++++++ \end{verbatim}
--}
ti0 = \ X pX -> case pX of {
$pr a b -> case a of {
$pr ze b1 -> ze}}
: wf FSbig zeroOT,
ti1 = \ X pX -> case pX of {
$pr a b -> case a of {
$pr ze sp -> sp zeroOT ze}}
: wf FSbig oneOT,
tiepsilon0
= tishift zeroOT ti0
: wf FS (phi zeroOT zeroOT) }
: ( FS : FSet )-> Theory,
{--
\begin{verbatim} ----------------- ti0 = \ X pX -> pX.z : ti FSbig zeroOT,
ti1 = \ X pX -> pX.s zeroOT pX.z : ti FSbig oneOT,
tiepsilon0 = tishift oneOT ti1 : ti FS (phi oneOT zeroOT) ++++++++++++++++++ \end{verbatim}
--}
{--
This is the culmination of everything. We define a sequence of proofs of well foundedness for the usual sequence of approximants of $\Gamma_0$
--}
P = \ FS n ->
case n of {
$0 -> \ X pX -> case pX of {
$pr a b -> case a of {
$pr a1 b1 -> b1 zeroOT a1}}, {-- pX.s zeroOT pX.z, --}
$S n' -> \ X pX ->
(veblentheory FS).tishift
(It OT (\ a -> phi a zeroOT) oneOT n')
(P (veblentheory FS).FSbig n') X pX }
: ( FS : FSet, n : N )
-> wf FS (It OT (\ a -> phi a zeroOT) oneOT n),
{-- It is a kind of tradition to end half files this way: --}
END = [ ]
: [ ]