Paranatural Category Theory

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi non lectus volutpat, posuere mauris quis, tristique elit. Morbi faucibus ipsum urna, eget sollicitudin ipsum sagittis eu. Integer gravida mauris ac purus facilisis, vitae dapibus ex mattis. Nulla eget interdum ipsum. Donec tempor augue luctus nisi consectetur sodales. Aliquam semper rutrum nisi eget congue. Mauris ac tellus id turpis tempus euismod et eget velit.

Preprints

Paranatural Category Theory

A framework for polymorphism, (co)induction, and more — preprint, arXiv:2307.09289, 18 July 2023

arXiv page

pdf

Theory of Paranatural Transformations

Parametricity and Paranaturality

Structural (Co)End Calculus

Difunctor Models of Type Theory

Talks

TYPES 2024

Updates on Paranatural Category Theory

— at the 30th International Conference on Types for Proofs and Programs (TYPES 2024), 11 June 2024, Copenhagen, Denmark

Abstract

Slides

Octoberfest

Paranatural Category Theory

— at the Category Theory Octoberfest, 28 October 2023, online

Slides

Video

Abstract:

In this talk, I’ll describe my work towards carving out a (novel?) branch of category theory, dubbed paranatural category theory. The central objects of study in paranatural CT are paranatural transformations (known in the literature as strong dinatural, or Barr dinatural, transformations), which are a kind of transformation between difunctors (functors of the form C^op × C → Set), intermediate between the standard category-theoretic notions of dinatural transformations and natural transformations. I’ll detail the basic theory of paranatural transformations and a di-variant analogue of presheaf toposes, including a lovely "diYoneda Lemma" and an accompanying calculus of structural (co)ends. I’ll also pose the (still open) question of whether these constructions can be viewed as instances of the usual theory of natural transformations. Time permitting, I will explore some of the exciting applications of this theory: a category-theoretic treatment of parametrically-polymorphic functional programming, impredicative encodings of (co)inductive types, representation independence of abstract data structures, and difunctor models of dependent type theory.

A preprint covering this material is available on the arXiv at arxiv.org/abs/2307.09289.

CMU HoTT Seminar

Paranatural Category Theory

— at the Carnegie Mellon University HoTT Seminar, 22 September 2023, Pittsburgh, Pennsylvania, USA

Slides

Abstract:

What is the appropriate notion of transformation between "difunctors", that is, functors C^op × C → Set? In this talk, we'll examine several applications in the semantics/metatheory of functional programming and type theory where we find ourselves in a "Goldilocks"-type situation: the usual notion of natural transformation is too narrow (excluding the examples we're interested in) and standard notions of 'diagonal natural transforms' are too broad (so broad, indeed, that they fail to be closed under composition). I'll talk about the notion which I think is 'just right': strong dinatural transformations. Strong dinatural transformations (which I advocate for rechristening as 'paranatural transformations') are a concept neglected in the present literature, I claim, and one which can serve as the centerpiece of a striking and widely-useful mathematical theory (which I dub 'paranatural category theory'). I hope to bring attention to some of the basic results in this fascinating branch of category theory, and instigate further research into it.

A preprint covering this material is available on the arXiv at arxiv.org/abs/2307.09289.

PARANATURAL

research by Jacob Neumann

Paranatural Category Theory

Preprints