First year PhD review report
Investigating Quotient Inductive-Inductive Types, July 2022.
Internal examiner: Prof. Graham Hutton.
Master's thesis
Constructing Simple and Mutual Inductive Types, University of Nottingham, September 2020.
Supervisor: Prof. Thorsten Altenkirch.
Formalisation in Agda can be found here.