Di- is for Directed: First-Order Directed Type Theory via Dinaturality
Andrea Laretto
Tallinn University of Technology
Abstract: This talk will be a practice talk for my presentation at POPL 2026.
Talk length will surely be under 30 minutes, and it's going to have very modest prerequisites (with little to no new material which I have not presented before).
So if you're curious about directed type theory and what I do please come by and give your feedback!
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.