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 comma 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 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.
    • CommentAuthorMike Shulman
    • CommentTimeMar 29th 2015

    The folks working on cubical type theory have been telling me about the virtues of a version of cubical sets that have diagonals (but not necessarily connections). That is, we define \Box to be the free cartesian monoidal category generated by an object II and two points 0,1:*I0,1:\ast\to I (i.e. the Lawvere theory of bipointed sets), and consider presheaves on this. Besides appearing well-adapted for designing a type theory, this has other virtues lacked by other kinds of cubical sets, such as a cartesian monoidal structure that is preserved by geometric realization (i.e. it is a strict test category) — the canonical functor Top\Box\to Top preserves finite products (being determined by the universal property of \Box) and hence so does left Kan extension along it. And apparently this presheaf topos classifies the geometric theory of objects equipped with two distinct points, so in this sense they are an obvious “unordered” analogue of simplicial sets (which classify the theory of linear orders equipped with distinct top and bottom points).

    It seems as though this very nice sort of cubical set has been almost completely missed by homotopy theorists? Has anyone studied it before? Is there something wrong with it that excluded it from consideration?

    • CommentRowNumber2.
    • CommentAuthorTim_Porter
    • CommentTimeMar 29th 2015
    • (edited Mar 29th 2015)

    Mike: This has been studied, but for details I suggest that you e-mail Ronnie. (Edit: I have sent him a message with a link to this.)

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 29th 2015

    I would suggest to ask Cisinski and Maltsiniotis, if you haven’t already.

    • CommentRowNumber4.
    • CommentAuthorronniegpd
    • CommentTimeMar 29th 2015
    There were some old notes

    \'Evrard, M.
    Homotopie des complexes simpliciaux et cubiques.
    Preprint. 1976?

    of which I mislaid my copy before I could scan it!

    He considered the category with objects {0,1}^n considered as a partially ordered set and the morphisms those of partially ordered sets.

    Of course you know the paper

    Grandis, M. and Mauri, L.
    {Cubical sets and their site}.
    {Theory Applic. Categories} \textbf{11} (2003) 185--201.

    and Marco has written a lot more recently.

    I am not sure how the diagonals fit into the Brown-Higgins material. The advantages of the cubes come out well in Chapter 15 of "Nonabelian Algebraic Topology", but we took the minimum needed for our work.

    The simplex model is, it seems to me, a non starter for
    algebraic inverses to subdivision
    tensor products and homotopies

    Presentations I gave in Paris and Galway in 2014 are available on my preprint page. It seems to me we need a variety of models of algebraic data, and the relations between them, of Dold-Kan type, and comparison and evaluation. There are "broad" and "narrow" algebraic models, and the equivalence, usually non trivial, enables one to hop between them at will. This freedom, and comparison and evaluation, is better than sticking to one model.

    Good to see variations are being looked at, and I look forward to hearing more.
  1. In response to a question about exactly this notion of cubical set, I made a few remarks about it here. As I wrote there, I agree with you, Mike, that this notion of cubical set would seem to be very well suited to homotopy type theory, for the reasons I give there.

    One can work with it in the same way as I am doing in the thread in which I am writing up material on the homotopy hypothesis and the foundations of cubical homotopy theory, namely making use of the 2-universal property.

    I am not aware that anyone has studied in depth the notion before. In particular, I am almost certain that it does not appear in the work of Brown and Higgins or in the work of Grandis, or in any work of Cisinski or Maltsiniotis.

    I have not seen Evrard’s preprint, but have long hoped to do so. If anybody has a copy and could scan it, I would be very grateful!

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMar 29th 2015

    Thanks! I’d be interested to see the Evrard preprint too, if anyone can track it down. I just looked at the Grandis-Mauri paper and didn’t see any diagonals (although they consider most of the other possible variations), so it does seem as Richard says that they have mostly been missed.

    • CommentRowNumber7.
    • CommentAuthorspitters
    • CommentTimeMar 29th 2015

    One disadvantage is that it is not Reedy. In fact, already the symmetries destroy this. So the techniques used by Cisinski to model type theory do not work directly. Also, I found a reference that claimd that diagonals break the Dold-Kan correspondence.

    However, I am quite happy with this model. I’ve checked using Cisinski machinery that cubes with diagonals (and possibly other structure) from a strict test category. Moreover, the Grothendieck-Cisinski model structures on cubical sets and on cubical sets with extra structure are Q-equivalent. This will probably not be a big surprise to the experts, but I was happy to have it clear for myself. I’ve also computed the classifying topos for cubical sets with extra structure.

    • CommentRowNumber8.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 29th 2015

    Worth asking on the ALG-TOP and categories mailing lists for a copy of the preprint?

    • CommentRowNumber9.
    • CommentAuthorronniegpd
    • CommentTimeMar 29th 2015
    Another comment: connections arose for us to obtain the notion of commutative cube and to get an equivalence between crossed modules and certain kinds of double groupoids: see the Brown Spencer Cahier paper, 1976. I doubt the latter equivalence works if you allow diagonals. This relates to spitters' comment about Dold-Kan. Cubical abelian groups with connections are equivalent to chain complexes.

    Horses for courses?
    • CommentRowNumber10.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 29th 2015
    • (edited Mar 29th 2015)

    A quick remark: it seems to me perfectly possible to have both connections and diagonals. Just take the ’free cartesian category’ on a slightly larger category, just as one takes the ’free monoidal category’ on slightly larger category when defining cubical sets with connections in the usual sense. Of course, one has to be careful to interpret ’free cartesian category’ in a correct sense: for example, in a way similar to the notion of the ’free monoidal category on a monoidal datum’ that I discussed here.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMar 30th 2015

    I’m told that Coquand and his collaborators are now working with a version of cubical sets that have both diagonals and connections, and also possibly reversals. That’s interesting about Dold-Kan, I don’t have any intuition for why that should be.

    • CommentRowNumber12.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMar 30th 2015

    @spitters Could it be that this problem is analogous to simplicial sets vs symmetric simplicial sets, i.e., perhaps if we use oriented cubes with diagonals, then we might get a Reedy category?

    • CommentRowNumber13.
    • CommentAuthorronniegpd
    • CommentTimeMar 30th 2015
    As a kind of nonablian Dold-Kan on dimension 2, given a crossed module $\mu : M \to P$ with $P$ a group, one defines a one vertex double groupoid with edges elements of P and squares quintuples (m; a,b,c,d) such that \mu(m) = b^{-1}a^{-1}cd. So m measures the non-commutativity. So how can we choose a diagonal?
  2. Regarding #11: it is certainly very simple to add reversals as well (I usually refer to these as ’involutions’).

    I would find it interesting if a model of Martin-Löf type theory in cubical sets with involutions exists. As far as I know, the prevailing point of view is that types in Martin-Löf type theory should be thought of as weak \infty-groupoids, but, in a model in cubical sets with involutions, one would (presumably) be modelling inverses strictly.

    • CommentRowNumber15.
    • CommentAuthorspitters
    • CommentTimeMar 31st 2015

    According to Coquand, cubes with diagonals is what Grothendieck called the simplest test category in prusuing stacks. Steve Awodey was the first to lecture about it at the IHP this spring, as far as I recall.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeApr 1st 2015

    Yes, all of the nice categorical facts about diagonals that I mentioned in #1 are AFAIK due to Steve Awodey.

    Re #14, I don’t think “strict inverses” necessarily make a notion of \infty-groupoid too strict. Symmetric simplicial sets, for instance, have strictly involutory inverses but still model all homotopy types.

    • CommentRowNumber17.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 1st 2015
    • (edited Apr 1st 2015)

    I completely agree. My point was specific to the case at the hand: the immediate way in which I can imagine involutions being used within a cubical model of Martin-Löf type theory would be one which would seem to me to correspond to modelling inverses (when viewing types as \infty-groupoids) strictly. This is not to say that this is incompatible with viewing types as weak \infty-groupoids, just that it seems to me that it would say something interesting about this viewpoint.

    Regarding the appearance of the category of cubes with diagonals in Pursuing Stacks as the ’simplest test category’, I believe that the specific reference is pg.48 in Grothendieck’s pagination (§34), pg.82 in the pdf available from Maltsiniotis’ page. There are some further brief ’cubical’ references on pg.69 in Grothendieck’s pagination (§42), pg. 103 in the pdf.

    I know Pursuing Stacks quite well, and I’m pretty certain that Grothendieck does not use cubical categories specifically very much at all, beyond these occasional observations.

    Regarding the first sentence in #14: I have not thought about the remark about classifying topoi, but the other facts that you mentioned, Mike, and the fact that Bas mentioned that cubes with diagonals are a strict test category, are of course more or less immediate! I would say that the main observation of significance is the possible suitability of cubical sets with diagonals for modelling type theory. And, as you can see from the remarks that I made that I linked to in #5 having not thought very much about cubical sets with diagonals before, this is not too much of a leap if one has cubical sets and type theory floating around in one’s mind!

    I should say that I have certainly considered the possibility of making use of diagonals before, but have always found a way to carry out what I needed to do in the non-cartesian setting. I had not considered the relevance for modelling type theory until the question I received, linked to in #5, though. One aesthetic reason that I personally prefer the usual category of cubical sets, at least for most purposes, is that I find the free construction simpler than the free cartesian one. In addition, for many purposes, one can ’make available’ connections, diagonals, involutions, and even compositions, inside just ordinary cubical sets. I made some remarks about this here. Since the setting of ordinary cubical sets is simplest and most general, it is therefore natural to work here unless there are strong reasons to do otherwise (and I do think, as I have already mentioned that, for the modelling of type theory, there are strong reasons for using cubical sets with diagonals).

    I can also take the opportunity to point out, in case anybody was wondering and had not already noticed this, that the category that Ronnie Brown mentions Evrard as studying in #4 is not the category of cubes with diagonals: it also, for example, has connections.

    • CommentRowNumber18.
    • CommentAuthorspitters
    • CommentTimeApr 2nd 2015

    Richard, about #17. Do you have more information about the work by Evrard?

  3. No, unfortunately not. My observation just refers to the category that Ronnie Brown mentioned in #4.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeApr 15th 2015

    What is the status of any version of cubical objects internal to a sheaf topos over some site modelling the hypercomplete \infty-topos over that site, the way that simplicial objects do?

    • CommentRowNumber21.
    • CommentAuthorZhen Lin
    • CommentTimeApr 15th 2015

    Doesn’t Jardine have a result along those lines?

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeApr 15th 2015
    • (edited Apr 15th 2015)

    Thanks! I was aware of Jardine’s work on the homotopy theory of cubical sets, but I had missed that he considered cubical (pre-)sheaves and related them to simplicial (pre-)sheaves.

    So theorem 71 in that article that you pointed to is the kind of statement I was asking about.

    This states an equivalence of homotopy categories. Does it lift to an equivalence of infinity-categories?

    And is there any indication that the cubical type theory of Coquand et al. would have interpretation in these cubical (pre-)sheaves? I mean, broadly speaking this is clear, given that their ambient type theory should interpret right away in the (pre-)sheaf 1-topos, but I suppose there must be a subtlety somewhere when it comes to equivalence of types to be interpreted as local weak equivalence in the model category of cubical (pre-)sheaves.

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeApr 15th 2015

    The first issue is that dependent types in cubical type theories have to get interpreted by “algebraic fibrations” satisfying a “uniform” Kan condition. AFAIK it’s unknown whether every ordinary Kan fibration of cubical sets can be uniformized (classically, I mean; constructively we shouldn’t expect it, but classically the analogous result for simplicial sets is true, so it might be true cubically too). Moreover, I don’t know whether it’s known whether either sort of Kan fibration is actually the fibrations for some model structure presenting the correct homotopy theory (i.e. having the right weak equivalences). I think there’s a good chance of it for cubical sets, but for cubical presheaves I’m more doubtful; it seems more likely that there they would correspond to some kind of free \infty-exact completion of the presheaf 1-topos.

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeApr 16th 2015

    Thanks, Mike!

    Ah, that sounds not so promising. I hope somebody is looking into these issues?

    Might there be a way to handle this purely type-theoretically, say by showing that the cubical theory is conservative over the theory from the book, so that one might not need to worry about cubical models but could maybe interpret the cubical TT in the book-HoTT and stick to worrying about models for the latter?

    Meanwhile, I have created a minimum entry model structure on cubical presheaves, just to record that theorem 71 of Jardine03, and cross-linked a bit.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeApr 16th 2015

    I hope so too! (-: It’s on my list of things to do, of course, but it’s a little ways down there, so I’d be ecstatic if someone else got to it first. Unfortunately, as you know, there aren’t enough people working on HoTT who have sufficient background in homotopy theory to really attack questions like these.

    Possibly I was too discouraging about cubical presheaves. Now that I think about it some more, I think the cubical type theory requires that the fibrations be in particular uniform Kan, but they could actually be a smaller class. That sounds more promising, e.g. maybe all injective fibrations are uniformizable? Or maybe there is an intermediate model structure that would work? We would, I think, want all objects to be cofibrant, but I’m not sure whether that restricts us to the injective model structure or whether there is some more wiggle room in the cofibrations while keeping the cofibrant objects the same. There would also still remain the problem of a universe.

    It would certainly work if we could show that Cubical HoTT is conservative over Book HoTT. But I don’t have any ideas for how to do that other than by essentially constructing a model of Cubical HoTT in Book HoTT, which would a fortiori yield a model of Cubical HoTT in simplicial presheaves etc.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeApr 16th 2015

    Thanks. Indeed, I am well aware that the hot part of HoTT is to a large extent carried by your shoulders. I am amplifiying this to whoever wants to listen. In fact we had discussion along these lines two weeks back in Bristol.

    But here my hope was more specific than the general purpose hope that you find enough time and energy to push further with this. Namely here I was getting worried that nobody made some plausibility checks that the cubicalTT, despite its promising superficial appearance, has a chance to have the right models and not turn out to be a dead-end.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeApr 16th 2015

    Your worry is entirely justified; as far as I know, no one has made any such plausibility checks, because most of the people working on cubical things are not semantically minded. I myself have only recently been convinced that cubical TT is worth looking seriously at.