Title: ***Paranatural Category Theory*** 

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 ℂop × ℂ → 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.