Mathematics

Mathematics has always been a passion of mine, and I have been lucky enough to have spent the last decade studying it full time. Here I have collected a few topics I have had the pleasure of studying.

Articles and theses

For convenience, here is a list of my articles and theses.

• Symmetric containers (Master thesis)
• Univalent types, sets and multisets (PhD Thesis)
• Multisets in type theory
• From multisets to sets in homotopy type theory
• Type theoretical databases

Type theory

Type theory is a family of formal languages for mathematics, based on the idea that mathematical objects can be separated into two classes: types and elements. At a first approximation one may think of types as collections of elements. For instance, the type of natural numbers is denoted ℕ, and has elements 0,1,2,3,4,…. The fact that an element, a, is of a certain type, A, is denoted a : A. So for instance 2 : ℕ is the fact that 2 is an element of the natural numbers. The origins of type theory was Russel and Whitehead’s developments in Principia Mathematica, but perhaps even more essential was the development of dependent type theory by Per Martin-Löf in the eary 1970’s.

The purpose of type theory is to provide a robust foundation of mathematics, and there are computer tools, such as Agda, which can check the correctness of mathematical proofs formulated in a type theory. Constructing a formal proof of a mathematical statement has many advantages:

• A formalised proof is mechanically checked, removing some of the concerns one might have about its correctness.
• Being forced to spell out the entire proof one sometimes reaches a new understanding of the proof. Perhaps there was a hidden symmetry in the cases you spelled out, allowing you to factor the proof more neatly. Or maybe there a case you thought was was trivial, but actually contained some deeper insight.
• Being a theorem of a formal theory means that the proof now applies to all models of that theory. This means that your theorem may apply more generally than you first thought.
• If the proof is constructive, you can now let the computer run it on any special case, giving you easy access to concrete results from the general theorem.

It is also possible to study type theory meta-mathematically. This means to study type theory as a mathematical object. This can be done proof-theoretically, by directly studying the structure of types and terms, or model-theoretically, by studying models — mathematical objects which behave according to the rules of type theory. These two ways are connected through the term-model, a model of type theory built from its terms and types.

There are few things which distingishes type theory from its rival, set theory. Most superficially, sets can elements of other sets, while types cannot be elements of other types. This complication of sets within sets within sets, is used in set theory to encode all kinds of mathematical objects as sets.

For instance, the number 3 is encoded as the set {∅,{∅},{∅,{∅}} Type theory, on the other hand, introduces new symbols for each kind of construction, so that the number 3 is encoded as S S S 0, the third successor of 0.

At a more fundamental level, type theory contains its own logic. In contrast, set theory is usually formulated on top of first-order logic. In type theory, all the logical connectives and quantifiers, such as “and”, “or”, “implies”, “for all”, “there exists”, “true” and “false”, are expressed as type constructions. For instance, the logical concept of “and” coincides with the cartesian product, since a proof a conjunction A & B is actually a pair of proofs (a,b). In general one of the many interpretations of a : A is that a is a proof of the proposition A. This feature of type theory is called propositions as types.

My personal perspective on type theory has two focusses. Firstly, I really enjoy working within type theory. I take much pleasure in formalising proofs neatly, and at the right level of abstraction. In fact, few pleasures come close to that of completing a formalised proof: That moment, when the type-checker program returns to me the confirmation that my proof is correct, and I realise that your proof is now done, is the moment when I can truly appriciate the Orphic meaning of the word theory (gr. θεωρία): passionate sympathetic contemplation.

Oposed to this strong appreciation of working within type theory, is a feeling that our, at least my own, understanding of type theory itself, and logical theories in general, is superficial. I get this feeling because, while we seem to know a lot of truths about type theories, few of these are stated and proved in any generality¹. For instance, the intiality theorem for term models should hold for any type theory satisfying certain constraints, but what exactly such type theories might be, we do not know, so we cannot even state the general theorem.

Algebraic type theory

Containers

Multisets and sets

Databases