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.
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 to be the free cartesian monoidal category generated by an object and two points (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 preserves finite products (being determined by the universal property of ) 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?
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.)
I would suggest to ask Cisinski and Maltsiniotis, if you haven’t already.
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!
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.
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.
Worth asking on the ALG-TOP and categories mailing lists for a copy of the preprint?
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.
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.
@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?
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 -groupoids, but, in a model in cubical sets with involutions, one would (presumably) be modelling inverses strictly.
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.
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 -groupoid too strict. Symmetric simplicial sets, for instance, have strictly involutory inverses but still model all homotopy types.
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 -groupoids) strictly. This is not to say that this is incompatible with viewing types as weak -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.
Richard, about #17. Do you have more information about the work by Evrard?
No, unfortunately not. My observation just refers to the category that Ronnie Brown mentioned in #4.
What is the status of any version of cubical objects internal to a sheaf topos over some site modelling the hypercomplete -topos over that site, the way that simplicial objects do?
Doesn’t Jardine have a result along those lines?
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.
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 -exact completion of the presheaf 1-topos.
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.
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.
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.
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.
1 to 27 of 27