Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory object of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  1. 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.

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

    • CommentRowNumber3.
    • CommentAuthorCharles Rezk
    • CommentTimeApr 17th 2016

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

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

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

    • CommentRowNumber6.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 17th 2016
    • (edited Apr 17th 2016)

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

    • CommentRowNumber7.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 21st 2016
    • (edited Apr 21st 2016)

    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 XNΠ 1(X)X \rightarrow N \Pi_{1}(X) is a homotopy equivalence. Indeed, one can almost construct a morphism NΠ 1(X)S|X|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 Top\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!

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

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

    diff, v79, current

    • CommentRowNumber10.
    • CommentAuthorDmitri Pavlov
    • CommentTimeNov 28th 2021

    Added:

    Model structure

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

    diff, v80, current

    • CommentRowNumber11.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 11th 2022

    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.

    diff, v81, current

    • CommentRowNumber12.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 11th 2022

    Added (but really there should be many more references…):

    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.

    diff, v82, current

    • CommentRowNumber13.
    • CommentAuthorEvan Cavallo
    • CommentTime14 hours ago

    Merge material from cubical set - exposition.

    diff, v85, current