# Paranatural Category Theory

A framework for polymorphism, (co)induction, and more

Jacob Neumann  0009-0003-5858-466X School of Computer ScienceUniversity of
NottinghamUnited Kingdom<EMAIL_ADDRESS>
###### 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.

category theory, Yoneda Lemma, parametricity, inductive types, coinductive
types, semantics of type theory

††journal: PACMPL††journalvolume: 0††article: 0††journalyear:
0††publicationmonth: 0††copyright: none

##  1\. Introduction

###  1.1. Background

One of the key selling points of functional programming is its proximity to
mathematical practice. A functional programmer does not conceive of functions
as sets of instructions and state changes to be inflicted upon a machine of
registers and bits and pointers, but, like the mathematician does, as a
transformation of data, a mapping of one kind of thing to another. By adopting
a mathematical view of programming, us evangelists will claim, we inherit the
wealth of mathematical tools for reasoning about our programming: inductively-
structured data is governed by inductive reasoning; constructs inspired by
category theory can be reasoned about using category theory; and so on. And,
indeed, the history of functional programming and type theory witnesses a kind
of convergence to pure logic and mathematics: from the genius insight of the
Curry-Howard Isomorphism, to the emergence of interactive theorem proving, to
the development of a type-theoretic foundation for mathematics.

However, there is a curious point—deep in functional programming’s heart—where
it diverges from mathematics. It has been clear for well over a century that,
in both the foundation and practice of mathematics, structure-preserving
functions must play a central role. The idea of studying topology without
continuous functions or algebra without homomorphisms is inconceivable. That
mathematics essentially consists of things and structure-preserving maps
between them serves as category theory’s fundamental premise, and seems
unlikely to be disavowed any time soon. But this centrality of functions is,
ironically, the point which functional programming research casts aside,
specifically in the articulation of parametricity. As Reynolds writes in his
landmark paper Types, Abstraction and Parametric Polymorphism (Reynolds,
1983), the way out of this impasse is to generalize homomorphisms from
functions to relations. In the study of parametricity, it is structure-
preserving relations which play the central role.

To understand the impasse Reynolds refers to, it is worth reiterating the
summary by (Hermida et al., 2014) of the intuitive affinity between parametric
polymorphism and the category-theoretic notion of naturality. The goal of
parametric polymorphism is to have polymorphic terms in our programming
language, i.e. ones which can assume different types, but to do so in a
principled, regular way. As Reynolds explains, a parametric polymorphic
function is one that behaves the same way for all types. A polymorphic
function which behaves differently based on the type it assumes is ad hoc
polymorphic, not parametric (Strachey, 2000). The basic task of parametricity
is making precise what behaving the same way means.

In the world of category theory, a natural transformation between two functors
is defined by a class of maps, which must be given simultaneously for every
object of the relevant category. More precisely, these maps are subject to a
naturality condition ensuring that the choice of maps is appropriately
uniform, and not the result of arbitrary choices. As Hermida et al. observe,
the pre-theoretic intuitions expressed by the pioneers of category theory and
those of programming language theory match up essentially word for word:
‘artificial choices’ corresponds to ‘ad hoc polymorphism;’ ‘given
simultaneously’ corresponds ‘work on all types’ and ‘behave the same way;’ and
‘natural’ corresponds to ‘parametric polymorphism.’ So, one might expect to
have a single mathematical theory that captures the intuitions expressed in
both the contexts.

Why isn’t there such a mathematical theory? Indeed, we have the beginnings of
one: for instance, a polymorphic term of type
$\textsf{List}\;\alpha\to\textsf{List}\;\alpha$ (where $\alpha$ is the type
parameter) is precisely a natural transformation from the List functor to
itself: naturality is exactly the free theorem, à la (Wadler, 1989). So, in
some cases, parametricity is naturality. The issue arises when dealing with
mixed-variant operators like $\to$, which is contravariant in one argument and
covariant in the other. It is not a functor, but a difunctor.111This notion is
often called a profunctor, but here we reserve that term for functors of the
form $\mathbb{C}^{\text{op}}\times\mathbb{D}\to\textsf{Set}$, i.e. difunctors
whose positive and negative arguments can come from different categories. So
the notion of natural transformation (which is defined only between two
covariant functors or between two contravariant functors) must be generalized
to difunctors. At this point, several works (Scott, 2000; Hermida et al.,
2014; Bainbridge et al., 1990) all rehearse the same story: the most obvious
notion of a dinatural transformation (Dubuc and Street, 1970) is not closed
under composition, and therefore not suitable as a solution. Bainbridge et al.
do carve out a class of composable dinatural transformations—realizable
dinaturals—but otherwise the failure of dinatural transformations to compose
is taken as justification to abandon the category-theoretic pursuit.
Consequently, Reynolds’s approach, based on relations rather than functions,
is followed.

The present author views this as a false impasse. Certainly, the above-
mentioned notion of dinatural transformation is not suited for the task, in
part because of its lack of composability but, more seriously, because
dinaturality doesn’t match parametricity anyways (Paré and Román, 1998, 2.2).
However, this doesn’t at all indicate that there isn’t some generalization of
natural transformations to difunctors which is composable and which does
appropriately capture parametricity. Indeed, our claim is that such a notion
has indeed been identified: strong dinatural transformations.

Strong dinatural transformations first appeared in (Mulry, 1992), though they
appear to have been independently invented as Barr dinatural transformations
in (Paré and Román, 1998). The latter work represents the most systematic
development of strong dinaturality, including a development of the natural
numbers as strong dinaturals (partially repeated here as Example 4.2) and some
generalization to abstract categories. A connection between strong
dinaturality and parametricity was first suggested in (Eppendahl, 1999) and
(Vene, 2006). Some more recent work in this vein includes (Hackett and Hutton,
2015), though no definitive statement on the relationship between
parametricity and strong dinaturality is made there. Another noteworthy aspect
of the strong dinaturality literature are the rich connections to initial
algebras and fixpoint operators, such as in the work of (Uustalu, 2010, 2000).

###  1.2. Contribution

However, development of the category theory surrounding strong dinatural
transformations has been lacking. For instance, there has not been (to the
author’s knowledge) a systematic account of the category of difunctors and
strong dinatural transformations, despite it being known for thirty years now
that strong dinaturals compose. The primary aim of the present work is to
remedy this situation. To emphasize their correlation to parametricity and
their status as a fundamental category-theoretic concept in their own right
(and not a mere variation on dinatural transformations),222And because the
double-adjective name occasionally proves annoying we will throughout be
referring to strong dinatural transformations as paranatural transformations,
and the study centered around them as paranatural category theory. With the
present work, we aim to establish some core results of paranatural category
theory, which hopefully will serve as a base for future exploration.

Additionally, our goal is to present some ideas of what paranatural category
theory is for. We outline three applications. First, as indicated above,
parametric polymorphism is a key motivation. Though we refrain (for now) from
pronouncing that parametricity is paranaturality, the examples we explore here
will indicate that, at least in the most important cases, these ideas do seem
to coincide. We take one step towards a systematic connection between
parametricity and paranaturality, by outlining a paranaturality-based
procedure for calculating Wadler’s free theorems. Our second application of
paranatural category theory will be the development of a calculus for Church
encodings of (co)inductive types, combining the work of (Awodey et al., 2018)
and (Uustalu, 2010). And, finally, we apply the tools of paranatural category
theory towards defining a new class of categorical models of type theory,
leveraging a deep analogy between presheaf categories and our new category of
difunctors and paranatural transformations.

###  1.3. Overview

In Section 2 the basics of paranatural category theory are laid out, including
a Yoneda Lemma for difunctors which, to the author’s knowledge, is entirely
novel. In Section 3, the connection between paranaturality and relational
parametricity is made more explicit, and the method for calculating free
theorems is described. In Section 4, the connection between paranaturality and
encodings of (co)inductive types is detailed; a special case of this
construction forms the backbone of (Awodey et al., 2018), but otherwise this
theory has only appeared in talks (Uustalu, 2010; Neumann, 2022). Finally, in
Section 5, we develop a different application of the tools of paranaturality:
defining a difunctor model of dependent type theory analogous to the presheaf
model (Hofmann, 1997), complete with a universe type obtained via our
difunctor Yoneda Lemma (analogously to (Hofmann and Streicher, 1999)). The
hope is that this model will prove useful for defining directed/parametric
variants of homotopy type theory, though its precise properties are still the
topic of ongoing investigation. We conclude by enumerating some possible
avenues of further research.

##  2\. Paranaturality

We begin by establishing paranatural category theory. Throughout, we adopt an
informal dependent type theory as our metatheory, e.g. writing $x:X$ instead
of $x\in X$ to indicate that $x$ is an element of the set $X$. Our notation
will generally match that of (Univalent Foundations Program, 2013), though we
don’t make use of the more elaborate features of that text, like univalence or
higher inductive types. Our main motivation for using a type-theoretic
metatheory is to facilitate a future formalization of this work in a typed
computer proof assistant. Throughout, we use $\equiv$ to denote judgmental or
definitional equality and $=$ to denote identity types, that is, propositional
equality. We use the notations

$(x:A)\to B(x)\quad\quad\text{and}\quad\quad\sum_{x:A}B(x)$

for the dependent product and dependent sum types, and assume function
extensionality. We’ll occasionally use lambda-expressions to define functions,
e.g. $(\lambda(x:X)\to x)\colon X\to X$ for the identity on $X$. When defining
dependent functions of many arguments, we will often omit implicit arguments
which are clear from context. Additionally, for dependent sums
$\sum_{x:A}B(x)$ where $B(x)$ is a proposition (e.g. an equality of elements
of a set), we will often omit the second component when writing elements of
the type, e.g. $\textsf{id}_{X}\colon\sum_{g:X\to X}g\circ g=g$ where $X$ is
some set. We will not make any systematic distinction between curried and
uncurried multivariable functions, writing the arguments separated by spaces
or as a tuple, whichever is more convenient.

Our presentation of category theory is relatively standard. A category
$\mathbb{C}$ will consist of a type of objects, denoted
$\left|\mathbb{C}\right|$; hom-sets, denoted $\textsf{Hom}_{\mathbb{C}}(I,J)$
or just $\textsf{Hom}(I,J)$, for every $I,J\colon\left|\mathbb{C}\right|$;
identity morphisms denoted $\textsf{id}_{I}$; and composition denoted $\circ$
(written in the traditional order, i.e. $g\circ f$ for $f$ followed by $g$),
with the usual associativity and unit laws. The category Set of sets and
functions will be our canonical example of a category, which we will
complement with further examples.

###  2.1. Difunctors and Dinaturality

An essential notion for us will be that of a difunctor.

###### Definition 2.1.

For a given category $\mathbb{C}$, a difunctor $\Gamma$ on $\mathbb{C}$,
denoted $\Gamma\colon\mathbb{C}^{\text{op}}\times\mathbb{C}\to\textsf{Set}$
consists of a function, the object part:

$\Gamma\colon\left|\mathbb{C}\right|\to\left|\mathbb{C}\right|\to\left|\textsf{Set}\right|$

along with two morphism parts:

$\displaystyle\textsf{map}^{-}_{\Gamma}$
$\displaystyle\colon\textsf{Hom}(I_{0},I_{1})\to\Gamma(I_{1},J)\to\Gamma(I_{0},J)$
$\displaystyle\textsf{map}^{+}_{\Gamma}$
$\displaystyle\colon\textsf{Hom}(J_{0},J_{1})\to\Gamma(I,J_{0})\to\Gamma(I,J_{1})$

subject to functoriality laws:

$\displaystyle(\textsf{map}^{-}_{\Gamma}\;i_{2})\circ(\textsf{map}^{+}_{\Gamma}\;j_{2})$
$\displaystyle=(\textsf{map}^{+}_{\Gamma}\;j_{2})\circ(\textsf{map}^{-}_{\Gamma}\;i_{2})$
$\displaystyle\textsf{map}^{-}_{\Gamma}\;\textsf{id}=\textsf{id}\qquad\qquad$
$\displaystyle\qquad\qquad\textsf{map}^{+}_{\Gamma}\;\textsf{id}=\textsf{id}$
$\displaystyle\textsf{map}^{-}_{\Gamma}(k\circ
j)=(\textsf{map}^{-}_{\Gamma}\;j)\circ(\textsf{map}^{-}_{\Gamma}\;k)\quad$
$\displaystyle\quad\textsf{map}^{+}_{\Gamma}(i\circ
h)=(\textsf{map}^{+}_{\Gamma}\;i)\circ(\textsf{map}^{+}_{\Gamma}\;h).$

Throughout, we’ll refer to the first argument to a difunctor as its negative
or contravariant argument, and the second argument as positive or covariant.

Difunctors can, of course, be defined to have a codomain category besides Set.
They can also be generalized to the fruitful notion of a profunctor, whose
positive and negative argument can come from different categories. But, for
us, this definition of (set-valued) difunctors will be the correct level of
generality. The canonical example of such a difunctor is the hom-set operation
itself:

###### Example 2.2.

The hom difunctor sends objects $I,J$ to the hom-set $\textsf{Hom}(I,J)$ and
has morphism parts given by pre- and post-composition: for
$i_{2}\colon\textsf{Hom}(I_{0},I_{1})$ and
$j_{2}\colon\textsf{Hom}(J_{0},J_{1})$,

