Canonicity and normalisation for Dependent Type Theory

10/22/2018

∙

by   Thierry Coquand, et al.

∙

0

∙

share

We show canonicity and normalization for dependent type theory with a cumulative sequence of universes and a type of Boolean. The argument follows the usual notion of reducibility, going back to Godel's Dialectica interpretation and the work of Tait. A key feature of our approach is the use of a proof relevant notion of reducibility.