Internal Models of Homotopy Type Theory

Homotopy Type Theory is a formal system that conjecturally can be used as a foundation for Mathematics. It has at least two advantages over other existing foundations of Mathematics. It has a flexible language in which the notion of space is as primitive as the notion of set, thus making it easier to work with space-like structures. It is also easy to encode in a computer, so that the computer can automatically check that the proofs written in this language are correct. One of the key steps in showing that this language can indeed be used as a foundation for Mathematics, is to show that it is expressible enough to describe itself. For this a model of the language has to be constructed using the language itself, this is known as an internal model. This project aims to construct such an internal model.

Faculty Supervisor:

J. Daniel Christensen

Student:

Partner:

University of Nottingham

Discipline:

Mathematics

Sector:

Education

University:

Western University

Program: