Implementing the type theory CCTT
Master Project

Project Description

This project is about implementing the type theory developed in “A Type Theory for Comprehension Categories with Applications to Subtyping”

The abstract of the paper is as follows: n this paper we develop a type theory that we show is an internal language for comprehension categories. This type theory is closely related to Martin-Löf type theory (MLTT). Indeed, semantics of MLTT are often given in comprehension categories, albeit usually only in discrete or full ones. As we explain, requiring a comprehension category to be full or discrete can be understood as removing one `dimension’ of morphisms. Thus, in our syntax, we recover this extra dimension. We show that this extra dimension can be used to encode subtyping in a natural way. Important instances of non-full comprehension categories include ones used for constructive or univalent intensional models of MLTT and directed type theory, and so our syntax is a more faithful internal language for these than is MLTT.

The goal of this project is to implement the type theory, either in a computer proof assistant (Rocq, Agda, Lean, or other) or in a programming language such as Haskell or Ocaml - according to the preferences of the student. In the first case, the goal is to prove properties of the type theory. In the second, the goal would be to have a practical implementation.

Links:

• The paper is available at https://arxiv.org/abs/2503.10868

Project Goals

In this project, you will work on the following goals:

• Learn the basics of Martin-Löf type theory and its categorical semantics
• Understand the paper “A Type Theory for Comprehension Categories with Applications to Subtyping”
• Option 1: Learn to use a computer proof assistant
• Option 2: Learn how to implement a type theory in a functional programming language

Contacts for the Project

• Benedikt Ahrens (TU Delft)