Category Theory in univalent Type Theory

Potential supervisors: 


The goal of this project will be to implement category theory in cubical Agda, which is a computational implementation of type theory with the axiom of univalence. It will be a continuation of a previous master thesis which implemented some results about monads.

The goal will be on one hand to find examples in category theory where univalence simplifies significantly the formalisation, and on the other hand to implement examples that are useful for proving properties of functional programs.

Prerequisites: Familiarity with Agda and type theory or having taken the course DAT350/DIT233 Types for programs and proofs.The project is suitable for 1 or 2 students.

Contact: Thierry Coquand

Date range: 
October, 2020 to October, 2024