Di- is for Directed: First-Order Directed Type Theory via Dinaturality

TL;DR

This paper develops a first-order directed type theory using dinaturality, interpreting types as categories and directed equality via hom-functors, with formal proofs in Agda.

Contribution

It introduces a novel interpretation of directed type theory based on dinaturality, including a new elimination principle and categorical characterizations of directed equality.

Findings

Characterizes directed equality as a left relative adjoint.

Formalizes interpretation of quantifiers as ends and coends.

Proves key categorical properties like Fubini rule and Yoneda lemma.

Abstract

We show how dinaturality plays a central role in the interpretation of directed type theory where types are interpreted as (1-)categories and directed equality is represented by $\hom$-functors. We present a general elimination principle based on dinaturality for directed equality which very closely resembles the $J$-rule used in Martin-L\"of type theory, and we highlight which syntactical restrictions are needed to interpret this rule in the context of directed equality. We then use these rules to characterize directed equality as a left relative adjoint to a functor between (para)categories of dinatural transformations which contracts together two variables appearing naturally with a single dinatural one, with the relative functor imposing the syntactic restrictions needed. We then argue that the quantifiers of such a directed type theory should be interpreted as ends and coends, which dinaturality allows us to present in adjoint-like correspondences to a weakening functor. Using these rules we give a formal interpretation to Yoneda reductions and (co)end calculus, and we use logical derivations to prove the Fubini rule for quantifier exchange, the adjointness property of Kan extensions via (co)ends, exponential objects of presheaves, and the (co)Yoneda lemma. We show transitivity (composition), congruence (functoriality), and transport (coYoneda) for directed equality by closely following the same approach of Martin-L\"of type theory, with the notable exception of symmetry. We formalize our main theorems in Agda.