Peter LeFanu Lumsdaine

general-type-theories. A (formalised) general definition of type theories

palmgren-archive. Research material of Erik Palmgren (1963–2019)

cartmell-thesis. HoTT group project to TeXify Cartmell's PhD thesis “Generalised Algebraic Theories and Contextual Categories”

Oberwolfach-explorations. collaboration on work in progress

hott-limits. A formalization of (homotopy) limits in Homotopy Type Theory

higher-inductive-paper. Paper in progress

Homotopy. Homotopy theory in Coq.

UniMath2017-CategoryTheory. Category theory group projects at UniMath workshop, Birmingham, Dec 2017

HoTT. Homotopy type theory

pllthesis. Fossil record of the growth of my thesis.