$\displaystyle\textsf{map}^{-}_{\textsf{Hom}}\;i_{2}$
$\displaystyle:\equiv\lambda x\to x\circ i_{2}\qquad$
$\displaystyle\colon\textsf{Hom}(I_{1},J)\to\textsf{Hom}(I_{0},J)$
$\displaystyle\textsf{map}^{+}_{\textsf{Hom}}\;j_{2}$
$\displaystyle:\equiv\lambda y\to j_{2}\circ y$
$\displaystyle\colon\textsf{Hom}(I,J_{0})\to\textsf{Hom}(I,J_{1})$

A difunctor which completely ignores its negative argument is known as a
covariant set-valued functor $\mathbb{C}\to\textsf{Set}$, and a difunctor
which ignores its positive argument is acontravariant set-valued functor
$\mathbb{C}^{\text{op}}\to\textsf{Set}$, commonly known as a presheaf. As
discussed in the introduction, our first concern is generalizing the well-
known notion of a natural transformation, which can be defined between two
covariant functors or between two presheaves, to difunctors. The correct such
notion is that of a paranatural transformation.

###### Definition 2.3.

Given difunctors
$\Delta,\Gamma\colon\mathbb{C}^{\text{op}}\times\mathbb{C}\to\textsf{Set}$, a
family of maps

${\Delta(I,I)}$${\Gamma(I,I)}$$\scriptstyle{\phi_{I}}$

indexed over objects $I\colon\left|\mathbb{C}\right|$ is a paranatural
transformation, denoted $\phi\colon\Delta\xrightarrow{\diamond}\Gamma$, if,
for all $i_{2}\colon\textsf{Hom}_{\mathbb{C}}(I_{0},I_{1})$ and all
$d_{0}\colon\Delta(I_{0},I_{0})$, $d_{1}\colon\Delta(I_{1},I_{1})$,

$\textsf{map}^{+}_{\Delta}\;i_{2}\;d_{0}=\textsf{map}^{-}_{\Delta}\;i_{2}\;d_{1}\quad\quad\text{implies}\quad\quad\textsf{map}^{+}_{\Gamma}\;i_{2}\;(\phi_{I_{0}}\;d_{0})=\textsf{map}^{-}_{\Gamma}\;i_{2}\;(\phi_{I_{1}}\;d_{1}).$

Diagrammatically: if the diamond commutes, so too does the hexagon.

(1)
${\Delta(I_{0},I_{0})}$${\Gamma(I_{0},I_{0})}$${\mathbf{1}}$${\Delta(I_{0},I_{1})}$${\Gamma(I_{0},I_{1})}$${\Delta(I_{1},I_{1})}$${\Gamma(I_{1},I_{1})}$$\scriptstyle{\phi_{I_{0}}}$$\scriptstyle{\textsf{map}^{+}_{\Delta}\;i_{2}}$$\scriptstyle{\textsf{map}^{+}_{\Gamma}\;i_{2}}$$\scriptstyle{d_{0}}$$\scriptstyle{d_{1}}$$\scriptstyle{\phi_{I_{1}}}$$\scriptstyle{\textsf{map}^{-}_{\Delta}\;i_{2}}$$\scriptstyle{\textsf{map}^{-}_{\Gamma}\;i_{2}}$

As desired, when we instantiate this definition with $\Delta,\Gamma$ both
covariant functors or both presheaves, we get the standard notion of a natural
transform. For instance, if
$\Gamma,\Delta:\mathbb{C}^{\text{op}}\to\textsf{Set}$ then the
$\textsf{map}^{+}$ edges of Equation 1 are just the respective identity
functions, and we get this: if the triangle commutes, then so too does the
outer pentagon.

(2)
${1}$${\Delta(I_{0})}$${\Gamma(I_{0})}$${\Delta(I_{1})}$${\Gamma(I_{1})}$$\scriptstyle{d_{0}}$$\scriptstyle{d_{1}}$$\scriptstyle{\phi_{I_{0}}}$$\scriptstyle{\textsf{map}^{-}_{\Delta}\;i_{2}}$$\scriptstyle{\phi_{I_{1}}}$$\scriptstyle{\textsf{map}^{-}_{\Gamma}\;i_{2}}$

This is the same as saying that
$(\textsf{map}^{-}_{\Gamma}\;i_{2})\circ\phi_{I_{1}}=\phi_{I_{0}}\circ(\textsf{map}^{+}_{\Delta}\;i_{2})$
for every $i_{2}\colon\textsf{Hom}(I_{0},I_{1})$, which is the usual condition
that defines $\phi$ as a natural transformation from $\Delta$ to $\Gamma$.
Likewise if $\Delta$ and $\Gamma$ are just covariant. So this is indeed a
generalization of natural transformation to difunctors. Moreover, the
paranaturality condition (Equation 1) is the correct generalization for
parametricity. The following instance, originally formulated in the relational
parametricity setting by (Wadler, 1989), will serve as our paradigm example.

###### Example 2.4.

The presheaf of boolean-valued comparison functions has an object part that
sends a set $X$ to the set of functions $X\times X\to\mathbf{2}$, and a
morphism part given by precomposition.

The difunctor of list rearrangement sends a set $X$ to the set
$\textsf{List}\;X\to\textsf{List}\;X$, with the morphism parts given by pre-
and post-composition using the morphism part of the List functor.333I.e.
$\textsf{map}^{-}\;f\colon(\textsf{List}\;Y\to\;\textsf{List}Z)\to(\textsf{List}\;X\to\textsf{List}\;Z)$
for some $f\colon X\to Y$ is given by precomposition with
$\textsf{map}_{\textsf{List}}\;f\colon\textsf{List}\;X\to\textsf{List}\;Y$.

A paranatural transformation from the boolean-valued comparison presheaf to
the difunctor of list rearrangements is a family of operations

$s_{X}\colon(X\times X\to\mathbf{2})\to\textsf{List}\;X\to\textsf{List}\;X$

for each set $X$, which is parametrically polymorphic in $X$: if
$\prec_{X}\colon X\times X\to\mathbf{2}$ and $\prec_{Y}\colon Y\times
Y\to\mathbf{2}$ are comparison functions and $f\colon X\to Y$ is monotone in
the sense that

for all $x,x^{\prime}:X$ $\displaystyle(x\prec_{X}x^{\prime})\quad$
$\displaystyle=\quad(f(x)\prec_{Y}f(x^{\prime}))$

then, given some $L\colon\textsf{List}\;X$, it makes no difference whether one
applies $s_{X}$ to $L$ and then list-maps $f$ over the result, or does the
list-map first and then applies $s_{Y}$:

$(\textsf{map}_{\textsf{List}}\;f)\circ
s_{X}=s_{Y}\circ(\textsf{map}_{\textsf{List}}\;f).$

The main example of such a family of functions $s$ is a sorting function
which, for any type whatsoever, takes a comparison function on that type and a
list of values of that type, and sorts the list according to the comparison
function.

This example still does not take advantage of the full generality of
paranaturality, as the domain difunctor is just a presheaf. But it does show
how paranaturality manages to encode the essential idea of parametric
polymorphism: making the parametric type variable a black box which the
polymorphic function is not able to inspect. The only thing a polymorphic
function

$s\colon(\alpha\times\alpha\to\mathbf{2})\to\textsf{List}\;\alpha\to\textsf{List}\;\alpha$

should know about the type is the provided comparison function. Therefore, it
should not be able to notice if we pre-map by a monotone function. This is
what it means for a polymorphic function of this type to do the same thing for
every type $\alpha$, i.e. to be parametrically polymorphic; paranaturality
gets it right.

###  2.2. Paranatural Category Theory

Famously, the dinatural transformations of (Dubuc and Street, 1970) do not
compose: given a dinatural transformation from $\Delta$ to $\Gamma$ and one
from $\Gamma$ to $\Theta$, there is not, in general, a way to define one from
$\Delta$ to $\Theta$ that serves as their composite. As mentioned, this fact
is the generally-cited reason to abandon purely function-based approaches to
parametricity and stick to logical relations. From a category-theoretic
perspective, not being composable severely limits the usefulness of dinatural
transformations, in particular making it impossible to form a category of
difunctors and dinatural transformations, let alone try and replicate some of
the amazing structure of the category of presheaves. So, if paranatural
transformations are to be worth much, they must at least compose. Thankfully,
they clear this bar easily.

###### Proposition 2.5.

If $\gamma:\Delta\xrightarrow{\diamond}\Gamma$ and
$\theta\colon\Gamma\xrightarrow{\diamond}\Theta$, then their pointwise-defined
composite

$(\theta\gamma)_{I}:\equiv\theta_{I}\circ\gamma_{I}\quad\colon\Delta(I,I)\to\Theta(I,I)$

is a paranatural transformation $\Delta\xrightarrow{\diamond}\Theta$.

Intuitively, the naturality squares of a natural transformation are replaced
by paranaturality chevrons. This fragment of Equation 1

(3)
${\Delta(I_{0},I_{0})}$${\Gamma(I_{0},I_{0})}$${\Delta(I_{0},I_{1})}$${\Gamma(I_{0},I_{1})}$${\Delta(I_{1},I_{1})}$${\Gamma(I_{1},I_{1})}$$\scriptstyle{\phi_{I_{0}}}$$\scriptstyle{\textsf{map}^{+}_{\Delta}\;i_{2}}$$\scriptstyle{\textsf{map}^{+}_{\Gamma}\;i_{2}}$$\scriptstyle{\phi_{I_{1}}}$$\scriptstyle{\textsf{map}^{-}_{\Delta}\;i_{2}}$$\scriptstyle{\textsf{map}^{-}_{\Gamma}\;i_{2}}$

can be called a commutative chevron, where here commutative means that the
condition from Definition 2.3 is satisfied: for any span
$\Delta(I_{0},I_{0})\leftarrow\mathbf{1}\to\Delta(I_{1},I_{1})$ on the left
for which the resulting diamond commutes, the resulting hexagon commutes. So,
similarly to how naturality squares can be combined side-by-side (giving us
the composability of natural transformations), paranaturality chevrons can be
snapped together, giving us the composability of paranatural transformations.

The existing literature provides several alternative characterizations of
strong dinaturality, allowing us to use spans with vertices besides
$\mathbf{1}$ in the description of commutative chevrons given in the previous
paragraph.

###### Proposition 2.6.

For difunctors $\Delta,\Gamma$ and a class of maps
$\phi_{I}:\Delta(I,I)\to\Gamma(I,I)$, the following are equivalent:

  1. (1)

$\phi$ is a paranatural transform: if $d_{0},d_{1},i_{2}$ are such that
$\textsf{map}^{+}_{\Delta}\;i_{2}\;d_{0}=\textsf{map}^{-}_{\Delta}\;i_{2}\;d_{1}$,
then
$\textsf{map}^{+}_{\Gamma}\;i_{2}\;(\phi_{I_{0}}\;d_{0})=\textsf{map}^{-}_{\Gamma}\;i_{2}\;(\phi_{I_{1}}\;d_{1})$.

  2. (2)

For any set $W$, functions $w_{0}\colon W\to\Delta(I_{0},I_{0})$ and
$w_{1}\colon W\to\Delta(I_{1},I_{1})$, and
$i_{2}\colon\textsf{Hom}_{\mathbb{C}}(I_{0},I_{1})$ such that
$(\textsf{map}^{+}_{\Delta}\;i_{2})\circ
w_{0}=(\textsf{map}^{-}_{\Delta}\;i_{2})\circ w_{1}$, it is the case that
$(\textsf{map}^{+}_{\Gamma}\;i_{2})\circ\phi_{I_{0}}\circ
w_{0}=(\textsf{map}^{-}_{\Gamma}\;i_{2})\circ\phi_{I_{1}}\circ w_{1}$.

  3. (3)

For every $i_{2}\colon\textsf{Hom}_{\mathbb{C}}(I_{0},I_{1})$, it is the case
that

$(\textsf{map}^{+}_{\Gamma}\;i_{2})\circ\phi_{I_{0}}\circ
p_{0}=(\textsf{map}^{-}_{\Gamma}\;i_{2})\circ\phi_{I_{1}}\circ p_{1}$

where $p_{0},p_{1}$ are the projection maps of the pullback

${\Delta(I_{0},I_{1})\times_{\Delta(I_{0},I_{1})}\Delta(I_{1},I_{1})}$${\Delta(I_{0},I_{0})}$${\Delta(I_{1},I_{1})}$${\Delta(I_{0},I_{1}).}$$\scriptstyle{p_{0}}$$\scriptstyle{p_{1}}$${\lrcorner}$$\scriptstyle{\textsf{map}^{+}_{\Delta}\;i_{2}}$$\scriptstyle{\textsf{map}^{-}_{\Delta}\;i_{2}}$

The latter formulation is the definition that appears in the older
references(Paré and Román, 1998; Mulry, 1992), though more recent works often
use the second (e.g. (Uustalu, 2010; Hackett and Hutton, 2015)). Regardless,
the difference is superficial (at least when Set is the codomain of the
difunctors): (1) and (3) are equivalent due to the standard explicit
description of pullbacks in Set. Similarly, (2) is just (1), repeated for each
element of the set $W$. However, the more category-theoretic nature of (2) and
(3) provide at least some promise that this notion of paranaturality will
generalize to difunctors with codomains besides Set. We leave exploration of
this point to future work.

A rephrasing of paranaturality which will see more use in the present work—and
which sheds more light on the composition of paranaturals444We’ll sometimes
abbreviate paranatural transformations to just paranaturals when
convenient.—involves a diagonal analogue of the category of elements.

###### Definition 2.7.

