Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created directed homotopy type theory
Hm, maybe the references given there so far factor through 2-type theory. Anyway, eventually somebody should say something that fits into this entry! :-)
Next semester our “group seminar”, starting in a few weeks, has the topic “-categories”. I guess I’ll be sort of running the seminar. Last semester we ended the analogous seminar on -toposes with me giving the survey talk, the notes for which now constitute the Lab entry (infinity,n)-category. Now we plan to dig deeper into the details. So I need to acquaint myself with plenty of those details, to the extent that I haven’t yet (which is just a small extent).
As usual, I have a “personal hook” into the topic: there is a certain question that I would like to eventually understand the answer to, and I’ll probably be looking at the entire seminar through this lens. I had recently posted here a link to a little text that describes this idea, at next (schreiber). In brief, the issue is this:
Complete the step indicated in the very last paragraph of Quantum gauge field theory in Cohesive homotopy type theory (schreiber) .
That is: inside cohesive homotopy type theory postulate a map together with a suitable representation of . At least when interpreted in a model such as Smooth∞Grpd, associated to this data should be an extended topological quantum field theory which to the point assigns the “space of sections” of the -bundle -associated to the -principal bundle modulated by , and this should be internal.
The task is: describe / construct this eTQFT in the internal logic, as far as possible.
The result should involve -directed homotopy type theory in one flavor or other. Moreover, it needs to be with all duals.
I really like the approach to this rough kind of problem that Mike was recently suggesting on the blog here. Maybe that’s the lens through which I want to be looking at the whole question.
Mike, did you make further progress with the ideas sketched there, meanwhile? I’d love to know about whatever you have, to the degree that you can share it.
Another thought that crossed my mind was: for the purpose of -cats with all duals, it might be best to go via blob n-categories. Does anyone what the latest status is of relating that theory to models of -categories is?
No, I haven’t gotten any further with that idea.
I added the reference.
Can’t see where they’re from.
Can’t see where they’re from.
What?
@David C
You wean where Paige is from?
@David R, yes. I couldn’t find anything to form a page on Paige, but then I am limited to Baidu as a search engine since in China.
@David C
note that her surname used to be just ’North’. Here is her current home page: https://paigenorth.github.io/
Oh, was “they” in #5 supposed to be a singular genderless pronoun? (-:O
Coincidentally, Paige is here with me in San Diego this week, with Benedikt Ahrens and Dimitris Tsementzis, working on a different project.
Seems like a good solution to me. Do you always write “he or she”?
I do sometimes use “they” as a singular genderless pronoun, but it usually sounds slightly awkward to me because its primary meaning in my idiolect is still a plural. It also didn’t occur to me that Paige’s gender might not be obvious from her name, so I didn’t think of the possibility that “they” in #5 might be referring to her, and was therefore unable to make sense of the sentence. In this situation, if I were unsure of her gender, I would probably just have re-used her name: “Can’t see where Paige is from”.
It’s not a name I’ve ever encountered. I dare say with Google I could have worked out the gender, but try Baidu. Had I known Wikipedia is available here, it wouldn’t have helped so much:
Paige is a given name for males and females. It is of Latin origin (Byzantine “Págius” young boy helper/mate of young nobles, from “padius” young boy, derived from Greek “Paidion” child) and its meaning is “young helper” or “young child”. A page in medieval households was usually a young boy whose service was the first step in his training as a knight. Use may possibly indicate an ancestor who was a page.
In modern times Paige has become a given name, generally given to girls living in North America since the middle of the 20th century, but also occasionally to boys.
I’m not saying her gender should have been clear from her name, just that at the time, it failed to occur to me that it wouldn’t be. (-:
I’ve been wondering how well the type theoretic usage of contexts captures our interpretative practices. We each have our own context, and then when we speak with someone else, we can theorise as to theirs. This includes what we take to be common knowledge, but we will also envisage that they will have parts different from ours, through ignorance, mistakes, greater knowledge, different experience, etc. Adjustments to our own context and to our model of the other’s context must continually be made as we converse.
On reading ’Paige’, I adjust my context to add, ’Paige: Name of person’. You already have ’Paige: Name of female person’, and a supply of people so named, and take it to be within common knowledge.
It seems we do a lot of work in reconstructing sensibly the contexts in which statements make sense. We often use the language of inference, but it’s better to distinguish presupposition from inference. We hear something, postulate a reasonable context in which it makes sense, then infer some component of that postulated context, and take it to be inference from the original statement. On hearing that X has stopped smoking without knowing anything of his habits, I see that it is presupposed that X once was in the habit of smoking. It’s better to distinguish this inference to presupposition from a proper inference, such as to the claim that X now has a lower chance of a heart attack.
added the following pointer to this upcoming talk series:
(Unfortunately there seems to be no way to directly/anchoredly link to the announcement item – does anyone know who at HoTT-CMU has control over their seminar webpage? I have had this problem before and will have it again.)
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)
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 (under 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.
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.)
Re #17, so the novel aspect, over other attempts listed in the references, is that the type theory is univalent?
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 -toposes.
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?
The answer to your last question is: “…for constructions in parameterized directed homotopy theory”, namely in cocartesian slices of the -category of -categories (they make this fully explicit on the top of slide 11 in the 2nd notes pdf) and presumeably (I guess) more generally of -sheaves of such -categories.
added this remark:
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).
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.
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.
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.
…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.”
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 -category theory, in extension of how “homotopy theory” is another word for -category theory (, 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 -categories.
added pointer to
and cross-link with directed univalence axiom
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 2009 to get this up and running by direct definition of higher -categories led little beyond nowhere. The breakthrough came from understanding that higher category theory works well inside or on a backdrop of homotopy theory/-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 -category internal to plain HoTT is still to be discovered.
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 -categories led little beyond nowhere. The breakthrough came from understanding that higher category theory works well inside or on a backdrop of homotopy theory/(,1) -category theory.
Definitely agree with that example. While the -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.)
Regarding the directed HIT example: if is to be interpreted as a(n ∞-)functor, then wouldn’t the correct definition have instead of ? Otherwise it seems like you have , so that isn’t a poset.
Added reference
Anonymouse
1 to 43 of 43