Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 24th 2011
    • (edited Nov 24th 2011)
    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 24th 2011

    Hm, maybe the references given there so far factor through 2-type theory. Anyway, eventually somebody should say something that fits into this entry! :-)

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeAug 21st 2012
    • (edited Aug 21st 2012)

    Next semester our “group seminar”, starting in a few weeks, has the topic “(,n)(\infty,n)-categories”. I guess I’ll be sort of running the seminar. Last semester we ended the analogous seminar on (,1)(\infty,1)-toposes with me giving the survey talk, the notes for which now constitute the nnLab 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 c conn:BG connB nA conn\mathbf{c}_{conn} : \mathbf{B}G_{conn} \to \mathbf{B}^n A_{conn} together with a suitable representation ρ\rho of B n1A\mathbf{B}^{n-1}A. 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 \infty-bundle ρ\rho-associated to the B n1A\mathbf{B}^{n-1}A-principal bundle modulated by c conn\mathbf{c}_{conn}, and this should be internal.

    The task is: describe / construct this eTQFT in the internal logic, as far as possible.

    The result should involve nn-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 (,n)(\infty,n)-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 (,n)(\infty,n)-categories is?

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeAug 21st 2012

    No, I haven’t gotten any further with that idea.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 14th 2018

    I added the reference.

    Can’t see where they’re from.

    diff, v8, current

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeAug 14th 2018

    Can’t see where they’re from.

    What?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeAug 14th 2018

    Added reference to Riehl-Shulman.

    diff, v9, current

    • CommentRowNumber8.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 14th 2018

    @David C

    You wean where Paige is from?

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 14th 2018

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

    • CommentRowNumber10.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 15th 2018

    @David C

    note that her surname used to be just ’North’. Here is her current home page: https://paigenorth.github.io/

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeAug 15th 2018

    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.

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 15th 2018

    Seems like a good solution to me. Do you always write “he or she”?

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeAug 15th 2018

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

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 15th 2018

    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.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeAug 15th 2018

    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. (-:

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 16th 2018

    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.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMar 5th 2023

    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.


    diff, v12, current

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeMar 6th 2023
    • (edited Mar 6th 2023)

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

    diff, v13, current

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeMar 6th 2023

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

    diff, v13, current

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 6th 2023

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

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeMar 6th 2023

    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 (,2)(\infty,2)-toposes.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeMar 6th 2023

    added pointer to:

    diff, v14, current

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeMar 28th 2023
    • (edited Mar 29th 2023)

    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]

    diff, v17, current

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 28th 2023

    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?

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeMar 28th 2023
    • (edited Mar 28th 2023)

    The answer to your last question is: “…for constructions in parameterized directed homotopy theory”, namely in cocartesian slices of the (,2)(\infty,2)-category of (,1)(\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 (,2)(\infty,2)-sheaves of such (,1)(\infty,1)-categories.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeMar 29th 2023
    • (edited Mar 29th 2023)

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


    diff, v19, current

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeMar 29th 2023

    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.

    diff, v19, current

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeMar 29th 2023
    • (edited Mar 29th 2023)

    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.


    diff, v19, current

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeMar 29th 2023
    • (edited Mar 29th 2023)

    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.

    • CommentRowNumber30.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 30th 2023

    …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.”

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeMar 30th 2023

    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 (,n)(\infty,n)-category theory, in extension of how “homotopy theory” is another word for (,0)(\infty,0)-category theory (±1\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 (,n)(\infty,n)-categories.

    • CommentRowNumber32.
    • CommentAuthoranuyts
    • CommentTimeApr 18th 2023

    Naturality TT citations.

    diff, v21, current

    • CommentRowNumber33.
    • CommentAuthoranuyts
    • CommentTimeApr 18th 2023

    Link to the generalizations section of the Grothendieck construction.

    diff, v21, current

    • CommentRowNumber34.
    • CommentAuthoranuyts
    • CommentTimeApr 18th 2023

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

    diff, v23, current

    • CommentRowNumber35.
    • CommentAuthoranuyts
    • CommentTimeApr 18th 2023

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

    diff, v23, current

    • CommentRowNumber36.
    • CommentAuthoranuyts
    • CommentTimeApr 18th 2023

    Remove dangling link to generalizations of the Grothendieck construction.

    diff, v23, current

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2023

    added pointer to

    and cross-link with directed univalence axiom

    diff, v25, current

    • CommentRowNumber38.
    • CommentAuthorChristoph Dorn
    • CommentTimeJun 1st 2023
    • 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

    diff, v27, current

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeJun 2nd 2023

    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 \sim2009 to get this up and running by direct definition of higher nn-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)(\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.

    • CommentRowNumber40.
    • CommentAuthorChristoph Dorn
    • CommentTimeJun 3rd 2023
    • (edited Jun 3rd 2023)

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

    • CommentRowNumber41.
    • CommentAuthorncfavier
    • CommentTimeMar 5th 2024

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

    • CommentRowNumber42.
    • CommentAuthoranuyts
    • CommentTimeAug 22nd 2024

    Citations to Naturality Pretype Theory

    diff, v30, current

  1. Added reference

    Anonymouse

    diff, v31, current