Doctoral Dissertation, Carnegie Mellon University
September 13, 2021
A significant mathematical error in this dissertation was discovered by Thierry Coquand and Daniel Gratzer in April 2022 in my adaptation of Sterling and Angiuli's normalization proof for cubical type theory to support universes: the computability and normalization structures for stabilized neutral types were ill-defined, and (relatedly) the definition of the normal forms for neutral types was incorrect.
The root of the error was that the normalization struture for a stabilized neutral type did not extend its stabilization data as required. A corrected account for type theory without Kan operations was proposed by Coquand and Gratzer, and it posed no difficulties to apply this solution to full cubical type theory. The current version of this dissertation contains the needful corrections which suffice to fully recover the claimed results.
My sincere thanks to Thierry and Daniel.
Journal of the ACM
After going to press, we have fixed the following mistakes:
The local copy linked here has the corrections implemented.