Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Directed type theory, with a twist

Fernando Rafael Chu Rivera, Paige Randall North

TL;DR

This paper presents a new type theory, Twisted Type Theory (TTT), which features a novel ``twisting''operation on types: given a type that depends both contravariantly and covariantly on some variables, its twist is a new type that depends only covariantly on the same variables.

Abstract

In recent years, Homotopy Type Theory (HoTT) has had great success both as a foundation of mathematics and as internal language to reason about $\infty$-groupoids (a.k.a. spaces). However, in many areas of mathematics and computer science, it is often the case that it is categories, not groupoids, which are the more important structures to consider. For this reason, multiple directed type theories have been proposed, i.e., theories whose semantics are based on categories. In this paper, we present a new such type theory, Twisted Type Theory (TTT). It features a novel ``twisting'' operation on types: given a type that depends both contravariantly and covariantly on some variables, its twist is a new type that depends only covariantly on the same variables. To provide the semantics of this operation, we introduce the notion of dependent 2-sided fibrations (D2SFibs), which generalize Street's notion of 2-sided fibrations. We develop the basic theory of D2SFibs, as well as characterize them through a straightening-unstraightening theorem. With these results in hand, we introduce a new elimination rule for Hom-types. We argue that our syntax and semantics satisfy key features that allow reasoning in a HoTT-like style, which allows us to mimic the proof techniques of that setting. We end the paper by exemplifying this, and use TTT to reason about categories, giving a syntactic proof of Yoneda's lemma.

Directed type theory, with a twist

TL;DR

This paper presents a new type theory, Twisted Type Theory (TTT), which features a novel ``twisting''operation on types: given a type that depends both contravariantly and covariantly on some variables, its twist is a new type that depends only covariantly on the same variables.

Abstract

In recent years, Homotopy Type Theory (HoTT) has had great success both as a foundation of mathematics and as internal language to reason about -groupoids (a.k.a. spaces). However, in many areas of mathematics and computer science, it is often the case that it is categories, not groupoids, which are the more important structures to consider. For this reason, multiple directed type theories have been proposed, i.e., theories whose semantics are based on categories. In this paper, we present a new such type theory, Twisted Type Theory (TTT). It features a novel ``twisting'' operation on types: given a type that depends both contravariantly and covariantly on some variables, its twist is a new type that depends only covariantly on the same variables. To provide the semantics of this operation, we introduce the notion of dependent 2-sided fibrations (D2SFibs), which generalize Street's notion of 2-sided fibrations. We develop the basic theory of D2SFibs, as well as characterize them through a straightening-unstraightening theorem. With these results in hand, we introduce a new elimination rule for Hom-types. We argue that our syntax and semantics satisfy key features that allow reasoning in a HoTT-like style, which allows us to mimic the proof techniques of that setting. We end the paper by exemplifying this, and use TTT to reason about categories, giving a syntactic proof of Yoneda's lemma.
Paper Structure (21 sections, 32 theorems, 13 equations, 5 figures, 1 table)

This paper contains 21 sections, 32 theorems, 13 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Categorical models of MLTT
  3. The category model of MLTT
  4. The displayed category model of MLTT
  5. Twisted types and dependent 2-sided fibrations
  6. Twisted Type Theory
  7. Hom-types revisited
  8. Other operations in TTT
  9. Applications
  10. Directed univalence
  11. Natural transformations
  12. Yoneda lemma
  13. Conclusion and future work
  14. Complete description of TTT
  15. Straightening and unstraightening for D2SFibs
  16. ...and 6 more sections

Key Result

Proposition 5

The category model has strong $\Sigma$-types and, if a countable hierarchy of inaccessible cardinals is assumed, universes ${\mathcal{U}}_i$. Further, it also validates the following rules about opposite types and ${\mathsf{Hom}}$-types.

Figures (5)

  • Figure 1: Rules about displayed types and twists.
  • Figure 2: Rules about opposite types and contexts.
  • Figure 3: Rules about $\Sigma$-types.
  • Figure 4: Rules about $\Pi$-types.
  • Figure 5: Rules about ${\mathsf{Hom}}$-types.

Theorems & Definitions (53)

  • Definition 1: Comprehension categories jacobsComprehensionCategoriesSemantics1993
  • Definition 3: The category model
  • Proposition 5: licata_2-dimensional_2011north_towards_2019
  • Remark 6
  • Proposition 8: Straightening-unstraightening for opfibrations
  • Proposition 9: Straightening-unstraightening for displayed categories
  • Remark 10
  • Definition 11: Displayed category model
  • Remark 12
  • Proposition 13
  • ...and 43 more