I am a postdoc at the Functional Programming Laboratory of the University of Nottingham, working on type theory and category theory.
My PhD thesis.
Semantics for certain classes of higher inductive definitions in 0-truncated Homotopy Type Theory.
My paper for the FP Lab Away Day 2014. An internalisation of the syntax of mutual and higher inductive types in 0-truncated Homotopy Type Theory.
My first year report: an introduction to fibrational models of type theory.
An implementation of basic category theory in Agda/HoTT.
Base library for homotopy type theory in Agda.
A Haskell library for parsing command line options using Applicative functors.