Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Directed univalence in simplicial homotopy type theory

Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz

TL;DR

This work develops TT\boxslash, a modal extension of simplicial type theory with a weakened interval, to realize a directed univalent universe ${\mathcal S}$ of groupoids and covariant fibrations. It proves that ${\mathcal S}$ is directed univalent, Segal, and Rezk, and provides an internal API for a wide range of categorical constructions, including subcategories and higher algebraic structures. The construction relies on amazing covariance, a cubical-spaces model, and a straightening--unstraightening correspondence to encode covariant families. The results establish a foundational framework for directed higher category theory and synthetic higher algebra within type theory, with potential for formalization and computational interpretation in future work.

Abstract

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 $\mathcal{S}$. We prove that homomorphisms in this type correspond to ordinary functions of types i.e., that $\mathcal{S}$ is directed univalent. The construction of $\mathcal{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 $\mathcal{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.

Directed univalence in simplicial homotopy type theory

TL;DR

This work develops TT\boxslash, a modal extension of simplicial type theory with a weakened interval, to realize a directed univalent universe of groupoids and covariant fibrations. It proves that is directed univalent, Segal, and Rezk, and provides an internal API for a wide range of categorical constructions, including subcategories and higher algebraic structures. The construction relies on amazing covariance, a cubical-spaces model, and a straightening--unstraightening correspondence to encode covariant families. The results establish a foundational framework for directed higher category theory and synthetic higher algebra within type theory, with potential for formalization and computational interpretation in future work.

Abstract

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 . We prove that homomorphisms in this type correspond to ordinary functions of types i.e., that is directed univalent. The construction of 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 , 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.
Paper Structure (40 sections, 68 theorems, 48 equations, 1 figure)

This paper contains 40 sections, 68 theorems, 48 equations, 1 figure.

Table of Contents

  1. Introduction
  2. A type theory for categories
  3. Simplicial type theory, a reprise
  4. Directed univalence
  5. Constructing S
  6. Extending simplicial type theory to triangulated type theory
  7. Contributions
  8. A primer on simplicial and modal type theory
  9. Simplicial type theory and basic category theory
  10. Multimodal type theory
  11. Triangulated type theory
  12. The definition of triangulated type theory
  13. The mode theory
  14. The interval
  15. The simplicial monad
  16. ...and 25 more sections

Key Result

lemma 1.2

If $F,G : \mathsf{Monoid} \to {\mathcal{S}}$ and $\alpha : \DelimPrn{A : \mathsf{Monoid}} \to F\DelimPrn{A} \to G\DelimPrn{A}$ then $\alpha$ is natural i.e. if $f : A \to B$ is a monoid homomorphism, then $\alpha\DelimPrn{B} \circ F\DelimPrn{f} = G\DelimPrn{f} \circ \alpha\DelimPrn{A}$.

Figures (1)

  • Figure 1: Illustrations of simplices

Theorems & Definitions (138)

  • definition 1.2
  • lemma 1.2
  • lemma 1.2
  • definition 2.1
  • definition 2.2
  • definition 2.4
  • definition 2.5
  • definition 2.7
  • definition 2.8
  • remark 2.9
  • ...and 128 more