一句话：提出一阶有向类型论，以范畴与双自然变换解释有向相等，并借助双自然性刻画 J 规则与 (co)end 量词。
本文研究有向类型论的语义与证明论：类型解释为 (1-)范畴，项为函子，谓词为双预层，证明相关的蕴含为双自然变换。作者提出一阶有向类型论，其有向相等的消去原理受双自然性启发，形似 Martin-Löf 类型论的 J 规则，并带有简单句法限制，从而恢复除对称性外的对称相等定理。双自然性用于证明传递、同余与传输，如同 MLTT。文章进一步论证有向类型论的量词应解释为 end 与 coend，形式化 (co)end 演算与 Yoneda 归约，并给出 (co)Yoneda 引理、Kan 扩张伴随性、预层指数对象及 Fubini 交换律的逻辑证明。主要定理已在 Agda 中形式化。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{LarettoLV26,
title = {Di- is for Directed: First-Order Directed Type Theory via Dinaturality},
author = {Andrea Laretto and Fosco Loregian and Niccolò Veltri},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776703}
}