Showing changes from revision #30 to #31: Added | Removed | Changed

Contents

Idea

What homotopy type theory is for homotopy theory/(∞,1)-category theory, directed homotopy type theory is (or should be) for directed homotopy theory/(∞,n)-category theory.

More in detail: Where

• the types of homotopy type theory have interpretation as ∞-groupoids aka (∞,0)-categories (and more generally: as ∞-stacks), so that homotopy type theory itself is an internal language for the (∞,1)-categories (specifically, for univalent HoTT: (∞,1)-toposes) that these (∞,0)-categories form

so

• the types of directed homotopy type theory ought to have interpretation as (∞,n)-categories for some $n \in \{1, 2, \cdots, \infty\}$ (and more generally: as (∞,n+1)-sheaves) so that directed homotopy type theory itself should be an internal language for the (∞,n+1)-categories (and in the suitably directed univalent case: (∞,n+1)-toposes) that these (geometric) (∞,n)-categories form.

A proposal for the case $n = \infty$ (potentially describing (∞,∞)-categories aka omega-categories) is opetopic type theory, going back to Finster (2012).

A proposal for the case $n = 1$ with the directed analog of the univalence axiom included — hence for a type theory whose types may be interpreted as (∞,1)-categories/(∞,2)-sheaves and which itself would be the internal language of the $(\infty,2)$-categories/$(\infty,2)$-toposes that these form — is announced in Cisinski et al. (2023).

Appeal and practicality

One obvious reason for studying directed homotopy type theory (especially when $n = \infty$ in the above) is generality: $(\infty,\infty)$-categories are among the most general higher categorical structures. Besides this reason, access to higher directed structure may offer, in particular, the following conceptual advantages.

• Universe types can retain their higher directed structure. Universe types are (small) ‘internal’ reflections of the category of all types of our type theory, but without sufficient higher structure in the theory, this reflection process must forget structure present in the external category (for instance, the category of sets can only contain a ‘set of sets’ as an object which does not remember functions; similarly, the universe type in homotopy type theory must forget about maps between types that are not equivalences).

• Dependent function types become ‘just’ function types. In the presence of higher directed structure, equipped with a universe type $\mathcal{U}$ and unit type $\mathbf{1}$, dependent function types $\Pi_{x : A} F(x)$, for $F$ a type family $F : A \to \mathcal{U}$, can be understood in terms of ‘just’ function types, namely, as $\mathsf{Fun}_{\mathsf{Fun}(A,\mathcal{U})}(\mathrm{const}_{\mathbf{1}}, F)$ (where $\mathrm{const}_{\mathbf{1}} : A \to \mathcal{U}$ is the constant functor with image $\mathbf{1}$).

• Inductive types become substantially more expressive. Inductive types with dependent constructors can also be expressed in terms of non-dependent constructors: for instance, for $F$ a type family $F : A \to \mathcal{U}$, the dependent pair type $\Sigma_{x : A} F(x)$ can be introduced with a single constructor $\mathrm{in} : F \to \mathrm{const}_{\Sigma_{x : A} F(x)}$ (which is a map in the function type $\mathsf{Fun}(A, \mathcal{U})$ and should thus be thought of as a natural transformation between functors). Moreover, there is the topic of higher inductive types; a useful example of a ‘true’ directed higher inductive type is the poset type $(\mathbb{N},\leq)$ with constructors

  $$0 : \mathbf{1} \to \mathbb{N}$$
  $$\mathsf{succ} : \mathbb{N} \to \mathbb{N}$$
  $$\mathsf{less} : \id_{\mathbb{N}} \to \mathsf{succ}$$

• Formalization of (higher) categorical semantics. On a more practical side, access to higher directed structure could allow us to formalize the categorical semantics of other types theories, such as homotopy type theory, as discussed in Cisinki et al 2023.

On the other hand, working directed higher type theory may not be very practical.

• While it is clear that one eventually wants to speak about higher categorical concepts with type theory, it is not a priori clear that this motivates the dedicated formulation of new rules for directed higher type theory: it might still be more convenient to instead work internal to ordinary homotopy type theory.

• More generally, it has been argued that directed higher type theories may not aid the practical usability of proof assistants due to the potential complexity of the rules involved.

Related concepts

• directed univalence axiom

• directed type theory, 2-type theory

• opetopic type theory

• semi-simplicial type

• geometric homotopy type theory

• modal homotopy type theory

• fibered category theory

References

General

• Robert Harper, Dan Licata, Canonicity for 2-Dimensional Type Theory (pdf)

• Robert Harper, Dan Licata, 2-Dimensional directed dependent type theory (pdf slides)

• Michael Warren, Directed Type Theory (video lecture)

• Dan Licata, Chapters 7 and 8 of Dependently Typed Programming with Domain-Specific Logics PhD thesis, (pdf)

