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.
Proceedings of 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

Quotient inductive-inductive types

Semantics for certain classes of higher inductive definitions in 0-truncated Homotopy Type Theory.

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 GitLab

@pcapriotti on GitHub

PGP key fingerprint: C12C 69A6 008E 2DEF AED7 AC6D 6D6C 5D72 34BA 1BC2