Paolo Capriotti's blog

Functional programming and more

About me

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


Extending Homotopy Type Theory with Strict Equality

With Thorsten Altenkirch and Nicolai Kraus.
To appear at CSL 2016

Functions out of Higher Truncations

With Nicolai Kraus and Andrea Vezzosi.
Proceedings of CSL 2015.

Non-Wellfounded Trees in Homotopy Type Theory

With Benedikt Ahrens and Régis Spadotti.
Proceedings of TLCA 2015, LIPIcs Vol. 38, pp. 17-30.
Project webpage.

Free Applicative Functors

With Ambrus Kaposi, proceedings of 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