Synthetic 1-Categories in Directed Type Theory

TL;DR

This paper develops a directed type theory framework for reasoning about categories with asymmetric hom-types, introducing new rules and modalities to facilitate synthetic 1-category theory within type theory.

Contribution

It presents a novel directed type theory with a directed-J rule and modalities, enabling synthetic reasoning about 1-categories and laying groundwork for higher directed type theories.

Findings

Introduces a directed-J rule for hom-types

Develops modalities for variance tracking

Constructs synthetic 1-category theory within the framework

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\"of 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.