Canonicity and Computability in Homotopy Type Theory
arXiv:2308.09621
Abstract
This dissertation gives an overview of Martin Lof's dependant type theory, focusing on its computational content and addressing a question of possibility of fully canonical and computable semantic presentation.
arXiv commentDissertation submitted in partial fulfillment of a requirement for the degree of Master in Mathematics and Computer Science at University of Oxford