Di- is for Directed: First-Order Directed Type Theory via Dinaturality
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öf 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öf type theory, with the notable exception of symmetry. We formalize our main theorems in Agda.