2026-08-08T00:33:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23369 2025-07-03T08:54:54Z ddc:004 open_access

Synthetic 1-Categories in Directed Type Theory Neumann, Jacob Altenkirch, Thorsten Semantics directed type theory homotopy type theory category theory generalized algebraic theories 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jacob Neumann and Thorsten Altenkirch 2025 Is Part Of LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2024.7 urn:nbn:de:0030-drops-233694 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.7 eng https://creativecommons.org/licenses/by/4.0/legalcode