For a difunctor
$\Gamma:\mathbb{C}^{\text{op}}\times\mathbb{C}\to\textsf{Set}$, define the
category of $\Gamma$-structures (or category of diagonal elements of
$\Gamma$), denoted ${\Gamma}\textsf{-Struct}$, by

$\displaystyle\left|{\Gamma}\textsf{-Struct}\right|$
$\displaystyle:\equiv\sum_{I:\mathbb{C}}\Gamma(I,I)$
$\displaystyle\left({\Gamma}\textsf{-Struct}\right)\;(I_{0},g_{0})\;(I_{1},g_{1})$
$\displaystyle:\equiv\sum_{i_{2}:\textsf{Hom}(I_{0},I_{1})}\textsf{map}^{+}_{\Gamma}\;i_{2}\;g_{0}=\textsf{map}^{-}_{\Gamma}\;i_{2}\;g_{1}$

We’ll sometimes write $i_{2}\colon(I_{0},g_{0})\to(I_{1},g_{1})$ to indicate
that $i_{2}$ is a ${\Gamma}\textsf{-Struct}$-homomorphism.

An essential aspect of paranaturals is that they only operate on the diagonal
(hence their earlier name of strong dinatural transformations, that is, strong
diagonal natural transformations). Paranatural transformations manage a
careful balance of being chiefly concerned with the diagonal, but not
discarding off-diagonal data (e.g. elements of $\Delta(I,J)$ and how the
morphism parts of $\Delta$ affect them). Ultimately, the structures we’ll be
interested in will live in the diagonal—hence the above definition of diagonal
structures—but homomorphisms between them will be dictated by the morphism
parts, which take us away from the diagonal. This tension is exhibited in the
following example.

###### Example 2.8.

The wild group data difunctor
$\textsf{WldGrpData}\colon\textsf{Set}^{\text{op}}\times\textsf{Set}\to\textsf{Set}$
has object part

(4) $\textsf{WldGrpData}(X^{-},X^{+})\quad:\equiv(X^{-}\times X^{-}\to
X^{+})\times X^{+}\times(X^{-}\to X^{+})$

with morphism parts given by the appropriate pre- and post-compositions.

The category WldGrp of wild groups is defined as WldGrpData-Struct: objects
are pairs $(X,\mu_{X},e_{X},i_{X})$ with $\mu_{X}\colon X\times X\to X$,
$e_{X}\colon X$ and $i_{X}\colon X\to X$. Spelling out the morphism part of
Definition 2.7, we get that a wild group homomorphism
$(X,\mu_{X},e_{X},i_{X})\to(Y,\mu_{Y},e_{Y},i_{Y})$ is a function $f\colon
X\to Y$ such that

$f\circ\mu_{X}=\mu_{Y}\circ(f\times f)\quad\quad\text{and}\quad\quad
f(e_{X})=e_{Y}\quad\quad\text{and}\quad\quad f\circ i_{X}=i_{Y}\circ f.$

In other words, a function that preserves all the relevant structure.

The structures in this example–wild groups–come from the diagonal
$\textsf{WldGrpData}(X,X)$, but defining homomorphisms involves the off-
diagonal $\textsf{WldGrpData}(X,Y)$, a set which otherwise is not really of
interest. The fact that these are wild groups as opposed to just groups refers
to the fact that we have not imposed the group laws of associativity, unit,
and inverse. We cannot impose these as parts of the difunctor (i.e. in
Equation 4), since the laws only make sense on the diagonal. Instead, we must
later carve the category of groups out as a subcategory of the category of
wild groups: the latter encodes the actual stuff of the construction, to which
we must impose laws. We also leave to future work the question of whether
these steps can be unified.

The equality required for $i_{2}$ to be a $\Gamma$-structure homomorphism is,
of course, the same equality which appears in the definition of paranatural
transformation. This observation leads to the following alternative
characterization of paranaturality (a special case of which appears in (Paré
and Román, 1998, 2.8)).

###### Proposition 2.9.

For difunctors $\Delta,\Gamma$ and a class of maps
$\phi_{I}:\Delta(I,I)\to\Gamma(I,I)$, the following are equivalent:

  1. (1)

$\phi$ is a paranatural transform: if $d_{0},d_{1},i_{2}$ are such that
$\textsf{map}^{+}_{\Delta}\;i_{2}\;d_{0}=\textsf{map}^{-}_{\Delta}\;i_{2}\;d_{1}$,
then
$\textsf{map}^{+}_{\Gamma}\;i_{2}\;(\phi_{I_{0}}\;d_{0})=\textsf{map}^{-}_{\Gamma}\;i_{2}\;(\phi_{I_{1}}\;d_{1})$.

  2. (2)

$\phi$ preserves structure homomorphisms: if $i_{2}$ is a
${\Delta}\textsf{-Struct}$-homomorphism from $(I_{0},d_{0})$ to
$(I_{1},d_{1})$, then $i_{2}$ is a ${\Gamma}\textsf{-Struct}$-homomorphism
from $(I_{0},\phi_{I_{0}}\;d_{0})$ to $(I_{1},\phi_{I_{1}}\;d_{1})$.

So, for any $\gamma\colon\Delta\xrightarrow{\diamond}\Gamma$, we obtain a
corresponding functor
$\underline{\gamma}\colon{\Delta}\textsf{-Struct}\to{\Gamma}\textsf{-Struct}$,
which is the identity on underlying objects/morphisms and uses the components
of $\gamma$ to transform the attached structures. As the proposition above
indicates, the fact that morphisms get sent to morphisms (which is certainly
required to define a functor) is the content of paranaturality. This operation
of taking the corresponding functor is itself functorial, because
$\underline{\theta\gamma}=\underline{\theta}\circ\underline{\gamma}$, where
the composition on the left is the composition of paranaturals and the
composition on the right is composition of functors. Viewing a paranatural
transformation as a functor of structures will come in handy at several
points, particularly in Section 5.

As mentioned in the introduction, we wish to consider the category whose
objects are difunctors and whose morphisms are paranatural transformations. By
analogy to the use of the notation $\hat{\mathbb{C}}$ to denote the category
of presheaves on $\mathbb{C}$ and natural transformations, we’ll adopt the
following notation.

###### Definition 2.10.

Write $\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$ for the category
whose objects are difunctors
$\mathbb{C}^{\text{op}}\times\mathbb{C}\to\textsf{Set}$ and whose morphisms
are paranatural transformations.

For full formality, we would of course be obliged to verify that the
composition operations on paranaturals is associative, that the identity
functions $\Delta(I,I)\to\Delta(I,I)$ constitute paranatural transformations,
and so on. But this is all quite routine. Perhaps the most exciting aspect of
$\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$ from a category-
theoretic perspective is that it possesses much of the elegant structure of
$\hat{\mathbb{C}}$. Indeed, the structure on the former generalizes that of
the latter to simultaneously deal with both covariance and contravariance. To
exemplify this, we rehearse the paranatural analogue of a topic which plays a
central role in category theory: Yoneda-style reasoning.

###### Definition 2.11.

The diYoneda embedding
$\textbf{yy}:\mathbb{C}^{\text{op}}\times\mathbb{C}\to\;\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$ is a functor with
object part

$\textbf{yy}\;(I_{0},I_{1})\;(J_{0},J_{1}):\equiv\textsf{Hom}_{\mathbb{C}}(I_{0},J_{1})\times\textsf{Hom}_{\mathbb{C}}(J_{0},I_{1})$

and all four morphism parts given by the appropriate pre- and post-composition

To gain some intuition about how the diYoneda embedding works and how to write
paranatural transformations involving it, it’s helpful to look at the category
of structures of a difunctor of the form $\textbf{yy}(I,J)$—which, again by
analogy to usual category theory, we might call a direpresentable difunctor.
This too turns out to generalize the single-variant cases: the category of
elements of a presheaf $\textbf{y}J$ is the so-called slice category
$\mathbb{C}/J$, and, similarly, a covariant representable functor will have a
coslice category as its category of elements. These are simultaneously
generalized in what we’ll call the splice category.

###### Definition 2.12.

For objects $I,J\colon\left|\mathbb{C}\right|$, define the splice category
$I/\mathbb{C}/J$ between $I$ and $J$ to be the category whose objects are
diagrams of the form

${I}$${K}$${J}$$\scriptstyle{\textsf{into}_{K}}$$\scriptstyle{\textsf{from}_{K}}$

and whose morphisms from $(K,\textsf{into}_{K},\textsf{from}_{K})$ to
$(L,\textsf{into}_{L},\textsf{from}_{L})$ are maps
$\ell\colon\textsf{Hom}(K,L)$ making both triangles commute:

${L}$${I}$${J}$${K}$$\scriptstyle{\textsf{from}_{L}}$$\scriptstyle{\textsf{into}_{L}}$$\scriptstyle{\textsf{into}_{K}}$$\scriptstyle{\textsf{from}_{K}}$$\scriptstyle{\ell}$

We’ll call an object $I\to K\to J$ an $(I,J)$-splice with vertex $K$.

Observe it would be the same to define $I/\mathbb{C}/J$ as
${\textbf{yy}(I,J)}\textsf{-Struct}$. If $\mathbb{C}$ has an initial object
$\mathbf{0}$ or a terminal object $\mathbf{1}$, the splice category
construction generalizes the construction of slice and coslice categories
(respectively) from usual category theory:

$\mathbb{C}/J\cong\mathbf{0}/\mathbb{C}/J\quad\quad\text{and}\quad\quad
I/\mathbb{C}\cong I/\mathbb{C}/\mathbf{1}.$

But, more relevant for our current purposes, this helps us say what it means
to define paranatural transformations involving direpresentable difunctors. To
define a paranatural transformation
$\alpha\colon\textbf{yy}(I,J)\xrightarrow{\diamond}\Gamma$ requires us to
assign, for each $(I,J)$-splice with vertex $K$, an element of $\Gamma(K,K)$,
in a functorial fashion: if $\ell\colon\textsf{Hom}(K,L)$ is a morphism of
splices from $(K,\textsf{from}_{K},\textsf{into}_{K})$ to
$(L,\textsf{from}_{L},\textsf{into}_{L})$, then it needs to be a morphism of
$\Gamma$-structures from $\alpha_{K}(\textsf{from}_{K},\textsf{into}_{K})$ to
$\alpha_{L}(\textsf{from}_{L},\textsf{into}_{L})$.

We’re now able to state our key result: a new Yoneda Lemma for difunctors.

###### Lemma 2.13 (diYoneda Lemma).

For any $\Gamma\colon\mathbb{C}^{\text{op}}\times\mathbb{C}\to\textsf{Set}$,
there is a paranatural isomorphism555That is, a pair of paranatural
transformations in either direction, whose composites are the identity
transformations; or, equivalently, a paranatural transfomation all of whose
components are bijections.

$\Gamma(I,J)\cong(\textbf{yy}(J,I)\xrightarrow{\diamond}\Gamma).$

Note that, on the right-hand side, the arguments to yy are flipped: this is
because the yy is itself in negative position, so the arguments must be
flipped so that both sides are still contravariant in $I$ and covariant in
$J$. More explicitly: the morphism parts of the right-hand side are given as
follows.

$\displaystyle(\textsf{map}^{-}_{RHS}\;(i_{2}\colon\textsf{Hom}(I_{0},I_{1}))\;(\phi\colon\textbf{yy}(J,I_{1})\xrightarrow{\diamond}\Gamma))_{K}$
$\displaystyle:\textsf{Hom}(J,K)\times\textsf{Hom}(K,I_{0})\to\Gamma(K,K)$
$\displaystyle(\textsf{map}^{-}_{RHS}\;i_{2}\;\phi)_{K}\;(\textsf{into}_{K},\textsf{from}_{K})$
$\displaystyle:\equiv\phi_{K}(\textsf{into}_{K},i_{2}\circ\textsf{from}_{K})$
$\displaystyle(\textsf{map}^{+}_{RHS}\;(j_{2}\colon\textsf{Hom}(J_{0},J_{1}))\;(\psi\colon\textbf{yy}(J_{0},I)\xrightarrow{\diamond}\Gamma))_{K}$
$\displaystyle:\textsf{Hom}(J_{1},K)\times\textsf{Hom}(K,I)\to\Gamma(K,K)$
$\displaystyle(\textsf{map}^{+}_{RHS}\;j_{2}\;\psi)_{K}\;(\textsf{into}_{K},\textsf{from}_{K})$
$\displaystyle:\equiv\psi_{K}(\textsf{into}_{K}\circ j_{2},\textsf{from}_{K})$

So the right-hand side indeed is difunctorial in $(I,J)$, hence it makes sense
to speak of paranatural transformations between it and the difunctor $\Gamma$.
With this established, we can prove the diYoneda Lemma. Thankfully, we don’t
need anything too novel: the proof is the same as the proof of the original
Yoneda Lemma, mutatis mutandis.

###### Proof.

For a given $g:\Gamma(I,I)$, the corresponding paranatural transformation
$\alpha_{g}\colon\textbf{yy}(I,I)\xrightarrow{\diamond}\Gamma$ is given by

$\displaystyle(\alpha_{g})_{K}$
$\displaystyle:\textsf{Hom}(I,K)\times\textsf{Hom}(K,I)\to\Gamma(K,K)$
$\displaystyle(\alpha_{g})_{K}\;(\textsf{into}_{K},\textsf{from}_{K})$
$\displaystyle:\equiv\textsf{map}^{+}_{\Gamma}\;\textsf{into}_{K}\;(\textsf{map}^{-}_{\Gamma}\;\textsf{from}_{K}\;g).$

