Paolo Capriotti's blog

Functional programming and more

About me

I am a PhD student at the Functional Programming Laboratory of the University of Nottingham, working on homotopy type theory, functional programming and language design.


Free Applicative Functors

With Ambrus Kaposi, MSFP 2014.
Previous version, submitted to ICFP 2013.

Recent work

Mutual and Higher Inductive Types in 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.

Inheritance and overloading in Agda

My paper for the FP Lab Away Day 2013 (slides). An exposition of the techniques I used in the implementation of my category theory library in Agda.

Type theory through comprehension categories

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.


@pcapriotti on GitHub

View Paolo Capriotti's profile on LinkedIn