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.
In the article connection on a cubical set the definition of a connection uses two types of maps, denoted Γ^+_i and Γ^-_i. Roughly, the former corresponds to a map of cubes that takes the minimum of some coordinates, whereas the latter takes the maximum of some coordinates.
However, in the book by Brown-Higgins-Sivera in Definition 13.1.3, page 446, only the maps Γ^-_i are used. There they are denoted simply by Γ_i. The paper by Maltsiniotis about the strict test category of cubes with connection also uses the same definition.
Which definition is correct? What is the reference for nLab’s definition and why does it deviate from the definition of Brown-Higgins-Sivera?
I have asked Ronnie who I think wrote the entry originally as I have not time to ferret out the answer which involves a process for turning one into the other I think. If he does not reply I suggest you ask him directly as he usually is very quick to answer. (I know he is around his home base at the moment.)
Of course one can pick and choose as it fits one’s purpose, but by default I would definitely take both the ’upper left’ and ’lower right’ connections to be included. Tim is correct: Ronnie Brown and collaborators do use both as well, it is just that they typically use additional structures (’transport’) which allow to derive one from the other. Marco Grandis uses both types of connections, for a direct reference. I also use both types, in a slightly different setting, in my thesis.
I would need to check, but I believe that Maltsiniotis’ work will go through perfectly well if one uses both types of connections; the main point I think is just that once one has one of them available, one gets strictness. This is really a re-working of an old observation of Ronnie Brown and collaborators that products in cubical sets work better if one has connections.
We started off with the emphasis on the cubical $\omega$-groupoids, so the groupoid structures gave the other connections. The theses of Mosa and of Al-Agl brought in the more general case, see my doctorate’s web page. This was continued with the paper with Al-Agl and Steiner.
For a summary of the cubical history, and some methodology on the use of strict higher structures, see this paper
https://www.sciencedirect.com/science/article/pii/S0019357717300460
on “Modelling and computing homotopy types: I”.
Okay, so I guess both are used. I think it would be better to indicate this in the article explicitly, because as it stands the article is very confusing.
Also, probably the merits/demerits of each variant should be mentioned. I would add this myself if only I knew what to write.
the main point I think is just that once one has one of them available, one gets strictness
Could you elaborate on this point? What does “strictness” mean?
This is really a re-working of an old observation of Ronnie Brown and collaborators that products in cubical sets work better if one has connections.
This is another thing I was wondering about. If we consider the (categorical) product of two 1-cubes as cubical sets with connections, then apart from 2-cubes inside the boundary we seem to get at six proper 2-cubes: a 2-cube of C^1 is given by two maps p,q: C^2 → C^1 (where C^n is an n-cube), both maps must be surjective in order for (p,q) not to be a boundary cube, there are three (or four) different surjective maps C^2 → C^1 (two projections p_1, p_2 and one connection c, using the Brown-Higgins-Severa definition, or two connections c_1, c_2 using the nLab definition). Thus we get 3×3=9 pairs of surjective maps, of which 3 pairs give degenerate simplices, and the remaining 6 give four triangles and two squares: upper triangle in a square: (c,p_1) or (c,p_2) lower triangle in a square: (p_1,c) or (p_2,c) the square itself: (p_1,p_2) or (p_2,p_1).
So the 2-skeleton of C^1×C^1 looks really weird and not at all like an actual square (which is what I would expect it to be). Did I misinterpret something, or is this the expected outcome?
I made some clarifications based on the above comments, please feel free to edit further.
Could you elaborate on this point? What does “strictness” mean?
That the underlying test category is a strict test category, which basically just means that products are preserved up to homotopy.
So the 2-skeleton of $C^1 \times C^1$ looks really weird and not at all like an actual square (which is what I would expect it to be). Did I misinterpret something, or is this the expected outcome?
It is expected. It is the tensor product of cubical sets that behaves in the expected way (and is the one of the main advantages of cubical sets over simplicial sets). There is no real reason a priori to expect the categorical product to look nice. However, it just so happens that the homotopy type is fine with connections, just like with simplicial sets: products of simplicial sets are also pretty horrible combinatorially, but things work out there too. The remark on the page that connections make cubical sets behave more like simplicial sets is very true.
A comment on the actual entry: for me, the ’best’ description of categories of cubical sets of any flavour is to begin with some ’structured interval’, take the free strict monoidal category on that in some sense, and then take presheaves on that. One can do everything without knowing the explicit combinatorics, just using the universal property. However, once connections or other 2-dimensional structures are involved, one has to careful about what ’free strict monoidal’ means, and I don’t think this is in the literature. Even for plain cubical sets, one has to be a bit careful: it is not exactly the free strict monoidal category, but the free strict monoidal category with a specified unit.
Maybe one day I’ll get around to writing up some of this on my personal web. But since I’ve not written it up in 8 or 9 years, who knows if and when it wil happen :-).
Richard: Is that material in your thesis? If so why not put it on your personal web as it is with caveats. (BTW the link to your thesis from your nlab page does not seem to be working.) I know I have a copy ;-) but I am not sure where it is!
I have fixed the link to my thesis now, thanks for mentioning! I am honoured that you still have a copy somewhere!
Unfortunately there is very little of this in my thesis. What I am referring to as ’structured intervals’ are described carefully in the first few chapters. But there is nothing on cubical sets there. I think the only thing I have written on cubical sets that is publically available are these lecture notes. But I’m not really happy with these; in particular, they do use combinatorics, rather than the more conceptual approach of #9. Indeed, I was planning to remove them from my website a few years ago, but they suddenly were cited a bit in the early days of cubical type theory, e.g. by Thierry Coquand. So I felt I had to leave them! Nowadays there are many more people who have thought a lot about this kind of thing, such as Ulrik Buchholtz, so the notes have probably outlived their usefulness; but I suppose I have to leave them up now :-).
I think there are few people who have digested my thesis! I have plenty of ideas on how to take it further (it was originally just a step in a broad programme), and worked on quite a lot of things related to it, though for a few years now I’ve been mainly working on diagrammatic knot theory; I will try at some point to begin putting things up on my personal web from my older work.
Added:
The category of cubical sets with connections is a strict test category and therefore admits a cartesian model structure that is Quillen equivalent to the Kan–Quillen model structure on simplicial sets. This was proved by Maltsiniotis \cite{Maltsiniotis}.
See also the article model structure on cubical sets.
Added:
In complete analogy to simplicial sets, there is also an analogue of the Joyal model structure on cubical sets, with or without connection. See the article model structures for cubical quasicategories.
1 to 14 of 14