Master's Thesis

Posted on January 4, 2021
Tags: Agda

The final version of my master’s thesis got approved recently so I thought I’d post it here for people who might be interested.

Here’s the pdf.

And all of the theorems in the thesis have been formalised in Agda. The code is organised to follow the structure of the pdf here.

The title of the thesis is “Finiteness in Cubical Type Theory”: basically it’s all about formalising the notion of “this type is finite” in CuTT. I also wanted to write something that could serve as a kind of introduction to some components of modern dependent type theory which didn’t go the standard length-indexed vector route.