Conversely, given a $\phi\colon\textbf{yy}(I,I)\xrightarrow{\diamond}\Gamma$,
obtain an element of $\Gamma(I,I)$ by applying $\phi_{I}$ to the pair of
identity morphisms $(\textsf{id}_{I},\textsf{id}_{I})$.

∎

To indicate how this diYoneda Lemma is used, we can show that
$\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$ is automatically a
cartesian closed category, irrespective of whatever structure $\mathbb{C}$
possesses. The analogous result for $\hat{\mathbb{C}}$ is a standard result of
basic category theory, and the author suspects (though has not verified yet)
that $\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$ can also be shown to
be a (co)complete elementary topos, and moreover that diYoneda preserves
whatever limits exist in $\mathbb{C}$, just as is the case with
$\hat{\mathbb{C}}$.

The terminal object and binary products in
$\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$ are precisely what
one might expect: the constant-$\mathbf{1}$ difunctor and the pointwise binary
product, respectively. Where diYoneda sees interesting application is in
determining what exponential objects must be (just like the Yoneda Lemma tells
us what exponentials in $\hat{\mathbb{C}}$ must be (MacLane and Moerdijk,
2012, I.6)). Yoneda-style reasoning proceeds in the following manner: assume
the thing exists with its desired universal property; use the Yoneda Lemma and
said property to transform it, eliminating reference to the purported thing;
then use the result as a definition and verify it indeed has the property. So
let’s do this. Given $\Delta,\Gamma$, suppose their exponential
$\Gamma^{\Delta}$ exists. Then,

(diYoneda Lemma) $\displaystyle\Gamma^{\Delta}(I,J)$
$\displaystyle\cong\textbf{yy}(J,I)\xrightarrow{\diamond}\Gamma^{\Delta}$
(desired property)
$\displaystyle\cong\textbf{yy}(J,I)\times\Delta\xrightarrow{\diamond}\Gamma$

So now we turn this into a definition: $\Gamma^{\Delta}(I,J)$ is defined as
the set of paranatural transformations from $\textbf{yy}(J,I)\times\Delta$ to
$\Gamma$. We can expand this definition into a more explicit description666An
element of $\Gamma^{\Delta}(I,J)$ is a family of maps $\psi$, where for each
$K\colon\left|\mathbb{C}\right|$, $\psi_{K}$ accepts $\Delta$-tagged $(J,I)$
splices with vertex $K$ (that is, triples
$(\textsf{into}_{K},\textsf{from}_{K},d)$ where $d\colon\Delta(K,K)$) and
sends them to $\Gamma$-structures on $K$ (i.e.
$\psi_{K}(\textsf{into}_{K},\textsf{from}_{K},d)\colon\Gamma(K,K)$) which is
paranatural: if $\ell\colon\textsf{Hom}(K,L)$ is a $(J,I)$-splice homomorphism
from $(K,\textsf{into}_{K},\textsf{from}_{K})$ to
$(L,\textsf{into}_{L},\textsf{from}_{L})$ and also a $\Delta$-structure
homomorphism from $(K,d)$ to $(L,d^{\prime})$, then
$\textsf{map}^{+}_{\Gamma}\;\ell\;(\psi_{K}(\textsf{into}_{K},\textsf{from}_{K},d))=\textsf{map}^{-}_{\Gamma}\;\ell\;(\psi_{L}(\textsf{into}_{L},\textsf{from}_{L},d^{\prime}))$
i.e. $\ell$ is a $\Gamma$-structure homomorphism from
$\psi_{K}(\textsf{into}_{K},\textsf{from}_{K},d)$ to
$\psi_{L}(\textsf{into}_{L},\textsf{from}_{L},d^{\prime})$. if desired.

The evaluation morphism
$\Gamma^{\Delta}\times\Delta\xrightarrow{\diamond}\Gamma$ required by the
definition of exponential is, indeed, defined as evaluation: given
$(\psi,d)\colon\Gamma^{\Delta}(I,I)\times\Delta(I,I)$, we can obtain an
element of $\Gamma(I,I)$ by just evaluating $\psi_{I}$ at
$(\textsf{id}_{I},\textsf{id}_{I},d)$. One can confirm this satisfies the
universal property of exponentials (we omit this for space). The (di)Yoneda
trick works yet again!

##  3\. Parametric Naturality

Now we turn our attention to using paranatural category theory. As described
in the introduction, a key motivation for this theory will be the
establishment of a function-based articulation of the abstraction/data hiding
involved in parametric polymorphism. Example 2.4 already gave us a flavor of
how paranatural transformations capture this idea, and how Wadler’s free
theorems are, at heart, just instances of the paranaturality condition. But in
this section we’ll aim to be more systematic.

Let us repeat the famous opening of (Wadler, 1989), with only a few minor
adjustments:

write down the definition of a polymorphic type (of at most one polymorphic
variable) on a piece of paper. Tell me its type, but be careful to not let me
see the function’s definition. I will tell you a theorem that the function
satisfies. The purpose of this section is to explain this trick.

Like Wadler, we’ll develop our ‘trick’ to work on Girard/Reynolds-style System
F (Girard, 1972, 1986; Reynolds, 1983, 1974). To distinguish from our
metatheory, we’ll use teletype font to denote the syntax of System F, e.g.
writing unit and bool for the singleton type and boolean type, respectively,
in System F, and writing T1 -> T2 for the type of functions from T1 to T2. The
trick will be to convert type expressions of a single polymorphic type
variable into difunctors, and then obtain the free theorem as the
paranaturality condition of a paranatural transformation into said difunctor.
This is the reason for the restriction to only a single polymorphic type
variable: a difunctor only encodes positive and negative dependence on a
single argument. As we’ll indicate at the end of this section, this
restriction can be lifted by developing appropriate notions of multivariable
difunctiors and multi-paranatural transformations, but we avoid doing so here
for simplicity.

Let’s first develop the case that we’re mainly interested in: polymorphic
types of the form

$\forall\alpha.\texttt{T1}\;\texttt{->}\;\texttt{T2}$

where T1 and T2 are type expressions, possibly containing $\alpha$. If we have
a type of the form $\forall\alpha.\texttt{T}$ where the topmost connective of
T is not an arrow, we can equivalently replace T with unit -> T and carry on.
So the only real constraint is the above-mentioned restriction to single-
variable polymorphism. To obtain our free theorem, we translate T1 and T2 into
difunctors
$\left\llbracket\texttt{T1}\right\rrbracket,\left\llbracket\texttt{T2}\right\rrbracket\colon\textsf{Set}^{\text{op}}\times\textsf{Set}\to\textsf{Set}$
according to their dependence on $\alpha$. The following examples are
sufficiently illustrative of the procedure for doing this for an arbitrary
System F type expression T which may contain $\alpha$.

  * •

If T does not, in fact, contain $\alpha$ (i.e. it is a closed type, like unit
or $\texttt{list}(\texttt{nat})$), then
$\left\llbracket\texttt{T}\right\rrbracket$ is just the constant difunctor
returning the set of terms of T.

  * •

$\left\llbracket\alpha\right\rrbracket$ is the identity functor, taken as a
difunctor which ignores its contravariant argument.

  * •

$\left\llbracket\alpha\;\texttt{->}\;\texttt{bool}\right\rrbracket$ is the
presheaf whose object part sends $X$ to the set of functions $X\to\mathbf{2}$
and whose morphism part is given by precomposition.

  * •

$\left\llbracket(\alpha\;\texttt{->}\;\alpha)\;\texttt{->}\;\alpha\right\rrbracket$
is the difunctor whose object part sends $(I,J)$ to the set of functions
$(J\to I)\to J$, with morphism parts by composition, e.g.
$(\textsf{map}^{+}\;j_{2})\colon((J_{0}\to I)\to J_{0})\to(J_{1}\to I)\to
J_{1}$ sends $w:(J_{0}\to I)\to J_{0}$ and $x\colon J_{1}\to I$ to
$j_{2}(w\;(x\circ j_{2}))\colon J_{1}$.

  * •

$\left\llbracket\texttt{list}\;\alpha\;\texttt{->}\;\texttt{list}\;\alpha\right\rrbracket$
is the list rearrangement difunctor of Example 2.4.

And so on. The general pattern is that appearing to the left of an arrow flips
the variances, and morphism parts are ultimately given by composition of some
form (perhaps run through an endofunctor like List). With that, here’s our
notion of parametricity.

###### Principle 3.1.

Every term of type $\forall\alpha.\texttt{T1}\;\texttt{->}\;\texttt{T2}$
constitutes a paranatural transformation from
$\left\llbracket\texttt{T1}\right\rrbracket$ to
$\left\llbracket\texttt{T2}\right\rrbracket$.

This is stated as an informal principle rather than a theorem because we can
only determine its validity or falsity with respect to a given model of System
F, and because we are, at this point, only conjecturing it as a way of stating
parametricity. As our examples show, the resulting conditions we obtain from
this principle end up saying just the free theorems which can be obtained from
the relational formulation of parametricity, lending credence to the belief
that this notion of parametricity applies in any model where relational
parametricity holds. It remains to future work to fully sketch the connection
between both notions of parametricity, and determine if they are indeed the
same.

Let us demonstrate the use of this principle. We’ve had our first example
already, Example 2.4, which gave the free theorem for the type
$\forall\alpha.(\alpha*\alpha\to\texttt{bool})\;\texttt{->}\;\texttt{list}(\alpha)\to\texttt{list}(\alpha)$.
Here are two more standard examples, which further demonstrate the method.

###### Example 3.1.

For the type

$\forall\alpha.\texttt{list}\;\alpha\;\texttt{->}\;\texttt{list}\;\alpha\;\texttt{->}\;\texttt{list}\;\alpha,$

our T1 is $\texttt{list}(\alpha)$ and our T2 is
$\texttt{list}\;\alpha\;\texttt{->}\;\texttt{list}\;\alpha$, so
$\left\llbracket\texttt{T1}\right\rrbracket$ is just the List functor itself
and $\left\llbracket\texttt{T2}\right\rrbracket$ is the list rearrangement
functor. So the paranaturality condition of
$app\colon\left\llbracket\texttt{T1}\right\rrbracket\xrightarrow{\diamond}\left\llbracket\texttt{T2}\right\rrbracket$
says that if $f\colon X\to Y$ and

$\textsf{map}_{\textsf{List}}\;f\;xs=ys$

, then

$(\textsf{map}_{\textsf{List}}\;f)\circ(app_{X}\;xs)=(app_{Y}\;ys)\circ(\textsf{map}_{\textsf{List}}\;f)$

as functions of type $\textsf{List}(X)\to\textsf{List}(Y)$. This is just a
slightly-different phrasing from Wadler’s.

###### Example 3.2.

For the type

$\forall\alpha.\alpha$

i.e. $\forall\alpha.\texttt{unit}\;\texttt{->}\;\alpha$, Principle 3.1 says
that if $s:\forall\alpha.\alpha$, then, for any types $X$ and $Y$ and any
function $f\colon X\to Y$,

$f(s_{X})=s_{Y}.$

But taking $f$ to be the swapping function $\mathbf{2}\to\mathbf{2}$ shows
this to be absurd, hence this free theorem tells us $\forall\alpha.\alpha$
must be the empty type.

So we can see that, for these standard examples of polymorphic types,
relational parametricity and strong dinaturality coincide. As mentioned,
further work is needed to clarify whether this is true in general. But,
regardless of the outcome of this investigation, it is clear that the theory
of paranaturality outlined in Section 2 has a significant connection to the
theory of parametricity, and that the latter would undoubtedly benefit from
further research into paranatural category theory.

To conclude this section, let us briefly indicate how to lift the single-
variable restriction above, and thereby be able to apply this method to, for
example, the polymorphic zip type
$\forall\alpha\forall\beta.(\texttt{list}(\alpha)*\texttt{list}(\beta))\;\texttt{->}\;\texttt{list}(\alpha*\beta)$.
To do this in full generality, we’ll need a theory of multi-variable
difunctors. We already understood the diYoneda embedding (Definition 2.11) as
a kind of 2-variable difunctor: it takes in four objects in its object part,
and has four morphism parts. Since we wanted to supply only some of the
arguments at any given time, we expressed this as a difunctor whose codomain
is $\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$ instead of Set. To
iterate this, we would need to define a notion of paranatural transformation
of 2-variable difunctors, then define 3-variable difunctors as difunctors into
the category of 2-variable difunctors, and so on. Nothing about this theory
seems to be too burdensome or surprising, we only omit it here because it
would lead us too far afield for our purposes.

##  4\. Impredicative Encodings of (Co)Inductive Types

The theory of paranaturality laid out in Section 2 also connects in an elegant
way to another important theoretical topic in functional programming: the
category-theoretic semantics of (co)inductive types as initial algebras and
terminal coalgebras of endofunctors. Our goal for the present section will be
to sketch these connections, beginning with inductive types.

###  4.1. Structural Ends and Inductive Types

In the previous sections, we did not pay attention to size issues, i.e.
whether certain collections (particularly the collection of paranatural
transformations between two difunctors) constituted a set, or whether some
machinery of small sets vs. large sets, or sets vs. proper classes, or a
hierarchy of Grothendieck universes was required. In this section, we will be
more careful. The paranatural apparatus we’ll be using to study initial
algebras—insofar as they exist—will be the following notion, which are to
paranatural transformations what ends are to dinatural transformations (see
(Mac Lane, 1978, IX.4–5) and (Bainbridge et al., 1990, Sect. 1)).

###### Definition 4.1.

