Synthetic 1-Categories in Directed Type Theory
Thorsten Altenkirch, Jacob Neumann
TL;DR
This work develops a semantics-driven foundation for directed type theory aimed at synthetic (higher) category theory by moving from symmetric identity types to asymmetric Hom-types within a category-model framework. It introduces polarized and neutral-polarized generalized categories-with-families (DCwFs) and a directed J-rule, enabling 1-categorical synthetic reasoning and the iteration of Hom-types. The category model demonstrates how opposite-category modalities and neutral contexts support directed hom-typings, Pi-types, and basic synthetic category constructions like composition and functors, while universes and directed univalence illuminate fundamental limits like symmetry of hom-terms. The approach lays groundwork toward directed higher observational type theory, with future work addressing natural transformations, higher inductive types, and formalization, potentially bridging directed type theory with higher categorical semantics and SOGAT frameworks.
Abstract
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-Löf Type Theory to asymmetric hom-types. We articulate the directed type theory of the category model, with appropriate modalities for keeping track of variances and a powerful directed-J rule capable of proving results about arbitrary terms of hom-types; we put this rule to use in making several constructions in synthetic 1-category theory. Because this theory is expressed entirely in terms of generalized algebraic theories, we know automatically that this directed type theory admits a syntax model and is the first step towards directed higher observational type theory.