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 $\square_{\leq 1}$: surely there are non-identity endomorphisms of $I^{1}$?
Thanks very much, yes, I tried to cut some corners here, with the predictable consequences! Will fix later.
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.
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.
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!
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!).
1 to 9 of 9