Contents

1 Introduction 3 1.1 Overview, predigested summary of main points . . . . . . . . 3 1.2 Pointing out of original bits, and bits others contributed … 3 1.3 Whatever is formally necessary . . . . . . . . . . . . . . . . . 3

2 Apologia 5 2.1 Functional programming languages with dependent type systems 5 2.2 Expressibility . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Transition systems, simulations . . . . . . . . . . . . . . . . . 5 2.4 Accessibility, transitivity . . . . . . . . . . . . . . . . . . . . . 5 2.5 Concept of ordinal: ZF, type theory, etc . . . . . . . . . . . . 5 2.6 Ordinal notation systems, some examples . . . . . . . . . . . . 5 2.7 Decidable type/proof checking, and recursion theoretic rea-

sons why decidability entails incompleteness . . . . . . . . . . 6 2.8 The ‘tide mark’ of a type-system in an uncountable domain:

numerical functions, countable ordinals . . . . . . . . . . . . . 6

3 Basic arithmetic of transition systems 7 3.1 Arithmetic up to the exponential . . . . . . . . . . . . . . . . 7 3.2 Ordinal exponentiation . . . . . . . . . . . . . . . . . . . . . . 7

4 Models of type theory 9 4.1 Interest of predicativity . . . . . . . . . . . . . . . . . . . . . . 9 4.2 General concept of model for dtt . . . . . . . . . . . . . . . . 9 4.3 ‘Realisability ’ models . . . . . . . . . . . . . . . . . . . . . . 9 4.4 Some examples: Aczel, Beeson?, Martin-Löf/Caterina Coquand 9 4.5 Wrinkles to get strong normalisation, and for ‘open’ terms . . 10 4.6 Idea of this model . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.7 The use of a universe operator to formalise positive inductive

definitions of sets, families of sets, etc . . . . . . . . . . . . . . 10

5 Execution of this model 11

6 Idea of lenses 13

6.1 Non-dependent lenses . . . . . . . . . . . . . . . . . . . . . . . 13 6.1.1 Iteration/Exponentiation and higher types . . . . . . . 13 6.1.2 Iteration at transfinite types . . . . . . . . . . . . . . . 13

7 Construction 15

8 Loose ends 17

Chapter 1

Introduction

1.1 Overview, predigested summary of main points

1.2 Pointing out of original bits, and bits others contributed

1.3 Whatever is formally necessary

4 CHAPTER 1. INTRODUCTION

Chapter 2

Apologia

Argues for the interest of the subject matter, which may be unusual in computer science.

2.1 Functional programming languages with

dependent type systems 2.2 Expressibility 2.3 Transition systems, simulations 2.4 Accessibility, transitivity 2.5 Concept of ordinal: ZF, type theory, etc 2.6 Ordinal notation systems, some examples

Cantor normal form. Veblen-Schütte hierarchy. One using a ‘collapse’ of the third (constructive) number classes (basis of modern approach).

6 CHAPTER 2. APOLOGIA

2.7 Decidable type/proof checking, and recursion theoretic reasons why decidability entails incompleteness

2.8 The ‘tide mark’ of a type-system in an uncountable domain: numerical functions, countable ordinals

Numerical hierarchies: Hardy, Grzegorczyk, slow-growing.

Chapter 3 Basic arithmetic of transition systems

Bread-and-butter.

3.1 Arithmetic up to the exponential

Some categorical descriptions. (As in Kahrs, towards a semantics for termination proofs.)

3.2 Ordinal exponentiation

Why well-foundedness seems to be essential to develop arithmetic beyond exponential.

8 CHAPTER 3. BASIC ARITHMETIC OF TRANSITION SYSTEMS

Models of type theory

4.1 Interest of predicativity

The justification of inductive definitions. Their ‘justification’ by Π^{1}_{1} impredicative quantification. The (abandoned) idea of ‘meaning theory’ based on elimination rules. Why it is not clear why this idea was ever abandoned.

4.2 General concept of model for dtt

Martin-Löf, Dybjer, Hofmann.

Martin-Löf’s pursuit of models that are locally formalisable.

4.3 ‘Realisability ’ models

In which terms/programs are interpreted as ‘normal forms’, plus proofs that those normal terms are.

4.4 Some examples: Aczel, Beeson?, Martin-

Löf/Caterina Coquand

Martin-Löf’s pursuit of models that are locally formalisable.

4.5 Wrinkles to get strong normalisation, and for ‘open’ terms

4.6 Idea of this model

Relativisation of realisability with respect to a new, ‘indeterminate’ type variable.

4.7 The use of a universe operator to formalise positive inductive definitions of sets, families of sets, etc

μ for operators. Apparatus one needs: constructors, structural recursion. Something about ν.

Chapter 5 Execution of this model

12 CHAPTER 5. EXECUTION OF THIS MODEL

Idea of lenses

Note: the word ‘lens’ will probably not occur. A ‘lens’ is a predicate transformer that can be used to show a function preserves accessibility. A ‘nondependent’ lens is one where the predicates are ‘over a singleton’ (degenerate)

– really they are type-constructors.

6.1 Non-dependent lenses

How to use ‘arrow’ and ω-iteration to simulate ordinals up to ϵ_{0}.

6.1.1 Iteration/Exponentiation and higher types

6.1.2 Iteration at transfinite types

Aczel’s solution. My solution. Inverse limits.

How the step to the ‘next universe’ (extending and containing a given one, closed under predicative Π) corresponds to a ‘nesting’ the Veblen function an extra level.

14 CHAPTER 6. IDEA OF LENSES

Chapter 7 Construction

This is an exposition, extension and simplification of a construction of ordinals up to Γ_{0} done with Anton Setzer. (Resurrecting my original idea.)

16 CHAPTER 7. CONSTRUCTION

Loose ends

Upper bounds. Arithmetic combinators.

Exploitation of lenses to construct well-orderings in the system modelled in the middle two chapters. (Which probably has the same strength as typetheory with the W-type, analysed by Setzer, using classical Kripke-Platek set theory with one inaccessible and a few regulars beyond.)

Recent work on universes: Palmgren ‘super-universes’ (closed under the step to the next universe), Setzer, Rathjen. The idea of forming universes in type theory is to introduce them as (families of) sets closed under a specified gaggle G of type-constructors. The universe then ‘reflects’ G. Setzer’s ‘Mahlo’ universe.

The use of universes in functional programming. Translations of weak classical systems into ‘classical’ universes. (Coquand, Palmgren.)