Synthetic Tait Computability the Hard Way

TL;DR

This paper explores various proofs of canonicity and normalization in type theory, re-expressing them through category theory, and introduces synthetic Tait computability and a synthetic proof of parametricity for system F.

Contribution

It provides a comparative analysis of proofs of canonicity and normalization using category theory and introduces synthetic Tait computability and parametricity proofs.

Findings

Different proofs of canonicity and normalization are dissected and compared.

Synthetic Tait computability framework is proposed and explained.

A synthetic proof of parametricity for system F is presented.

Abstract

We walk through a few proofs of canonicity and normalization, each one with more aspects dissected and re-expressed in category theory, so that readers can compare the difference across proofs. During this process we isolate the different ideas that make up the proofs. Finally we arrive at synthetic Tait computability as proposed by J. Sterling. We also give a synthetic proof for parametricity of system F.