# About me

I am a postdoc at the Functional Programming Laboratory of the University of Nottingham, working on type theory and category theory.

### Publications

#### Univalent Higher Categories via Complete Semi-Segal Types

With Nicolai Kraus.

Formalisation.

#### Two-Level Type Theory and Applications

With Danil Annenkov and Nicolai Kraus.

Formalisation.

#### Models of Type Theory with Strict Equality

My PhD thesis.

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

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