2024/07/12 by Daniel Gratzer, Gratzer, Daniel, Jonathan Weinberger +3 · 3 citations
Mathematics · #03B38 #18B50 #18D30 #18N45 #18N50 #18N60 #55U35 #Advanced Topics in Algebra #Algebraic Topology (math.AT) #Algebraic structures and combinatorial models #Category Theory (math.CT) #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2407.09146
openalex publication_date 2024/07/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics -- where it allows for synthetic (higher) category theory -- and programming languages -- where it leads to a directed version of the structure identity principle. In this work, we construct the first types in simplicial type theory with non-trivial homomorphisms. We extend simplicial type theory with modalities and new reasoning principles to obtain triangulated type theory in order to construct the universe of discrete types S. We prove that homomorphisms in this type correspond to ordinary functions of types i.e., that S is directed univalent. The construction of S is foundational for both of the aforementioned applications of simplicial type theory. We are able to define several crucial examples of categories and to recover important results from category theory. Using S, we are also able to define various types whose usage is guaranteed to be functorial. These provide the first complete examples of the proposed directed structure identity principle.