## 2016

**Logic Colloquium 2016.***The real projective spaces in HoTT.*Joint work with Ulrik Buchholtz. Leeds, August 4th 2016.**W****orkshop on Categorical Logic and Univalent Foundations.***Principal equivalence relations.*Leeds, August 27th 2016.**Workshop on Homotopy Type Theory / Univalent Foundations.***Classifying types and the join construction.*Partly joint work with Ulrik Buchholtz. Porto, July 25th 2016.**Mathematics = Algorithms + Proofs.**Localization at ω-compact types, as sequential colimits. Joint work with Floris van Doorn. Luminy, January 11th-15th 2016.

## 2015

**MURI meeting.**Forms of type theoretical descent. Pittsburgh, March 27th-29th 2015.

## 2014

**Homotopy Type Theory Workshop.***An algebraic formulation of dependent type theory.*Oxford, November 7th-10th 2014.

## 2013

**Conference on type theory, homotopy theory and univalent foundations.**A descent theorem in type theory. Joint work with Bas Spitters. Barcelona, September 26th 2013.