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

Andrea Laretto, Fosco Loregian, Niccolò Veltri

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 $\…