I am a postdoc at the Functional Programming Laboratory of the University of Nottingham, working on type theory and category theory.
My PhD thesis.
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.