For a difunctor
$\Gamma\colon\textsf{Set}^{\text{op}}\times\textsf{Set}\to\textsf{Set}$, we
say that a set $\mu_{\Gamma}$ is the structural end of $\Gamma$ and write

$\mu_{\Gamma}=\int_{X\colon\textsf{Set}}\Gamma(X,X)\;\textbf{d}X$

if $\mu_{\Gamma}$ is the equalizer of the parallel arrows777For reasons of
space, we’ve made the quantification over $(I_{0},g_{0})$ and $(I_{1},g_{1})$
implicit on the right-hand side of Equation 5. The full right-hand side is:
$((I_{0},g_{0})\colon{\Gamma}\textsf{-Struct})\quad\to\quad((I_{1},g_{1})\colon{\Gamma}\textsf{-Struct})\quad\to\quad\big{(}i_{2}\colon\textsf{Hom}_{{\Gamma}\textsf{-Struct}}\;(I_{0},g_{0})\;(I_{1},g_{1})\big{)}\quad\to\quad
I_{1}$

(5) ${\bigg{(}\big{(}(I,g)\colon{\Gamma}\textsf{-Struct}\big{)}\to
I\bigg{)}}$${\bigg{(}\big{(}i_{2}\colon\textsf{Hom}_{{\Gamma}\textsf{-Struct}}\;(I_{0},g_{0})\;(I_{1},g_{1})\big{)}\to
I_{1}\bigg{)}}$

given by

$\displaystyle\lambda\;\varphi\;(I_{0},g_{0})\;(I_{1},g_{1})\;i_{2}$
$\displaystyle\to i_{2}\left(\varphi_{(I_{0},g_{0})}\right)$
$\displaystyle\lambda\;\varphi\;(I_{0},g_{0})\;(I_{1},g_{1})\;i_{2}$
$\displaystyle\to\varphi_{(I_{1},g_{1})}.$

Since this equalizer is taking place in Set, we have a definite description of
it:

(6)
$\mu_{\Gamma}:\equiv\sum_{\varphi\colon((I,g)\colon{\Gamma}\textsf{-Struct})\to
I}(\textsf{map}^{+}_{\Gamma}\;i_{2}\;g_{0}=\textsf{map}^{-}_{\Gamma}\;i_{2}\;g_{1})\to\left(i_{2}\left(\varphi_{(I_{0},g_{0})}\right)=\varphi_{(I_{1},g_{1})}\right).$

We’ve made the quantification of $(I_{0},g_{0}),(I_{1},g_{1}),$ and $i_{2}$
implicit here (for space), but spelled out explicitly the
${\Gamma}\textsf{-Struct}$ homomorphism condition. The reason for the phrasing
given in Definition 4.1 is to avoid assuming the existence of such a
$\mu_{\Gamma}$, since there’s no guarantee a priori that the expression on the
right-hand side, which quantifies over all sets, defines a set (under pain of
Russell’s paradox). We could remedy this issue by restricting $\Gamma$’s
codomain to a universe of small sets (the approach taken in the next section),
but for the moment we’re more concerned with those situations where $\Gamma$
has a structural end in the same universe as its elements. The most famous
instance of this is the following example.

###### Example 4.2.

Let $H^{N}:\textsf{Set}^{\text{op}}\times\textsf{Set}\to\textsf{Set}$ be the
difunctor with object part

$H^{N}(X^{-},X^{+}):\equiv X^{+}\times(X^{-}\to X^{+})$

with morphism parts by composition. We’ll call the category of
$H^{N}$-structures $N$-algebras:

$\left|{N}\textsf{-Alg}\right|:\equiv\sum_{X\colon\textsf{Set}}X\times(X\to
X).$

The set $\mathbb{N}$ of natural numbers, equipped with the injection

(7) $\lambda\;n\;(X,x,s)\to
s^{n}(x)\quad\colon\quad\mathbb{N}\to((X,x,s)\colon{N}\textsf{-Alg})\to X$

is the structural end of $H^{N}$.

  * •

For any homomorphism of $N$-algebras $f\colon(X,x,s)\to(Y,y,t)$ (i.e. a
function $f\colon X\to Y$ such that $f(x)=y$ and $f\circ s=t\circ f$), it is
indeed the case that, for any $n\colon\mathbb{N}$,

$f(s^{n}\;x)=t^{n}\;y,$

so the map given in Equation 7 equalizes the parallel arrows of Equation 5.

  * •

If $\zeta\colon Z\to((X,x,s)\colon{N}\textsf{-Alg})\to X$ is any other map
such that

(8) $f(\zeta\;z\;(X,x,s))=\zeta\;z\;(Y,y,t)$

for every $z\colon Z$ and homomorphism $f:(X,x,s)\to(Y,y,t)$, then define a
map $h\colon Z\to\mathbb{N}$ by

$h(z):\equiv\zeta\;z\;(\mathbb{N},0,\textsf{succ}).$

Then, for any $z$ and any $(Y,y,t)$,

$\displaystyle\big{(}(\lambda\;n\;(X,x,s)\to s^{n}(x))\circ
h\big{)}\;z\;(Y,y,t)$ $\displaystyle\equiv t^{h(z)}\;y$ $\displaystyle\equiv
t^{(\zeta\;z\;(\mathbb{N},0,\textsf{succ}))}\;y$ (Equation 8, with
$f\equiv\lambda\;n\to t^{n}y$) $\displaystyle=\zeta\;z\;(Y,y,t).$

We know that $\lambda\;n\to s^{n}x$ is a ${N}\textsf{-Alg}$-homomorphism from
$(\mathbb{N},0,\textsf{succ})$ to $(X,x,s)$, because
$s^{\textsf{succ}(n)}\equiv s\circ s^{n}$ and $s^{0}x\equiv x$, so the
application of Equation 8 is legitimate. Therefore, conclude

$\zeta=\big{(}\lambda\;n\;(X,x,s)\to s^{n}x\big{)}\circ h,$

satisfying the universal property of the equalizer.888For full formality, we
need to show that this factorization $h$ of $\zeta$ is unique, but this
follows easily from the injectivity of the map $\lambda\;n\;(X,x,s)\to
s^{n}x$.

The ideas rehearsed in this example are, of course, the main ingredients that
go into understanding $\mathbb{N}$ as the initial algebra of the maybe
endofunctor $N(X):\equiv\mathbf{1}+X$, just spelled out using the calculus of
difunctors and structural ends. If we were to define $\mathbb{N}$ as
$\int_{X\colon\textsf{Set}}X\times(X\to X)\;\textbf{d}X$, then this would be
an inherently impredicative definition, because it’s essential that we be able
to instantiate any of these $\varphi\colon((X,x,s)\colon{N}\textsf{-Alg})\to
X$ with the $N$-algebra $(\mathbb{N},0,\textsf{succ})$ itself (as we must do
above to prove the universal property). This therefore gives us an
impredicative encoding of the inductive type $\mathbb{N}$, the same one given
in (Awodey et al., 2018). Like Awodey et al., we can generalize this result to
one about algebras of an arbitrary endofunctor.

###### Definition 4.3.

Let $T\colon\textsf{Set}\to\textsf{Set}$ be an endofunctor. Define the
$T$-algebraic difunctor $H^{T}$ to have object part

$H^{T}(X^{-},X^{+}):\equiv T(X^{-})\to X^{+}$

with $\textsf{map}^{-}_{H^{T}}\;x_{2}$ given by precomposition by $T(x_{2})$
and $\textsf{map}^{+}_{H^{T}}$ given by postcomposition.

The category of $H^{T}$-structures is known in the literature as the category
of $T$-algebras: a $T$-algebra is a set $X$ equipped with a function $T(X)\to
X$, and a $T$-algebra homomorphism from $(X,u)$ to $(Y,v)$ is a function
$f\colon X\to Y$ such that $f\circ u=v\circ T(f)$.

An initial $T$-algebra is a $T$-algebra $(\mu_{T},\textsf{in}_{T})$ such that,
for every $T$-algebra $(X,u)$, there exists a unique $T$-algebra homomorphism
$(\textsf{rec}\;u)\colon(\mu_{T},\textsf{in}_{T})\to(X,u)$.

###### Proposition 4.4.

For an endofunctor $T$, the following are equivalent

  * •

The structural end $\int_{X\colon\textsf{Set}}T(X)\to X\;\textbf{d}X$ exists

  * •

$T$ has an initial algebra

Indeed, the underlying set $\mu_{T}$ of the initial algebra–when it exists–is
precisely the structural end $\int_{X\colon\textsf{Set}}T(X)\to
X\;\textbf{d}X$. Moreover, the required $T$-algebra homomorphism
$(\textsf{rec}\;u)\colon\mu_{T}\to X$ for any $T$-algebra $(X,u)$ takes
$\varphi\colon\mu_{T}$ to $\varphi_{(X,u)}$.999Here, and henceforth, we’re
making the map from $\mu_{T}$ to $((X,u)\colon{T}\textsf{-Alg})\to X$
implicit, since we’ll generally think of the former as a subset of the latter,
as in Equation 6. Only for a specific example where we have established
notation for $\mu_{T}$, like Example 4.2 above, is it helpful to make this
inclusion map explicit. And we can even give an explicit description of the
$T$-algebra structure which $\mu_{T}$ is equipped with:

$\displaystyle\textsf{in}_{T}:\equiv\lambda\;(\omega\colon
T(\mu_{T}))\;\big{(}(X,u)\colon{T}\textsf{-Alg}\big{)}\;\to
u(T(\textsf{rec}\;u)\;\omega)\quad\colon\quad T(\mu_{T})\to\mu_{T}.$

So this framework of structural ends of difunctors connects cleanly to the
logic of initial algebras, and the key results from that well-studied topic
(e.g. (Pohlová, 1973; Adámek, 1974)) can be employed.

Let us conclude this subsection by noting that Definition 4.1 admits a nice
generalization.

###### Definition 4.5.

For difunctors
$\Gamma,\Theta\colon\mathbb{C}^{\text{op}}\times\mathbb{C}\to\textsf{Set}$, we
say that a set $\mu$ is the structural end of $\Gamma$ with respect to
$\Theta$ and write

$\mu=\int_{X\colon\textsf{Set}}\Gamma(X,X)\;\textbf{d}\Theta(X,X)$

if $\mu$ is the equalizer of the parallel arrows

(9)
${\bigg{(}\big{(}(I,g)\colon{\Gamma}\textsf{-Struct}\big{)}\to\Theta(I,I)\bigg{)}}$${\bigg{(}\big{(}i_{2}\colon\textsf{Hom}_{{\Gamma}\textsf{-Struct}}\;(I_{0},g_{0})\;(I_{1},g_{1})\big{)}\to\Theta(I_{0},I_{1})\bigg{)}}$

given by

$\displaystyle\lambda\;\varphi\;(I_{0},g_{0})\;(I_{1},g_{1})\;i_{2}$
$\displaystyle\to\textsf{map}^{+}_{\Theta}\;i_{2}\;\varphi_{(I_{0},g_{0})}$
$\displaystyle\lambda\;\varphi\;(I_{0},g_{0})\;(I_{1},g_{1})\;i_{2}$
$\displaystyle\to\textsf{map}^{-}_{\Theta}\;i_{2}\;\varphi_{(I_{1},g_{1})}.$

First, this definition generalizes Definition 4.1: take $\Theta$ to be the
identity functor $\textsf{Set}\to\textsf{Set}$, considered as a difunctor.
Now, a discerning reader will notice that this $\mu$ is precisely the set of
paranatural transformations from $\Gamma$ to $\Theta$! So all that’s necessary
for this $\mu$ to exist is that there is only a set of such transformations–as
Lemma 2.13 shows, this happens whenever $\Gamma$ is direpresentable. This
observation also connects these results to the discussion in the previous
section: the standard Church encoding of the initial $T$-algebra in System F
is
$\forall\alpha.(\texttt{T}(\alpha)\;\texttt{->}\;\alpha)\;\texttt{->}\;\alpha$,
whose terms, according to Principle 3.1, are precisely paranatural
transformations from $H^{T}$ to the identity functor, i.e. elements of
$\int_{X:\textsf{Set}}T(X)\to X\;\textbf{d}X$. With paranatural category
theory, we are able to unite parametricity, induction, and structural ends,
all in a single, elegant theory.

Once again, the natural numbers supply us with an interesting example
(originally suggested in (Bainbridge et al., 1990), fully developed as (Paré
and Román, 1998, Prop. 1)) where this integral exists:

$\mathbb{N}=\int_{X\colon\textsf{Set}}(X\to X)\;\textbf{d}(X\to X).$

In other words: a natural number is just an endo-paranatural transformation of
the hom difunctor! In contrast to the earlier uncurried encoding of
$\mathbb{N}$ as the structural end of $H^{N}$, i.e. the initial $N$-algebra,
this is a curried encoding. The paranatural transformation corresponding to
some $n\colon\mathbb{N}$ is, of course, the one taking some $u:X\to X$ to its
$n$-fold composition $u^{n}\colon X\to X$.

This more general notion of structural end also allows us to state a Yoneda-
like Lemma for initial algebras.

###### Lemma 4.6 (Uustalu 2010, Prop. 1).

If $T\colon\textsf{Set}\to\textsf{Set}$ is an endofunctor which has an initial
algebra $\mu_{T}$, and $F\colon\textsf{Set}\to\textsf{Set}$ is any
endofunctor, then there is an isomorphism

$F(\mu_{T})\cong\int_{X\colon\textsf{Set}}T(X)\to X\;\textbf{d}F(X)$

