nLab directed homotopy type theory



Directed Type Theory

Higher category theory

higher category theory

Basic concepts

Basic theorems





Universal constructions

Extra properties and structure

1-categorical presentations



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


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

A proposal for the case n=1n = 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 ( , 2 ) (\infty,2) -categories/ ( , 2 ) (\infty,2) -toposes that these form — is announced in Cisinski et al. (2023).



Cisinski et al.

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

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:

Last revised on May 21, 2023 at 14:02:09. See the history of this page for a list of all contributions to it.