Parametricity via Cohesion

TL;DR

This paper addresses the challenge of internalizing parametricity in dependent type theories by proposing a synthetic, cohesion-based framework. It develops a categorical semantics built on cohesion, formulates a computable axiom system with path and graph types, and implements these ideas in Agda to verify parametricity theorems. The approach yields practical results, such as deriving induction principles for $\mathbb{N}$ and $S^1$ from recursors and demonstrating the management of higher-dimensional coherence via parametricity. By connecting parametricity to gluing, coherence, and the internal language of cohesive $\infty$-topoi, the work aims to unify disparate internal parametricity approaches and illuminate broader applications from homotopy theory to modular program analysis.

Abstract

Parametricity is a key metatheoretic property of type systems, which implies strong uniformity & modularity properties of the structure of types within systems possessing it. In recent years, various systems of dependent type theory have emerged with the aim of expressing such parametric reasoning in their internal logic, toward the end of solving various problems arising from the complexity of higher-dimensional coherence conditions in type theory. This paper presents a first step toward the unification, simplification, and extension of these various methods for internalizing parametricity. Specifically, I argue that there is an essentially modal aspect of parametricity, which is intimately connected with the category-theoretic concept of cohesion. On this basis, I describe a general categorical semantics for modal parametricity, develop a corresponding framework of axioms (with computational interpretations) in dependent type theory that can be used to internally represent and reason about such parametricity, and show this in practice by implementing these axioms in Agda and using them to verify parametricity theorems therein. I then demonstrate the utility of these axioms in managing the complexity of higher-dimensional coherence by deriving induction principles for higher inductive types, and in closing, I sketch the outlines of a more general synthetic theory of parametricity, with applications in domains ranging from homotopy type theory to the analysis of program modules.