nLab directed homotopy type theory

Contents

Context

Directed Type Theory

Higher category theory

higher category theory

Basic concepts

Basic theorems

Applications

Models

Morphisms

Functors

Universal constructions

Extra properties and structure

1-categorical presentations

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

so

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

Appeal and practicality

One obvious reason for studying directed homotopy type theory (especially when n=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 1\mathbf{1}, dependent function types Π x:AF(x)\Pi_{x : A} F(x), for FF a type family F:A𝒰F : A \to \mathcal{U}, can be understood in terms of ‘just’ function types, namely, as Fun Fun(A,𝒰)(const 1,F)\mathsf{Fun}_{\mathsf{Fun}(A,\mathcal{U})}(\mathrm{const}_{\mathbf{1}}, F) (where const 1:A𝒰\mathrm{const}_{\mathbf{1}} : A \to \mathcal{U} is the constant functor with image 1\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 FF a type family F:A𝒰F : A \to \mathcal{U}, the dependent pair type Σ x:AF(x)\Sigma_{x : A} F(x) can be introduced with a single constructor in:Fconst Σ x:AF(x)\mathrm{in} : F \to \mathrm{const}_{\Sigma_{x : A} F(x)} (which is a map in the function type Fun(A,𝒰)\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:1 0 : \mathbf{1} \to \mathbb{N}
    succ: \mathsf{succ} : \mathbb{N} \to \mathbb{N}
    less:id succ \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.

References

General

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 August 22, 2024 at 15:28:36. See the history of this page for a list of all contributions to it.