DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2024.7

Synthetic 1-Categories in Directed Type Theory

Authors: Jacob Neumann and Thorsten Altenkirch

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

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.

Cite as

Jacob Neumann and Thorsten Altenkirch. Synthetic 1-Categories in Directed Type Theory. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@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}
}

Search Results

Documents authored by Neumann, Jacob

Synthetic 1-Categories in Directed Type Theory

Abstract

Cite as

Thanks for your feedback!

Could not send message