There is also a sense in which this isomorphism is natural in $T$, but we
won’t delve into that here. Note that Proposition 4.4 can be proved as a
corollary of this result, by taking $F$ to be the identity functor. In op.
cit., this result is stated directly in terms of paranatural transformations
(there referred to as strong dinatural transformations), and some of the
consequences for fixpoint operators are developed.

As we saw, phrasing these results in terms of difunctors (rather than just
specifically about $T$-algebraic difunctors) opened up the path to Definition
4.5, allowing us to obtain the curried encoding of $\mathbb{N}$, connect these
results to the broader theory of paranaturality, and state Lemma 4.6. It also
suggests another direction to expand the theory: dualization.

###  4.2. Costructure Integrals and Coinductive Types

As with most major concepts in category theory, the notion of ends were
introduced along with their dual notion, coends. Since Definition 4.1 is
phrased in terms of equalizers, they are ripe for dualization in terms of
coequalizers.

###### Definition 4.7.

For a difunctor
$\Gamma\colon\textsf{Set}^{\text{op}}\times\textsf{Set}\to\textsf{Set}$, we
say that a set $\nu_{\Gamma}$ is the structural coend of $\Gamma$ and write

$\nu_{\Gamma}=\int^{X\colon\textsf{Set}}\Gamma(X,X)\;\textbf{p}X$

if $\nu_{\Gamma}$ is the coequalizer of the parallel arrows

(10)
${\sum\limits_{i_{2}\colon\textsf{Hom}_{{\Gamma}\textsf{-Struct}}\;(I_{0},g_{0})\;(I_{1},g_{1})}I_{0}}$${\sum\limits_{(I,g)\colon{\Gamma}\textsf{-Struct}}I}$

given by

$\displaystyle\lambda\;(i_{2},x)$ $\displaystyle\to((I_{0},g_{0}),x)$
$\displaystyle\lambda\;(i_{2},x)$ $\displaystyle\to((I_{1},g_{1}),i_{2}(x)).$

As with the dual $\mu_{\Gamma}$, this set $\nu_{\Gamma}$ admits an explicit
definition, with the attached caveat that its existence is not guaranteed. In
the category Set, coequalizers are given by quotients. Specifically, this
coequalizer is the type $\sum_{(I,g)\colon{\Gamma}\textsf{-Struct}}I$ of
pointed $\Gamma$ structures, quotiented by bisimilarity.

###### Definition 4.8.

The binary relation of bisimilarity on pointed $\Gamma$-structures

$\textsf{Bisim}_{\Gamma}\subseteq\left(\sum_{(I,g)\colon{\Gamma}\textsf{-Struct}}I\right)\times\left(\sum_{(I,g)\colon{\Gamma}\textsf{-Struct}}I\right)$

is the equivalence relation generated by

$\left(i_{2}\colon\textsf{Hom}_{{\Gamma}\textsf{-Struct}}\;(I_{0},g_{0})\;(I_{1},g_{1})\right)\quad\to\quad(x_{0}\colon
I_{0})\quad\to\quad\textsf{Bisim}_{\Gamma}\;(I_{0},g_{0},x_{0})\;(I_{1},g_{1},i_{2}(x_{0}))$

In short: two points are bisimilar if there’s a homomorphism connecting them.
The question of existence here is whether the bisimilarity relation glues
together enough pointed $\Gamma$-structures to obtain a small set. Similarly
to how endofunctor algebras provided us concrete examples of existent
structural ends, endofunctor coalgebras will furnish examples of existent
structural coends.

###### Definition 4.9.

Let $T\colon\textsf{Set}\to\textsf{Set}$ be an endofunctor. Define the
$T$-coalgebraic difunctor $H_{T}$ to have object part

$H_{T}(X^{-},X^{+}):\equiv X^{-}\to T(X^{+}).$

The category of $H_{T}$-structures is known as the category of $T$-coalgebras:
a $T$-coalgebra is a set $X$ equipped with a function $X\to T(X)$, and a
$T$-coalgebra homomorphism from $(X,u)$ to $(Y,v)$ is a function $f\colon X\to
Y$ such that $T(f)\circ u=v\circ f$.

An terminal $T$-coalgebra is a $T$-coalgebra $(\nu_{T},\textsf{out}_{T})$ such
that, for every $T$-coalgebra $(X,u)$, there exists a unique $T$-coalgebra
homomorphism $(\textsf{corec}\;u)\colon(X,u)\to(\nu_{T},\textsf{out}_{T})$.

###### Example 4.10.

For any set $A$, the set $\textsf{Stream}(A):\equiv\mathbb{N}\to A$ of
$A$-streams is the structural coend of the difunctor
$(X^{-},X^{+})\mapsto(X^{-}\to A)\times(X^{-}\to X^{+})$.101010Which is
equivalent to the coalgebraic difunctor $H_{S_{A}}$, where $S_{A}$ is the
endofunctor sending $X$ to to $A\times X$. To define the requisite map
$\epsilon$ from pointed coalgebras $\sum_{X\colon\textsf{Set}}(X\to
A)\times(X\to X)\times X$ to $\textsf{Stream}(A)$, send a pointed coalgebra
$(X,h_{X},t_{X},x_{0})$ to the stream

$h_{X}(x_{0}),\quad h_{X}(t_{X}\;x_{0}),\quad h_{X}(t_{X}(t_{X}\;x_{0})),\quad
h_{X}(t_{X}(t_{X}(t_{X}\;x_{0}))),\quad\ldots$

(more formally:
$\epsilon(X,h_{X},t_{X},x_{0})\equiv\lambda\;(n\colon\mathbb{N})\to
h_{X}(t_{X}^{n}\;x_{0})$). This respects the bimilarity equivalence relation:
if we have pointed coalgebras

$(X,h_{X},t_{X},x_{0}),\;(Y,h_{Y},t_{Y},y_{0})\quad\colon\sum_{X\colon\textsf{Set}}(X\to
A)\times(X\to X)\times X$

and a coalgebra homomorphism from $(X,h_{X},t_{X})$ to $(Y,h_{Y},t_{Y})$
sending $x_{0}$ to $y_{0}$, then we can show by a simple natural number
induction that

$\epsilon(X,h_{X},t_{X},x_{0})=\epsilon(Y,h_{Y},t_{Y},y_{0}).$

Moreover, we can construct a coalgebra structure
$(\textsf{Stream}(A),\textsf{hd},\textsf{tl})$ and show that every coalgebra
structure has a homomorphism into it. From this, we’ll be able to prove the
universal property of the coequalizer: that every function from pointed
coalgebras into any set which respects bisimilarity (i.e. sends bisimilar
pointed coalgebras to equal elements) must factor uniquely through $\epsilon$.

As with structural ends, structural coends permit us to connect the theory of
terminal coalgebras as categorical semantics for coinductive types to our
framework of paranaturality. We can show that the structural coend of a
$T$-coalgebraic difunctor, when it exists, furnishes us with a terminal
coalgebra $(\nu_{T},\textsf{out}_{T})$ for $T$, i.e. a coinductive type.
Indeed, we can generalize Definition 4.7 to get a notion of the structural
coend $\int^{X:\textsf{Set}}\Gamma(X,X)\;\textbf{p}\Theta(X,X)$ with respect
to any difunctor $\Theta$, dually to how we generalized Definition 4.1 to
Definition 4.5. We can then prove a dual version of Lemma 4.6, which, among
other things, has as a corollary that structural coends of coalgebraic
difunctors are terminal coalgebras.

But let us conclude this section by discussing the principle of coinduction, a
crucial component for working with coinductive types. The principle of
coinduction (see e.g. (Ahrens et al., 2015)) states that two terms of a
coinductive type (i.e. a terminal coalgebra) can be identified whenever they
are bisimilar in the appropriate sense. We’ll be able to state our principle
of coinduction for any difunctor whose structural coend exists, which will be
applicable beyond just specifying coinductive types.

We first state a more–general result, and then derive a more familiar
principle of coinduction as a consequence.

###### Definition 4.11.

Given a difunctor
$\Delta\colon\textsf{Set}^{\text{op}}\times\textsf{Set}\to\textsf{Set}$, a
logical relation (or bisimulation) between $\Delta$-structures $(I_{0},d_{0})$
and $(I_{1},d_{1})$ is a relation $R\subseteq I_{0}\times I_{1}$ and a
structure $r\colon\Delta(R,R)$ such that the projection functions
$\pi_{0},\pi_{1}$ are $\Delta$-structure homomorphisms

${(I_{0},d_{0})}$${(R,r)}$${(I_{1},d_{1}).}$$\scriptstyle{\pi_{0}}$$\scriptstyle{\pi_{1}}$

###### Lemma 4.12.

Let $\Delta$ be a difunctor on Set with structural coend $\nu_{\Delta}$, and
let $\eta$ the map sending pointed $\Delta$-structures to their equivalence
class in $\nu_{\Delta}$. If $(I_{0},d_{0},x_{0})$ and $(I_{1},d_{1},x_{1})$
are pointed $\Delta$-structures and $R$ is a bisimulation between
$(I_{0},d_{0})$ and $(I_{1},d_{1})$, then

$x_{0}\;R\;x_{1}\quad\quad\text{implies}\quad\quad\eta(x_{0})=\eta(x_{1}).$

###### Theorem 4.13.

If $\Delta\colon\textsf{Set}^{\text{op}}\times\textsf{Set}\to\textsf{Set}$ has
structural coend $\nu_{\Delta}$, and $R$ is a bisimulation between the
terminal $\Delta$-structure $(\nu_{\Delta},\textsf{out}_{\Delta})$ and itself,
then for any $n,n^{\prime}\colon\nu_{\Delta}$,

$n\;R\;n^{\prime}\quad\quad\text{implies}\quad\quad n=n^{\prime}.$

This provides a practical way to prove equalities between elements of
structural coends. For instance, when working with the $\textsf{Stream}(A)$
type of Example 4.10, it is often convenient to prove the equality of two
streams by coinduction: to prove that $S=S^{\prime}$, it suffices to construct
a relation $R\subseteq\textsf{Stream}(A)\times\textsf{Stream}(A)$ which is a
bisimulation from $(\textsf{Stream}(A),\textsf{hd},\textsf{tl})$ to itself
such that $S\;R\;S^{\prime}$. In the case of streams, $R$ is a bisimulation
if, for every $T,T^{\prime}\colon\textsf{Stream}(A)$,

$T\;R\;T^{\prime}\quad\quad\text{implies}\quad\quad\textsf{hd}(T)=\textsf{hd}(T^{\prime})\quad\text{and}\quad(\textsf{tl}\;T)\;R\;(\textsf{tl}\;T^{\prime}).$

But our examples are not confined to just coinductive types: it also allows us
to discuss representation independence in the sense of (Mitchell, 1986). The
following is a classic example.

###### Example 4.14.

For $A\colon\textsf{Set}$, define the $A$-queue data difunctor by

$\textsf{QData}(X^{-},X^{+}):\equiv X^{+}\times(A\times X^{-}\to
X^{+})\times(X^{-}\to\textsf{Maybe}(A\times X^{+}))$

where Maybe is the $X\mapsto\mathbf{1}+X$ endofunctor; we’ll use the Haskell-
like notation of $\textsf{Nothing}\colon\textsf{Maybe}(X)$ and
$\textsf{Just}\colon X\to\textsf{Maybe}(X)$ for the constructors of
$\textsf{Maybe}(X)$. A QData-Struct is an implementation of $A$-queues: a set
$Q$ (the type of queues) equipped with:

$\varepsilon\colon Q\qquad enq\colon A\times Q\to Q\qquad deq\colon
Q\to\textsf{Maybe}(A\times Q)$

corresponding to the empty queue, the enqueue operation, and the dequeue
operation, respectively.

Now suppose we have two such implementations
$(Q_{0},\varepsilon_{0},enq_{0},deq_{0})$ and
$(Q_{1},\varepsilon_{1},enq_{1},deq_{1})$. Observe that $R\subseteq
Q_{0}\times Q_{1}$ is a bisimulation between
$(Q_{0},\varepsilon_{0},enq_{0},deq_{0})$ and
$(Q_{1},\varepsilon_{1},enq_{1},deq_{1})$ if the following hold:

  * •

$\varepsilon_{0}\;R\;\varepsilon_{1}$;

  * •

if $q_{0}\;R\;q_{1}$, then, for any $a:A$,
$(enq_{0}(a,q_{0}))\;R\;(enq_{1}(a,q_{1}))$;

  * •

if $q_{0}\;R\;q_{1}$, then either
$deq_{0}(q_{0})=\textsf{Nothing}=deq_{1}(q_{1})$ or else
$deq_{0}(q_{0})=\textsf{Just}(a_{0},q_{0}^{\prime})$ and
$deq_{1}(q_{1})=\textsf{Just}(a_{1},q_{1}^{\prime})$ such that $a_{0}=a_{1}$
and $q_{0}^{\prime}\;R\;q_{1}^{\prime}$.

Now apply Lemma 4.12: if we have such a bisimulation $R$ and $q_{0}\colon
Q_{0}$, $q_{1}\colon Q_{1}$ such that $q_{0}\;R\;q_{1}$, then $q_{0}$ and
$q_{1}$ are equal as elements of
$\int^{X:\textsf{Set}}\textsf{QData}(X,X)\;\textbf{p}X$.