• Emily Riehl, Mike Shulman, A type theory for synthetic ∞-categories, Higher Structures 1 1 (2017) [[arxiv:1705.07442](https://arxiv.org/abs/1705.07442), published article]

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)

• Paige Randall North, Towards a directed homotopy type theory [[arXiv:1807.10566](https://arxiv.org/abs/1807.10566)]

• Alex Kavvos, A quantum of direction (2019) [[pdf](https://seis.bristol.ac.uk/~tz20861/papers/meio.pdf)]

• Andreas Nuyts, Higher Pro-arrows: Towards a Model for Naturality Pretype Theory, HoTTEST seminar, May 2, 2024, Slides, Video

• Andreas Nuyts, Higher Pro-arrows: Towards a Model for Naturality Pretype Theory, HoTT/UF 2023, PDF, Slides, Video

• Andreas Nuyts, Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance, 2015, PDF

Cisinski et al.

• Denis-Charles Cisinski, Hoang Kim Nguyen, Tashi Walde: Univalent Directed Type Theory, lecture series in the CMU Homotopy Type Theory Seminar (13, 20, 27 Mar 2023) [[web](https://www.cmu.edu/dietrich/philosophy/hott/seminars/index.html#230313), video 1:YT, 2:YT, 3:YT; slides 0:pdf, 1:pdf, 2:pdf, 3:pdf]

  Abstract: We will introduce a version of dependent type theory that is suitable to develop a synthetic theory of 1-categories. The axioms are both a fragment and an extension of ordinary dependent type theory. The axioms are chosen so that (∞,1)-category theory (in the form of quasi-categories or complete Segal spaces) gives a semantic interpretation, in a way which extends Voevodsky’s interpretation of univalent dependent type theory in the homotopy theory of Kan complexes. More generally, using a slight generalization of Shulman’s methods, we should be able to see that the theory of (∞,1)‑categories internally in any ∞‑topos (as developed by Martini and Wolf) is a semantic interpretation as well (hence so is parametrized higher category theory introduced by Barwick, Dotto, Glasman, Nardin and Shah). There are of course strong links with ∞-cosmoi of Riehl and Verity as well as with cubical HoTT (as strongly suggested by the work of Licata and Weaver), or simplicial HoTT (as in the work of Buchholtz and Weinberger). We will explain the axioms in detail and have a glimpse at basic theorems and constructions in this context (Yoneda Lemma, Kan extensions, Localizations). We will also discuss the perspective of reflexivity: since the theory speaks of itself (through directed univalence), we can use it to justify new deduction rules that express the idea of working up to equivalence natively (e.g. we can produce a logic by rectifying the idea of having a locally cartesian type). In particular, this logic can be used to produce and study semantic interpretations of HoTT.

This is based on the discussion of straightening and unstraightening entirely within the context of quasi-categories from

• Denis-Charles Cisinski, Hoang Kim Nguyen, The universal coCartesian fibration [[arXiv:2210.08945](https://arxiv.org/abs/2210.08945)]

which (along the lines of the discussion of the universal left fibration from Cisinski 2019) allows to understand the universal coCartesian fibration as categorical semantics for the univalent type universe in directed homotopy type theory (see video 3 at 1:16:58 and slide 3.33).

But the actual type-theoretic syntax (inference rules) for this intended semantics remains to be given:

[Cisinski in video 3 at 1:27:43]: I won’t provide the full syntax yet and actually I would be very happy to discuss that, because we don’t know yet and I have questions myself, actually.

[Awodey in video 3 at 1:46:23]: Maybe I’ll suggest something, you tell me if you agree: What we have is a kind of axiomatization of the semantics of a system for type theory, so that we know what exactly we want formalize in the type theory, and what depends on what, and it articulates and structures the intended interpretation of the type theory in a very useful way. Maybe in the way that the axiomatic description of a cartesian closed category was very good to have for formulating the lambda-calculus. But I think that what we have is more on the side of the axiomatic description of the semantics, like the cartesian closed category, that it is on the side of the lambda-calculus itself. So, maybe I would suggest the term “abstract type theory” to describe this system as an intermediate in between an actual formally implemented system of type theory and the big unclear world of possible semantics and all the different structures that one could try to capture with a type theory, in between is this abstract type theory which specifies a particular structure that we want to capture in our type theory, which is a very very useful methodological step. [] I am trying to maybe reconcile:

Some people would prefer to call a type theory only something which can immediately be implemented in a computer. So that’s different than an abstract description of a structure that we would want to describe in such a type theory.

[Cisinski in video 3 at 1:49:28]: I agree with what you say but I still have the hope to be able to produce an actual syntax [] that’s really the goal.

More on the directed univalence axiom in this context:

• Hoang Kim Nguyen, Directed univalence in simplicial sets, talk in Homotopy Type Theory Electronic Seminar Talks (March 2023) [[video](https://www.youtube.com/watch?v=GgcJqzGvq80), slides]