nLab directed homotopy type theory

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).

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, published article]

• Paige Randall North, Towards a directed homotopy type theory [arXiv:1807.10566]

• Alex Kavvos, A quantum of direction (2019) [pdf]

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

• 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, 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]

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, slides]