We show how dinaturality plays a central role in the interpretation of directed type theory where types are given by (1-)categories and directed equality by hom-functors. We introduce a first-order directed type theory where types are semantically interpreted as categories, terms as functors, predicates as dipresheaves, and proof-relevant entailments as dinatural transformation. This type theory is equipped with an elimination principle for directed equality, motivated by dinaturality, which closely resembles the J -rule used in Martin-Löf type theory. This directed J -rule comes with a simple syntactic restriction which recovers all theorems about symmetric equality, except for symmetry. Dinaturality is used to prove properties about transitivity (composition), congruence (functoriality), and transport (coYoneda) in exactly the same way as in Martin-Löf type theory, and allows us to obtain an internal “naturality for free”. We then argue that the quantifiers of directed type theory should be ends and coends, which dinaturality allows us to capture formally. Our type theory provides a formal treatment to (co)end calculus and Yoneda reductions, which we use to give distinctly logical proofs to the (co)Yoneda lemma, the adjointness property of Kan extensions via (co)ends, exponential objects of presheaves, and the Fubini rule for quantifier exchange. Our main theorems are formalized in Agda.

Abstract We study generalised automata (in the sense of Adámek and Trnková) in Joyal’s category of (set-valued) combinatorial species, and as an important preliminary step, we study coalgebras for its derivative endofunctor $\partial$ and for the ‘Euler homogeneity operator’ $L\circ \partial$ arising from the adjunction $L\dashv \partial \dashv R$ . The theory is connected with, and in fact provides relatively nontrivial examples of, differential 2-rigs , a notion recently introduced by the author putting combinatorial species on the same relation a generic (differential) semiring $(R,d)$ has with the (differential) semiring $\mathbb{N}[\![ X]\!]$ of power series with natural coefficients. The desire to study categories of ‘state machines’ valued in an ambient monoidal category $(\mathcal{K},\otimes )$ gives a pretext to further develop the abstract theory of differential 2-rigs, proving lifting theorems of a differential 2-rig structure from $(\mathcal{R},\partial )$ to the category of $\partial$ -algebras on objects of $\mathcal{R}$ and to categories of Mealy automata valued in $(\mathcal{R},\otimes )$ , as well as various constructions inspired by differential algebra such as jet spaces and modules of differential operators. These theorems adapt to various ‘species-like’ categories such as coloured species, $k$ -vector species (both used in operad theory), linear species (introduced by Leroux to study combinatorial differential equations), Möbius species and others.

We present a slick proof of completeness and cocompleteness for categories of F-automata, where the span of maps E ←d E⊗ I s→ O that usually defines a deterministic automaton of input I and output O in a monoidal category (K,⊗) is replaced by a span E ← FE → O for a generic endofunctor F : K → K of a generic category K: these automata exist in their "Mealy" and "Moore" version and form categories F-Mly and F-Mre; such categories can be presented as strict 2-pullbacks in Cat and whenever F is a left adjoint, both F-Mly and F-Mre admit all limits and colimits that K admits. We mechanize our main results using the proof assistant Agda and the library https://github.com/agda/agda-categories.

We provide a Lawvere-style definition for partial theories, extending the classical notion of equational theory by allowing partially defined operations. As in the classical case, our definition is syntactic: we use an appropriate class of string diagrams as terms. This allows for equational reasoning about the class of models defined by a partial theory. We demonstrate the expressivity of such equational theories by considering a number of examples, including partial combinatory algebras and cartesian closed categories. Moreover, despite the increase in expressivity of the syntax we retain a well-behaved notion of semantics: we show that our categories of models are precisely locally finitely presentable categories, and that free models exist.