2 papers
cs.LO2025
A Judgmental Construction of Directed Type Theory
Jacob Neumann
We reformulate recent advances in directed type theory--a type theory where the types have the structure of synthetic (higher) categories--as a logical calculus with multiple conte…
math.CT2024
Synthetic 1-Categories in Directed Type Theory
Thorsten Altenkirch, Jacob Neumann
The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin…