Errata

This page collects any errors I find in existing/already published papers.

Section 5.3 states that in general type equivalence relative to a collection of type equality hypotheses is undecidable. This is incorrect; it appears to be decidable using unification and congruence closure techniques. (Thanks to Andrew Kennedy for pointing this mistake out.)

In section 6, there is a missing elaboration rule $\Delta,\true \to \Delta$.
In Theorem 10, parts 2 and 3 are misstated: the right-hand judgments should be the same as the left hand ones, except with $D'$ or $\Delta'$ instead of $D$ or $\Delta$.