##
Computer formalization of Voevodsky's theory of type theories

Master Project

#### Project Description

In the last years of his life, Fields Medalist Vladimir developed a mathematical theory of type theories. The main purpose of this theory is twofold:

- to give a precise mathematical definition of what a “type theory” is
- to give a mathematical justification of recursion on the syntax of a type theory

Recursion on syntax is used to define interpretations of the syntax into worlds of mathematical objects.

When he passed away, Voevodsky left behind a large body of work, a significant part of it unfinished, on his theory of type theories. Voevodsky’s dream was to implement his theory in a computer proof assistant. To this end, his papers are in what he calls “formalization-ready” style, giving much more detail than traditional mathematics articles.

The goal of this project is to implement, in some computer proof assistant (Coq, Lean, Agda, Isabelle,…), a piece of Voevodsky’s mathematical theory.

### Project Goals

In this project, you will work on (some of) the following goals:

- Learn to use one or more computer proof assistants, e.g., Coq, Agda, Lean, Isabelle
- Understand a part of Voevodsky’s theory of type theories
- Implement Voevodsky’s definitions and proofs, possibly filling in gaps

#### Contacts for the Project

- Benedikt Ahrens (TU Delft)
- Kobe Wullaert (TU Delft)

Supervisor(s): Benedikt Ahrens, Kobe Wullaert

Posted: June 05, 2022