Paper
Paranatural Category Theory
Authors
Jacob Neumann
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.
Parse Issues: 14 warnings, 1 error