Read & Cite

A Generalized Algebraic Theory of Directed Equality

Abstract. We develop a directed type theory capable of synthetic reasoning about 1-categories, with straightforward semantics in the category of categories. All our semantic notions are defined as generalized algebraic theories, permitting modular reasoning about different type theories and ensuring the existence of initial syntax models.

We define the category model of type theory—the directed analogue of Hofmann and Steicher's groupoid model—where contexts are interpreted as categories and types as (split opfibrant) displayed categories. Adapting the groupoid model semantics of key type formers, (dependent) functions and identity types in particular, requires us to adopt a modal typing discipline to track the variances of terms. We define a succession of model notions—polarized categories with families, neutral-polarized categories with families, and directed categories with families—to abstractly capture more and more of the type theory of the category model; this includes an axiomatization of how the groupoid model's undirected type theory is situated inside the category model's directed type theory.

The symmetric (i.e. invertible) identity types of the groupoid model become directed hom-types of the category model; we can show by metatheoretic argument that our polarized typing discipline prevents invertibility of hom-types from being provable in our directed type theory. Each type therefore has the structure of a synthetic category and each function a synthetic functor; this is all proved within the theory using the eliminator for hom-types, directed path induction. We expound a new style of categorytheoretic reasoning appropriate to this setting, where the universal mapping properties of standard category theory are all phrased as principles of induction.

To support these developments, we outline generalized algebra, the mathematical discipline concerned with generalized algebraic theories. In particular, we highlight the construction of an initial algebra for every GAT (which is what guarantees a syntax model for the notions of model we use) and the fact that every GAT gives rise to a "concrete category with families", a model of type theory whose contexts are algebras and types are displayed algebras. The groupoid and category models can be viewed as a modification of the concrete CwFs of groupoids and categories, respectively, which ensures the fibrancy of their types.

June 2025 version

note

The page numbering, theorem and figure numbering, etc. is subject to change before the thesis is finalized in late 2025.

Cite the thesis

@phdthesis{neumann2025ageneralized,
  title={A Generalized Algebraic Theory of Directed Equality},
  author={Neumann, Jacob},
  year={2025},
  school={University of Nottingham}
}

Synthetic 1-Categories in Directed Type Theory

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.

Published version (TYPES 2024 post-proceedings)

Cite the paper

@InProceedings{neumann_et_al:LIPIcs.TYPES.2024.7,
  author =	{Neumann, Jacob and Altenkirch, Thorsten},
  title =	{{Synthetic 1-Categories in Directed Type Theory}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{7:1--7:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.7},
  URN =		{urn:nbn:de:0030-drops-233694},
  doi =		{10.4230/LIPIcs.TYPES.2024.7},
  annote =	{Keywords: Semantics, directed type theory, homotopy type theory, category theory, generalized algebraic theories}
}

Extended version (arXiv preprint)

Cite the preprint

@misc{neumann2024synthetic1categoriesdirectedtype,
      title={Synthetic 1-Categories in Directed Type Theory}, 
      author={Jacob Neumann and Thorsten Altenkirch},
      year={2024},
      eprint={2410.19520},
      archivePrefix={arXiv},
      primaryClass={math.CT},
      url={https://arxiv.org/abs/2410.19520}, 
}