What this says is that the quotient forming
$\int^{X:\textsf{Set}}\textsf{QData}(X,X)\;\textbf{p}X$ identifies pointed
queue implementations which are behaviorally indistinguishable: if $R$ is a
bisimulation, then, as mentioned above, it relates the empty queues of the two
representations, is preserved in any application of the enqueue operation, and
ensures indistinguishable results upon dequeueing. So a user who’s allowed to
start with the empty queue and then queue/dequeue to their heart’s content
with various elements of $A$ could never distinguish between bisimilar
implementations. The quotient makes this explicit by identifying pointed
queues which are equivalent in this way, thus functioning as the existential
type $\exists X.\textsf{QData}(X,X)$. As detailed in e.g. (Angiuli et al.,
2020), this is advantageous for the design and specification of software
libraries: a simple but slow implementation of queues (e.g. the single-stack
implementation) can be used for specification purposes, but in practice
replaced by a more efficient, provably-bisimilar implementation (e.g. the
double-stack implementation), with the representation independence result
guaranteeing that the user will never see the difference.

##  5\. A Difunctor Model of Type Theory

Finally, we’ll explore another branch of research which can potentially
benefit from the ideas and insights of paranatural category theory: the
categorical semantics of type theory. As is the case with the classical model
theory of logic, the study of semantics for type theory stems from a need to
prove metatheoretic results such as consistency or independence. Following in
the tradition of (Lawvere, 1963), such semantics investigations frequently
utilized category theory, as it often proved quite suitable for modelling type
theory (e.g. in the landmark result of (Lambek, 1980)). For dependent type
theory (in the style of (Martin-Löf, 1975, 1982)) in particular, a number of
category-theoretic notions of model of dependent type theory flourished (see
(Hofmann, 1997; nLab authors, 2023a) for a summary), and were used to
establish key metatheoretic results about dependent type theory (Hofmann and
Streicher, 1995). In this section, we’ll be using category with families
(CwFs) (Dybjer, 1995) as our notion of a model of type theory.

A model of a given theory is an interpretation of the syntax of the theory
into mathematical structures. In type theory, the syntactic objects which we
must interpret are contexts, substitutions, types, and terms, along with the
various operations for forming, combining, transforming, and inter-converting
these. A CwF is a straightforward rendering of these as a category-theoretic
structure: to define a CwF, we must supply a category (whose objects will
interpret contexts, and whose morphisms will interpret substitutions), a
presheaf on that category (whose object part sends contexts to their set of
types, and whose morphism part represents the substitution of free variables
in a type), a presheaf on the category of elements of that presheaf (sending a
context and a type to the set of terms of that type, also with an action under
substitution), as well as an appropriate operation on objects (interpreting
the extension of a context by a typed variable). So, while being deeply
category-theoretic, CwFs manage to stay very close to the syntax of type
theory they are designed to interpret.

One particularly fruitful class of models of dependent type theory are
presheaf models (see (Hofmann, 1997, Sect. 4) for a detailed definition),
which forms the basic semantics for many type theories of interest, e.g.
(Bezem et al., 2014). In a presheaf model, the category of contexts and
substitutions is taken to be $\hat{\mathbb{C}}$, the category of presheaves
(hence the name) and natural transformations on some fixed category
$\mathbb{C}$. Among the many useful features of such a model is the fact that
the Yoneda Lemma makes it expedient to import the Grothendieck universes of
the metatheory (see explanation below) into the syntax as type universes—a
process referred to as lifting these universes in (Hofmann and Streicher,
1999). Since the difunctor category
$\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$ generalizes the
category of presheaves, particularly by having its own Yoneda Lemma (Lemma
2.13), the question naturally arises whether we can formulate a difunctor
model of type theory which also permits the lifting of Grothendieck universes.
The purpose of the present section is to answer this affirmatively.

To do so, it will be helpful to generalize the definition of paranatural
transformation to dependent paranatural transformations.

###### Definition 5.1.

Given a difunctor
$\Gamma\colon\mathbb{C}^{\text{op}}\times\mathbb{C}\to\textsf{Set}$ and a
difunctor over $\Gamma$, i.e.
$A:\left({\Gamma}\textsf{-Struct}\right)^{\text{op}}\times{\Gamma}\textsf{-Struct}\to\textsf{Set}$,
a dependent paranatural transformation

$\tau\colon\left(C\colon{\Gamma}\textsf{-Struct}\right)\xrightarrow{\diamond}A(C,C)$

is a $\left|\mathbb{C}\right|$-indexed family of dependent functions

$\tau_{I}\colon(c\colon\Gamma(I,I))\to A((I,c),(I,c))$

satisfying

$\Gamma(I_{0},i_{2})\;c_{0}=\Gamma(i_{2},I_{1})\;c_{1}\quad\quad\text{implies}\quad\quad\textsf{map}^{+}_{A}\;i_{2}\;(\tau_{I_{0}}\;c_{0})=\textsf{map}^{-}_{A}\;i_{2}\;(\tau_{I_{1}}\;c_{1})$

for every $I_{0},I_{1}:\left|\mathbb{C}\right|$,
$i_{2}\colon\mathbb{C}(I_{0},I_{1})$, $c_{0}\colon\Gamma(I_{0},I_{0})$ and
$c_{1}\colon\Gamma(I_{1},I_{1})$. The antecedent says that $i_{2}$ is a
${\Gamma}\textsf{-Struct}$-morphism from $(I_{0},c_{0})$ to $(I_{1},c_{1})$,
hence why it is well-typed to apply the (positive and negative) morphism parts
of $A$ to $i_{2}$ in the consequent.

True to their name, dependent paranatural transformations serve as the
dependent analogue of paranatural transformations: instead of having a family
of simple functions $\phi_{I}$ sending $\Delta$-structures on $I$ to
$\Gamma$-structures on $I$, we have dependent functions $\tau_{I}$ sending
$\Gamma$-structures $c$ on $I$ to $A$-structures on $(I,c)$. But besides this
change (and the necessary changes to the paranaturality condition), this
notion is the same. Indeed, if $A$ is merely a difunctor on $\mathbb{C}$, i.e.
it ignores its $\Gamma$-structure arguments, then this is just the usual
notion of paranatural transformation.

One minor point on notation: readers who prefer the integral notation of
Definition 4.5 might prefer to write the type of dependent paranatural
transformations from $\Gamma$ to $A$ as

$\int_{I\colon\mathbb{C}}(c\colon\Gamma(I,I))\;\textbf{d}A\;(I,c)\;(I,c).$

In what follows, we’ll use the $\xrightarrow{\diamond}$ notation, but
sometimes the integral notation is easier to understand, analogously to how
the integral notation for ends often makes it easier to reason about dependent
natural transformations.

Now, the definition of difunctor models is as follows.

###### Definition 5.2.

For any category $\mathbb{C}$, the difunctor model of type theory (over
$\mathbb{C}$) is defined as follows.

  * •

Contexts are difunctors
$\Gamma:\mathbb{C}^{\text{op}}\times\mathbb{C}\to\textsf{Set}$ and
substitutions $\gamma\colon\textsf{Sub}(\Delta,\Gamma)$ are paranatural
transformations $\Delta\xrightarrow{\diamond}\Gamma$.

  * •

The empty context $\blacklozenge$ is the terminal object of
$\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$, the
constant-$\mathbf{1}$ difunctor.

  * •

A type $A:\textsf{Ty}\;\Gamma$ is a difunctor over $\Gamma$, i.e.
$A\colon\left({\Gamma}\textsf{-Struct}\right)^{\text{op}}\times{\Gamma}\textsf{-Struct}\to\textsf{Set}$.

  * •

Given $A\colon\textsf{Ty}\;\Gamma$ and
$\gamma\colon\textsf{Sub}(\Delta,\Gamma)$, define
$A[\gamma]\colon\textsf{Ty}\;\Delta$ by

$A[\gamma](D,D^{\prime}):\equiv
A\left(\underline{\gamma}\;D,\;\underline{\gamma}\;D^{\prime}\right)$

for any $D,D^{\prime}\colon{\Delta}\textsf{-Struct}$ (recall
$\underline{\gamma}\colon{\Delta}\textsf{-Struct}\to{\Gamma}\textsf{-Struct}$
is the functor corresponding to $\gamma$, by Proposition 2.9).

  * •

For $A\colon\textsf{Ty}\;\Gamma$, define $\textsf{Tm}(\Gamma,A)$ to be the set
of dependent paranatural transformations

$\tau\colon\left(C\colon{\Gamma}\textsf{-Struct}\right)\xrightarrow{\diamond}A(C,C).$

Define the morphism part
$-[\gamma]\colon\textsf{Tm}(\Gamma,A)\to\textsf{Tm}(\Delta,A[\gamma])$
similarly to the morphism part of Ty.

  * •

To define the context extension $\Gamma.A$, we’ll use diYoneda reasoning. We
want $\Gamma.A$ to satisfy:

$\textsf{Sub}\;\Delta\;\Gamma.A\quad\cong\quad\sum_{\gamma\colon\textsf{Sub}(\Delta,\Gamma)}\textsf{Tm}(\Delta,A[\gamma]).$

So apply the diYoneda Lemma:

$\displaystyle\Gamma.A(I,J)$
$\displaystyle\cong\textsf{Sub}\;(\textbf{yy}(J,I))\;\Gamma.A$
$\displaystyle\cong\sum_{\gamma\colon\textsf{Sub}(\textbf{yy}(J,I),\Gamma)}\textsf{Tm}(\textbf{yy}(J,I),A[\gamma])$
$\displaystyle\cong\sum_{g\colon\Gamma(I,J)}\textsf{Tm}(\textbf{yy}(J,I),A[\alpha_{g}])$

where $\alpha_{g}$ is the paranatural transformation
$\textbf{yy}(J,I)\xrightarrow{\diamond}\Gamma$ corresponding to
$g\colon\Gamma(I,J)$, like we used in the proof of Lemma 2.13. Applying the
definition of $\alpha$ and cleaning up a bit, we can come up with the
definition

$\Gamma.A(I,J):\equiv\sum_{g\colon\Gamma(I,J)}((K,\textsf{into}_{K},\textsf{from}_{K})\colon
J/\mathbb{C}/I)\xrightarrow{\diamond}A\;(K,g^{\prime})\;(K,g^{\prime})$

where $g^{\prime}\colon\Gamma(K,K)$ is given by
$\textsf{map}^{-}_{\Gamma}\;\textsf{from}_{K}\;(\textsf{map}^{+}_{\Gamma}\;\textsf{into}_{K}\;g)$.

This definition of $\Gamma.A$ is somewhat unsatisfying. In the presheaf case,
we’re able to make use of a dependent Yoneda Lemma to rephrase the
corresponding expression—which involves a dependent natural transformation out
of a representable presheaf—into a compact expression. However, it’s unclear
what the difunctorial/paranatural analogue of the dependent Yoneda Lemma ought
to be. We leave it to future work to clarify this point.

As we did in the first few sections, we have been neglecting concerns about
whether given collections are too big to be sets. For instance, there’s
nothing to ensure that the collection $\textsf{Ty}\;\Gamma$ of all difunctors
over $\Gamma$ constitutes a set, so we leave ourselves open to paradox by
assuming it is. Unlike Section 4, it is not suitable for our present purpose
to carefully avoid making existence claims. Rather, we’ll adopt a standard
approach in category theory for handling size issues: Grothendieck universes
(see (nLab authors, 2023b) for an introduction and references). What a
Grothendieck universe consists of is a set $\mathcal{U}$ of small sets which
is closed under all the usual operations on sets (e.g. cartesian product,
function, power sets). If we assume our metatheory has a Grothendieck universe
$\mathcal{U}$, then we can make the following two restrictions, and they will
guarantee that each $\textsf{Ty}\;\Gamma$ indeed constitutes a set.

  * •

$\mathbb{C}$ itself needs to a small category, i.e.
$\left|\mathbb{C}\right|\colon\mathcal{U}$ and each hom-set is in
$\mathcal{U}$.

  * •

$\textsf{Ty}\;\Gamma$ is actually the collection of all small difunctors on
$\Gamma$, that is, difunctors
$A\colon({\Gamma}\textsf{-Struct})^{\text{op}}\times{\Gamma}\textsf{-Struct}\to\textsf{Set}$
such that $A(C,C^{\prime})\colon\mathcal{U}$ for all $\Gamma$-structures
$C,C^{\prime}$.

Together, these also allow us to deduce that each $\textsf{Tm}(\Gamma,A)$
constitutes a set, freeing this construction from paradox.

While avoiding paradoxes is certainly important, assuming a Grothendieck
universe $\mathcal{U}$ in our metatheory and using it in the definition of the
difunctor model has a more exciting implication: we can ‘lift’ this
Grothendieck universe into the syntax of our type theory as a type-theoretic
universe.

###### Proposition 5.3.

In the difunctor model, there exists a closed type U such that, for all
contexts $\Gamma$,

(11) $\textsf{Tm}(\Gamma,\textbf{U})\cong\textsf{Ty}\;\Gamma$

So U acts as a type of all types. To avoid another paradox (due to (Girard,
1972), but conceptually related to the earlier paradoxes of Russell and
Burali–Forti), U actually must be a large type, that is, a difunctor
$({\blacklozenge}\textsf{-Struct})^{\text{op}}\times{\blacklozenge}\textsf{-Struct}\to\textsf{Set}$,
without the size restriction on the codomain. So U itself is not included in
the right-hand side of Equation 11, and hence U doesn’t contain itself. Note
that ${\blacklozenge}\textsf{-Struct}$ is isomorphic to just $\mathbb{C}$
itself, so we’ll describe U as just a difunctor over $\mathbb{C}$.

###### Proof.

By diYoneda reasoning. Suppose such a U existed. Then,

