This book will be a textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

Lecture material for DeepSpec Summer School 2018

joke page until I decide what to do with this domain name

Examples of divide-and-conquer recursion in Coq, based on our POPL 2023 paper "A Type-Based Approach to Divide-and-Conquer Recursion in Coq"

A Logical Relation for Martin-Löf Type Theory in Agda

Accompanying formalisation for the paper "Type theory in type theory using a strictified syntax"