TY  - RPRT
TI  - Di- is for Directed: First-Order Directed Type Theory via Dinaturality
AU  - Andrea Laretto
AU  - Fosco Loregian
AU  - Niccolò Veltri
PY  - 2026
DO  - 10.1145/3776703
UR  - https://arxiv.org/abs/2409.10237
ID  - 2409.10237
ER  -