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

- Daniel M. Kan,
*Abstract homotopy. I*, Proceedings of the National Academy of Sciences 41:12 (1955), 1092–1096. doi.

Kan switched to simplicial sets in Part III of the series.

]]>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:

The category of cubical sets admits a Cisinski model structure. See the article model structure on cubical sets for more information.

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

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

]]>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 $X \rightarrow N \Pi_{1}(X)$ is a homotopy equivalence. Indeed, one can *almost* construct a morphism $N \Pi_{1}(X) \rightarrow S \left| X \right|$, which does the same as the functor $\epsilon$ 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 $\mathsf{Top}$, 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!

]]>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 $\square^{1}$ in $\square^{n} = \underbrace{\square^{1} \otimes \cdots \otimes \square^{1}}_{n}$. Thus, for instance, it would work if one took the monoidal structure on $\mathsf{Set}^{\square^{op}}$ to be symmetric.

I have also added a little pictorial notation to cubical set, and removed this from homotopy hypothesis for 1-types.

]]>Have now fixed the definition of $\square_{\leq 1}$. One can add further structure, such as an ’involution’ endomorphism of $I^{1}$, but these are not part of the simplest category of cubes described at the page.

]]>Thanks very much, yes, I tried to cut some corners here, with the predictable consequences! Will fix later.

]]>The definition in category of cubes doesn’t look right to me. Specifically, that of $\square_{\leq 1}$: surely there are non-identity endomorphisms of $I^{1}$?

]]>Actually, the definition of a horn is not yet correct. Will fix it later.

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

]]>