Regarding the directed HIT example: if $\mathsf{succ}$ is to be interpreted as a(n ∞-)functor, then wouldn’t the correct definition have $\mathsf{less} : 0 \to \mathsf{succ}\ 0$ instead of $\mathrm{id}_\mathbb{N} \to \mathsf{succ}$? Otherwise it seems like you have $\mathsf{less}\ 1 \neq \mathsf{succ}(\mathsf{less}\ 0) : 1 \to 2$, so that $\mathbb{N}$ isn’t a poset.

]]>To a fair extent these points apply really to higher category theory as such

True! Especially point 1. Of course point 2 and 3 were meant to allude to the rules you may (not) need in your directed higher type theory.

A maybe more intrinsically type-theoretic motivation for directed HoTT is mentioned at the end of Cisinski et al.’s abstract (here): Formalization of categorical semantics of plain HoTT.

I added this point to the list of *pros*.

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 HoTT: It might still be better to instead work internal to plain HoTT, I think this isn’t clear yet.

I added this point to the list of *cons*.

The attempts pre 2009 to get this up and running by direct definition of higher $n$-categories led little beyond nowhere. The breakthrough came from understanding that higher category theory works well inside or on a backdrop of homotopy theory/($\infty$,1) -category theory.

Definitely agree with that example. While the $\infty$-PoV shifted paradigms in the field, one could argue that for some purposes it also came with drawbacks since spaces are (in some ways) incomputably hard. Incidentally, I always hoped manifold diagrams, as a resolution to the “directed tangle hypothesis”, would find a middle ground. (A highly hypothetical statement as you know.)

]]>These are interesting points. I’ll offer some critique:

To a fair extent these points apply really to higher category theory as such, not specifically to its (potential) formalization by type theories (though the lens of type theory puts some higher category theory concepts, such as universes, more into focus).

A maybe more intrinsically type-theoretic motivation for directed HoTT is mentioned at the end of Cisinski et al.’s abstract (here): Formalization of categorical semantics of plain HoTT.

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*HoTT: It might still be better to instead work internal to plain HoTT, I think this isn’t clear yet.Compare the history of non-type theoretic higher category theory: The attempts pre $\sim$2009 to get this up and running by direct definition of higher $n$-categories led little beyond nowhere. The breakthrough came from understanding that higher category theory works well inside or on a backdrop of homotopy theory/$(\infty,1)$-category theory.

Of course, when people tried to carry this lesson to HoTT they ran into the technical problem of defining (semi-)simplicial types inside plain HoTT and got stuck with this on technical grounds. But maybe this just serves to remind us that simplicial objects are convenient a model but hardly an intrinsic definition of higher structures, and maybe the good definition of $\infty$-category internal to plain HoTT is still to be discovered.

- recording some thoughts on directed higher type theories from a conversation with Mike I had a while ago.
- happy to discuss further
- feel free to dramatically rewrite

added pointer to

- Hoang Kim Nguyen,
*Directed univalence in simplicial sets*, talk in*Homotopy Type Theory Electronic Seminar Talks*(March 2023) [video, slides]

and cross-link with *directed univalence axiom*

Remove dangling link to generalizations of the Grothendieck construction.

]]>Add year to “Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance”

]]>Remove citation of controversial note; remove section header as only two citations remain.

]]>Link to the generalizations section of the Grothendieck construction.

]]>Naturality TT citations.

]]>Directed Algebraic Topology promises us “Models of non-reversible worlds”, and how we’ll be able to consider “concurrent processes, rewrite systems, traffic networks, space-time models, biological systems, etc.”

All that advertisement is predicated on assuming that these things form given categories or higher categories. Directed homotopy theory itself is just another word for $(\infty,n)$-category theory, in extension of how “homotopy theory” is another word for $(\infty,0)$-category theory ($\pm 1$, depending on how you want to count).

If we want to retain the topological aspect in this, then we are talking about some kind of stratified spaces presenting $(\infty,n)$-categories.

]]>…but no actual formal syntax yet

Right, that’s the part which I know is important but gain very little insight from.

Perhaps the part of my question I’m most interested in is whether there’s an analogue for

ordinary HoTT is a general-purpose programming language

Directed Algebraic Topology promises us “Models of non-reversible worlds”, and how we’ll be able to consider “concurrent processes, rewrite systems, traffic networks, space-time models, biological systems, etc.”

]]>This partly answers the first question in #24:

They don’t have an actual type theory yet.

It’s the same situation as with my suggestion of linear homotopy type theory in the past: A semantics neatly organized by simple rules which seem to lend themselves to type-theoretic formalization, but no actual formal syntax yet.

]]>expanded this out to the following dialogue, highlighting that 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.

]]>

added this quote:

]]>[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.

added this remark:

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

]]>

The answer to your last question is: “…for constructions in parameterized directed homotopy theory”, namely in cocartesian slices of the $(\infty,2)$-category of $(\infty ,1)$-categories (they make this fully explicit on the top of slide 11 in the 2nd notes pdf) and presumeably (I guess) more generally of $(\infty,2)$-sheaves of such $(\infty,1)$-categories.

]]>I’d be interested in people’s views on this work (#23). Others have been working on directed HoTT. Is there a breakthrough here?

And more broadly what would it mean to have a good directed HoTT?

E.g., if ordinary HoTT is

a general-purpose programming language as well as a proof language for constructions in parameterized homotopy theory (Topological Quantum Gates in HoTT)

what could be said for *directed* HoTT?

added pointers to the available resources for Cisinski et al.’s presentations (here):

[web, video 1:YT, 2:YT, 3:YT; slides 0:pdf, 1:pdf, 2:pdf, 3:pdf]

]]>added pointer to:

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

I am not aware of publically available information beyond that abstract. But the abstract does make it sound like they claim the internal language of $(\infty,2)$-toposes.

]]>Re #17, so the novel aspect, over other attempts listed in the references, is that the type theory is univalent?

]]>I have expanded the idea-section (here), to explain/recall how to count the directionality degree.

]]>Mathieu Anel was so kind to send the direct anchored link: …/hott/seminars/index.html#230313.

(I checked and this is the general pattern for the HoTT-CMU seminar page: The anchor for a specific event is the date in the format `#yymmdd`

.)