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.
Made some further tweaks at cubical set. Hopefully the definitions of the boundary functor, and of a horn, are correct now.
Am continuing to work on homotopy groups of a cubical Kan complex.
Actually, the definition of a horn is not yet correct. Will fix it later.
The definition in category of cubes doesn’t look right to me. Specifically, that of : surely there are non-identity endomorphisms of ?
Thanks very much, yes, I tried to cut some corners here, with the predictable consequences! Will fix later.
Have now fixed the definition of . One can add further structure, such as an ’involution’ endomorphism of , but these are not part of the simplest category of cubes described at the page.
Have now also given what should be a correct definition of a cubical horn.
For anybody interested, the approach attempted in Revision 66 would work if one has the extra sructure of ’transpositions’, i.e., one is able to ’interchange’ the (i,j)-th copies of in . Thus, for instance, it would work if one took the monoidal structure on to be symmetric.
I have also added a little pictorial notation to cubical set, and removed this from homotopy hypothesis for 1-types.
My apologies for the lack of updates. I just wished to say that I have been busy, but am still working on things for posting; I have just been trying to find a nice way to deal with a certain point. Maybe somebody else would enjoy thinking about this too.
If you look at the proof of Proposition 11 at homotopy hypothesis for 1-types, you can see that almost the same proof can be given to prove that the geometrical realisation of the adjunction morphism is a homotopy equivalence. Indeed, one can almost construct a morphism , which does the same as the functor of Notation 8, except that glueing and reversal of paths is used in place of composition of arrows and inverse arrows. However, it is only well-defined up to homotopy.
One can get around this by using homotopy groups. But, if one works in , one then needs some non-trivial ’simplicial approximation’ type result. One can work with cubical Kan complexes directly, but this is really just postponing such a result.
If one just ignores the fact that the morphism is not well-defined, the proof goes through perfectly. Thus it seems to me that the ’simplicial approximation’ type result is not really at the heart of the matter, and I would like to avoid it.
I have been thinking about all kinds of ways to get around it: type-theoretic, for instance. Really, I would like to find some way to define the morphism. It need not be exactly topological spaces, just something which will play the same role. I will keep thinking about it, but if anyone has any thoughts, I would be delighted to hear them!
I am not very happy with the definition of a horn at cubical set, because it seems painful to use this definition to construct the homotopy groups of a cubical Kan complex.
A challenge then: let’s come up with a good, constructive way to do this. Probably we will wish to use induction and the monoidal structure one way or another. You can see a ’traditional’ way to do it in III.4 of these notes of mine (somewhat unpolished).
I will not actually use the homotopy groups of Kan complexes anymore at homotopy hypothesis for 1-types, so working on this myself is a lower priority at the moment.
Re-organising and adding a few links to the ’Related entries’ section. At some point we/I should add an Idea section, and try to merge in some of what is at cubical set - exposition (somewhat old timers may recall that there was quite some discussion about the splitting off the latter back in the day; I have changed my mind a bit since those days and now think we should not have two pages, but the latter page is such a mess that it puts me off, which is why I split it off originally!).
Added:
The category of cubical sets admits a Cisinski model structure. See the article model structure on cubical sets for more information.
Added:
The category of cubical sets also admits a Joyal-type model structure, which admits a Quillen equivalence to the Joyal model structure on simplicial sets. See the article model structure for cubical quasicategories for more information.
Added (but really there should be many more references…):
The original reference for cubical sets (based on the previous 1950 paper by Eilenberg and Zilber on simplicial sets) is
Kan switched to simplicial sets in Part III of the series.
1 to 12 of 12