Canonicity and normalisation for Dependent Type Theory

TL;DR

This paper proves canonicity and normalization for a dependent type theory with universes and booleans, using a proof-relevant reducibility approach rooted in classical logic interpretations.

Contribution

It introduces a novel proof-relevant reducibility method to establish fundamental properties of dependent type theory with cumulative universes.

Findings

Proves canonicity for the type theory.

Establishes normalization for the type theory.

Uses proof-relevant reducibility inspired by Godel and Tait.

Abstract

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.