(diYoneda Lemma) $\displaystyle\textbf{U}(I,J)$
$\displaystyle\cong(\textbf{yy}(J,I)\xrightarrow{\diamond}\textbf{U})$ (U is a
closed type) $\displaystyle\cong\textsf{Tm}(\textbf{yy}(J,I),\textbf{U})$
(Equation 11) $\displaystyle\cong\textsf{Ty}(\textbf{yy}(J,I))$ (12)
$\displaystyle\equiv\left({\textbf{yy}(J,I)}\textsf{-Struct}\right)^{\text{op}}\times\left({\textbf{yy}(J,I)}\textsf{-Struct}\right)\to\mathcal{U}$
(13)
$\displaystyle\equiv(J/\mathbb{C}/I)^{\text{op}}\times(J/\mathbb{C}/I)\to\mathcal{U}$

So define $\textbf{U}(I,J)$ to be the set of (small) difunctors on the splice
category $J/\mathbb{C}/I$. ∎

The line labelled U is a closed type refers to the fact that we can weaken a
type in the empty context to a type in arbitrary context by ignoring further
arguments (hence why it makes sense to write
$\textsf{Tm}(\textbf{yy}(J,I),\textbf{U})$ when U is a type in context
$\blacklozenge$), and, as mentioned above, a dependent paranatural
transformation whose codomain doesn’t actually depend on the structure
argument of the domain is just a usual paranatural transform.

Thus, we have the beginnings of a model of type theory: a CwF interpreting the
basic syntax of type theory, plus a type universe. But much remains to be
done. Analogously to the presheaf model, it seems that this model can give
semantics for a stock of basic types, plus more sophisticated constructions
like dependent sums, dependent products, and identity types. Part of the hope
we have for this model is that it will allow us to simultaneously benefit from
the richness of the presheaf model (as we’ve already seen), but also be able
to leverage the deep ties to parametricity which come from paranaturality. But
further investigation is most definitely needed.

##  6\. Conclusion and Future Directions

What we have developed in this article is a small but powerful theory, which
will hopefully serve as the core of a more expansive branch of category
theory. Without the addition of paranatural transformations, category lacks
adequate tools to properly treat difunctors: natural transformations are too
strong, and dinatural transformations are too weak. Paranatural
transformations strike a delicate balance, privileging the difunctor’s
diagonal but not neglecting the off-diagonal. By doing so, they manage to
replicate all the intricate structure category theorists are accustomed to
from presheaves–particularly Yoneda-style reasoning–but in a way which
simultaneously handles both co- and contra-variance. To the author’s
knowledge, this paper gives the first instances of this diYoneda reasoning,
but certainly there are many more of interest.

Hopefully future work will continue to develop paranatural category theory,
further along the lines of the standard category theory, and beyond. We have
not endeavored to study adjunctions in the paranatural setting, but suspect
that they will prove interesting. We alluded to the possibility that
$\mathrel{\mathop{\mathbb{C}}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\diamond$}\vss}}}$ would admit a
subobject classifier, but have not explored paranatural topos theory to any
appreciable extent. As briefly discussed at the end of Section 3, the theory
of multivariable difunctors is presently lacking systematic development, e.g.
a Fubini theorem for structural ends. Section 5 furthermore mentioned the
question of how to formulate a dependent diYoneda Lemma, which also remains
open. Finally, we have confined ourselves entirely to 1-category theory in the
present work; undoubtedly there are numerous interesting research avenues
involving paranatural analogues of higher category theory and enriched
category theory.

After establishing the basic theory in Section 2, we endeavored to justify the
need for such a theory by developing connections to three branches of
research: parametricity, category-theoretic semantics of (co)inductive types,
and category-theoretic semantics of type theory. For parametricity, we were
able to use paranaturality to replicate the famous free theorems of Wadler by
interpreting System F into paranatural category theory. This task is still
incomplete. As mentioned, a theory of multivariable difunctors and paranatural
transformations will be needed to interpret the full range of polymorphic
types available in System F. More significantly, we presently lack a concrete
result connecting our parametricity theorem to the existing formulations in
the relational parametricity literature. Further work is needed to either
demonstrate that our notion of parametricity exactly coincides with the
relational one, or else clearly delineate where they differ. Beyond this,
there is work to be done to extend these results to richer and more elaborate
languages than System F, such as parametric dependent type theories (e.g.
(Bernardy et al., 2010, 2012)).

In Section 4, we saw that special instances of paranatural transformations
gave us impredicative encodings of inductive types, by taking the structural
end of the appropriate algebraic difunctor. Moreover, this formulation made it
convenient to dualize, which gave us structural coends, a paranatural
framework for reasoning about coinductive and existential types. Several
topics warrant further study: characterizing which difunctors have structural
(co)ends, analogously to the theory of containers/polynomial endofuctors;
giving a paranatural analysis of (co)monads and their (co)algebras; extending
this study to more exotic kinds of inductive types, such as higher inductive
types, inductive-recursive types, inductive-inductive types, and so on.

Finally, we introduced difunctor models of type theory and showed that, by
virtue of the diYoneda Lemma, we could lift Grothendieck universes in our
metatheory to type-theoretic universes in the syntax interpreted by these
models. As mentioned, work is needed to fully elaborate the type theory which
is interpreted by difunctor models. In particular, it remains unclear how the
parametricity encoded by difunctors and paranatural transformations is
reflected syntactically in the type theory interpreted by difunctor models.
Another question which the present author is keen to explore is how the
insight of (Hofmann, 1999)—that presheaf models are well-suited for
interpreting higher order abstract syntax—can be copied over to the difunctor
model.

## References

  * (1)
  * Adámek (1974) Jivrí Adámek. 1974\.  Free algebras and automata realizations in the language of categories.  _Commentationes Mathematicae Universitatis Carolinae_ 15, 4 (1974), 589–602.
  * Ahrens et al. (2015) Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. 2015\.  Non-wellfounded trees in homotopy type theory.  _arXiv preprint arXiv:1504.02949_ (2015).
  * Angiuli et al. (2020) Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner. 2020.  Internalizing representation independence with univalence.  _arXiv preprint arXiv:2009.05547_ (2020).
  * Awodey et al. (2018) Steve Awodey, Jonas Frey, and Sam Speight. 2018.  Impredicative encodings of (higher) inductive types. In _Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science_. 76–85.
  * Bainbridge et al. (1990) Edwin S Bainbridge, Peter J. Freyd, Andre Scedrov, and Philip J. Scott. 1990.  Functorial polymorphism.  _Theoretical computer science_ 70, 1 (1990), 35–64.
  * Bernardy et al. (2010) Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. 2010\.  Parametricity and dependent types. In _Proceedings of the 15th ACM SIGPLAN international conference on Functional programming_. 345–356.
  * Bernardy et al. (2012) Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. 2012\.  Proofs for free: Parametricity for dependent types.  _Journal of Functional Programming_ 22, 2 (2012), 107–152.
  * Bezem et al. (2014) Marc Bezem, Thierry Coquand, and Simon Huber. 2014\.  A model of type theory in cubical sets. In _19th International conference on types for proofs and programs (TYPES 2013)_ , Vol. 26. 107–128.
  * Dubuc and Street (1970) Eduardo Dubuc and Ross Street. 1970.  Dinatural transformations. In _Reports of the Midwest Category Seminar IV_. Springer, 126–137.
  * Dybjer (1995) Peter Dybjer. 1995\.  Internal type theory. In _International Workshop on Types for Proofs and Programs_. Springer, 120–134.
  * Eppendahl (1999) A Eppendahl. 1999\.  Parametricity and Mulry’s Strong.  (1999).
  * Girard (1972) Jean-Yves Girard. 1972\.  _Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur_.  Ph. D. Dissertation. Éditeur inconnu.
  * Girard (1986) Jean-Yves Girard. 1986\.  The system F of variable types, fifteen years later.  _Theoretical computer science_ 45 (1986), 159–192.
  * Hackett and Hutton (2015) Jennifer Hackett and Graham Hutton. 2015.  Programs for cheap!. In _2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science_. IEEE, 115–126.
  * Hermida et al. (2014) Claudio Hermida, Uday S Reddy, and Edmund P Robinson. 2014\.  Logical relations and parametricity–a Reynolds programme for category theory and programming languages.  _Electronic Notes in Theoretical Computer Science_ 303 (2014), 149–180.
  * Hofmann (1997) Martin Hofmann. 1997\.  Syntax and semantics of dependent types.  In _Extensional Constructs in Intensional Type Theory_. Springer, 13–54.
  * Hofmann (1999) Martin Hofmann. 1999\.  Semantical analysis of higher-order abstract syntax. In _Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158)_. IEEE, 204–213.
  * Hofmann and Streicher (1995) Martin Hofmann and Thomas Streicher. 1995.  The groupoid interpretation of type theory.  _Twenty-five years of constructive type theory (Venice, 1995)_ 36 (1995), 83–111.
  * Hofmann and Streicher (1999) Martin Hofmann and Thomas Streicher. 1999.  Lifting grothendieck universes.  _Unpublished note_ 199 (1999), 3.
  * Lambek (1980) Joachim Lambek. 1980\.  From lambda-calculus to cartesian closed categories.  _To HB Curry: essays on combinatory logic, lambda calculus and formalism_ (1980), 375–402.
  * Lawvere (1963) F William Lawvere. 1963\.  Functorial semantics of algebraic theories.  _Proceedings of the National Academy of Sciences_ 50, 5 (1963), 869–872.
  * Mac Lane (1978) Saunders Mac Lane. 1978\.  _Categories for the Working Mathematician_.  Springer New York.  https://doi.org/10.1007/978-1-4757-4721-8
  * MacLane and Moerdijk (2012) Saunders MacLane and Ieke Moerdijk. 2012.  _Sheaves in geometry and logic: A first introduction to topos theory_.  Springer Science & Business Media.
  * Martin-Löf (1975) Per Martin-Löf. 1975\.  An Intuitionistic Theory of Types: Predicative Part.  In _Logic Colloquium ’73_ , H.E. Rose and J.C. Shepherdson (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 80. Elsevier, 73–118.  https://doi.org/10.1016/S0049-237X(08)71945-1
  * Martin-Löf (1982) Per Martin-Löf. 1982\.  Constructive Mathematics and Computer Programming.  In _Logic, Methodology and Philosophy of Science VI_ , L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, and Klaus-Peter Podewski (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 104. Elsevier, 153–175.  https://doi.org/10.1016/S0049-237X(09)70189-2
  * Mitchell (1986) John C Mitchell. 1986\.  Representation independence and data abstraction. In _Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages_. 263–276.
  * Mulry (1992) Philip S Mulry. 1992\.  Strong monads, algebras and fixed points.  _Applications of Categories in Computer Science_ 177 (1992), 202–216.
  * Neumann (2022) Jacob Neumann. 2022\.  (Co)ends and (Co)structure. (1 Dec. 2022).  https://www.youtube.com/watch?v=X4v5HnnF2-o Homotopy Type Theory Electronic Seminar Talks (HoTTEST).
  * nLab authors (2023a) nLab authors. 2023a.  categorical semantics of dependent type theory.  https://ncatlab.org/nlab/show/categorical+semantics+of+dependent+type+theory.  Revision 70.
  * nLab authors (2023b) nLab authors. 2023b.  Grothendieck universe.  https://ncatlab.org/nlab/show/Grothendieck+universe.  Revision 57.
  * Paré and Román (1998) Robert Paré and Leopoldo Román. 1998.  Dinatural numbers.  _Journal of Pure and Applied Algebra_ 128, 1 (1998), 33–92.
  * Pohlová (1973) Vvera Pohlová. 1973\.  On sums in generalized algebraic categories.  _Czechoslovak Mathematical Journal_ 23, 2 (1973), 235–251.
  * Reynolds (1974) John C Reynolds. 1974\.  Towards a theory of type structure. In _Programming Symposium: Proceedings, Colloque sur la Programmation Paris, April 9–11, 1974_. Springer, 408–425.
  * Reynolds (1983) John C Reynolds. 1983\.  Types, abstraction and parametric polymorphism. In _Information Processing 83, Proceedings of the IFIP 9th World Computer Congres_. 513–523.
  * Scott (2000) Phill J Scott. 2000\.  Some aspects of categories in computer science.  In _Handbook of algebra_. Vol. 2. Elsevier, 3–77.
  * Strachey (2000) Christopher Strachey. 2000\.  Fundamental concepts in programming languages.  _Higher-order and symbolic computation_ 13 (2000), 11–49.
  * Univalent Foundations Program (2013) The Univalent Foundations Program. 2013\.  _Homotopy Type Theory: Univalent Foundations of Mathematics_.  https://homotopytypetheory.org/book, Institute for Advanced Study.
  * Uustalu (2000) Tarmo Uustalu. 2000\.  Strong dinaturality and initial algebras.  _12th Nordic Wksh. on Programming Theory, NWPT_ 2 (2000).
  * Uustalu (2010) Tarmo Uustalu. 2010\.  A Note on Strong Dinaturality, Initial Algebras and Uniform Parameterized Fixpoint Operators.. In _FICS_. 77–82.
  * Vene (2006) Varmo Vene. 2006\.  Parametricity and Strong Dinaturality. (2006).  https://www.ioc.ee/~tarmo/tday-voore/vene-slides.pdf Teooriapäevad Voorel.
  * Wadler (1989) Philip Wadler. 1989\.  Theorems for free!. In _Proceedings of the fourth international conference on Functional programming languages and computer architecture_. 347–359.