# About me

I am a Senior Haskell Developer at Wire.

Until February 2021, I was a postdoc at the Logic Group in TU Darmstadt, working on homotopy type theory and category theory. Previously, I was a postdoc at the University of Nottingham, where I also got my PhD under the supervision of Venanzio Capretta.

## Publications

#### Two-Level Type Theory and Applications [bibtex]

With Danil Annenkov, Nicolai Kraus and Christian Sattler.

Published in MSCS.

Formalisation.

#### Higher lenses [bibtex]

With Nils Anders Danielsson and Andrea Vezzosi. Proceedings of LICS 2021.

#### Quotient inductive-inductive types [bibtex]

With Thorsten Altenkirch, Gabe Dijkstra, Nicolai Kraus and Fredrik Nordvall Forsberg.

Proceedings of FoSSaCS 2018.

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

#### Univalent higher categories via complete semi-Segal types [bibtex]

With Nicolai Kraus.

Proceedings of POPL 2018.

Formalisation.

#### Models of type theory with strict equality [bibtex]

My PhD thesis.

#### Extending Homotopy Type Theory with strict equality [bibtex]

With Thorsten Altenkirch and Nicolai Kraus.

Proceedings of CSL 2016

#### Functions out of higher truncations [bibtex]

With Nicolai Kraus and Andrea Vezzosi.

Proceedings of CSL 2015.

#### Non-wellfounded trees in Homotopy Type Theory [bibtex]

With Benedikt Ahrens and Régis Spadotti.

Proceedings of TLCA 2015, LIPIcs Vol. 38, pp. 17-30.

Project webpage.

#### Free applicative functors [bibtex]

With Ambrus Kaposi.

Proceedings of MSFP 2014.

Previous version, submitted to ICFP 2013.

## Recent work

#### Lecture notes on topology

Lecture notes for an introductory topology course given at TU Darmstadt in the Summer semester of 2019.

#### Lecture notes on semantics of type theory

An introduction to models of type theory and the construction of the simplicial model, based on a course given at TU Darmstadt in the Summer semester of 2020.

#### 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.

## Projects

#### agda-categories

An implementation of basic category theory in Agda/HoTT.

#### agda-base

Base library for homotopy type theory in Agda.

#### optparse-applicative

A Haskell library for parsing command line options using Applicative functors.

## Contact

@pcapriotti on GitLab

@pcapriotti on GitHub

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