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.

翻译：本文阐述了双自然性在定向类型论解释中的核心作用，其中类型被解释为（1-）范畴，而定向等式则由 $\hom$-函子表示。我们提出了一种基于双自然性的定向等式通用消去原理，该原理与 Martin-Löf 类型论中使用的 $J$-规则高度相似，并阐明了在定向等式语境下解释此规则所需的语法限制。随后，我们运用这些规则将定向等式刻画为双自然变换（副）范畴间函子的左相对伴随，该函子将两个自然出现的变量与一个双自然变量收缩在一起，而相对函子则施加了所需的语法限制。进而，我们论证了此类定向类型论的量词应解释为端和余端，双自然性使我们能够以伴随式对应关系将其呈现于弱化函子。利用这些规则，我们为 Yoneda 约化与（余）端演算提供了形式化解释，并通过逻辑推导证明了量词交换的 Fubini 规则、Kan 扩张通过（余）端的伴随性、预层的指数对象以及（余）Yoneda 引理。通过严格遵循 Martin-Löf 类型论的相同进路（对称性除外），我们展示了定向等式的传递性（复合性）、同余性（函子性）与迁移性（余 Yoneda 性）。我们的主要定理已在 Agda 中形式化实现。