Paranatural Category Theory

TL;DR

This paper introduces paranatural category theory, a new branch centered on paranatural transformations, which generalize natural transformations while maintaining composability, enabling advances in parametric polymorphism and type theory modeling.

Contribution

It defines the category of difunctors and paranatural transformations, proves a diYoneda Lemma, and demonstrates applications in parametric polymorphism, (co)inductive types, and type theory models.

Findings

Paranatural transformations precisely capture parametricity.

The diYoneda Lemma provides a new framework for reasoning about (co)algebras.

Paranatural category theory offers novel tools for type theory modeling.

Abstract

We establish and advocate for a novel branch of category theory, centered around strong dinatural transformations (herein known as "paranatural transformations"). Paranatural transformations generalize natural transformations to mixed-variant difunctors, but, unlike other such generalizations, are composable and exceptionally well-behaved. We define the category of difunctors and paranatural transformations, prove a novel "diYoneda Lemma" for this category, and explore some of the category-theoretic implications. We also develop three compelling uses for paranatural category theory: parametric polymorphism, impredicative encodings of (co)inductive types, and difunctor models of type theory. Paranatural transformations capture the essence of parametricity, with their "paranaturality condition" coinciding exactly with the "free theorem" of the corresponding polymorphic type; the paranatural analogue of the (co)end calculus provides an elegant and general framework for reasoning about initial algebras, terminal coalgebras, bisimulations, and representation independence; and "diYoneda reasoning" facilitates the lifting of Grothendieck universes into difunctor models of type theory. We develop these topics and propose further avenues of research.