Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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 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

1. • CommentRowNumber1.
   • CommentAuthorRichard Williamson
   • CommentTimeApr 8th 2016
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexI have begun the page [[homotopy hypothesis for 1-types]] with a view to giving a proof. It will take some time before it is complete, I will be building it up gradually. I also added a link pointing to this new page from [[homotopy hypothesis]]. The proof that I will give has some novel aspects, such as using cubical sets, and is I guess slightly original, though it is only really a variation on the usual arguments. It has been known to me for many years.

   I have begun the page homotopy hypothesis for 1-types with a view to giving a proof. It will take some time before it is complete, I will be building it up gradually.

   I also added a link pointing to this new page from homotopy hypothesis.

   The proof that I will give has some novel aspects, such as using cubical sets, and is I guess slightly original, though it is only really a variation on the usual arguments. It has been known to me for many years.

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeApr 11th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexNotation 3 seems to duplicate Notation 2.

   Notation 3 seems to duplicate Notation 2.

3. • CommentRowNumber3.
   • CommentAuthorRichard Williamson
   • CommentTimeApr 11th 2016
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexThanks! I am working offline and then copying in, and sometimes also cutting and pasting things within the edit box too, so this may turn out not to be the only case of this. Do let me know if you find any more. After originally writing some more abstract material which can be found in the revision history, I have removed this and gone with a completely explicit construction of the fundamental groupoid/nerve adjunction. For the proof that I am giving, one needs an explicit characterisation in the end anyway, so one might as well just define it explicitly in the first place. I have also explained one direction of the 'equivalence' part of the Quillen equivalence (although I have not discussed model structures yet). The other direction is the most interesting one, and is the point I am principally looking to explain (it is also where the principal novelty of the proof lies). But in fact the idea of the proof of the other direction is fully present in the direction I have given here, one just needs a little extra step. I will explain this in the next significant update of the nLab page.

   Thanks! I am working offline and then copying in, and sometimes also cutting and pasting things within the edit box too, so this may turn out not to be the only case of this. Do let me know if you find any more.

   After originally writing some more abstract material which can be found in the revision history, I have removed this and gone with a completely explicit construction of the fundamental groupoid/nerve adjunction. For the proof that I am giving, one needs an explicit characterisation in the end anyway, so one might as well just define it explicitly in the first place.

   I have also explained one direction of the ’equivalence’ part of the Quillen equivalence (although I have not discussed model structures yet). The other direction is the most interesting one, and is the point I am principally looking to explain (it is also where the principal novelty of the proof lies). But in fact the idea of the proof of the other direction is fully present in the direction I have given here, one just needs a little extra step. I will explain this in the next significant update of the nLab page.

4. • CommentRowNumber4.
   • CommentAuthorRichard Williamson
   • CommentTimeApr 24th 2016
   • (edited Apr 24th 2016)
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexHave done some re-arranging, moving some things out of [[homotopy hypothesis for 1-types]] to other pages: [[fundamental groupoid of a cubical set and the cubical nerve of a groupoid]] (newly created), and [[cubical truncation, skeleton, and co-skeleton]] (some minor additions). I also now have an idea for addressing the point that I discussed [here](https://nforum.ncatlab.org/discussion/7060/cubical-set/?Focus=57064#Comment_57064), which I hope to write up this evening.

   Have done some re-arranging, moving some things out of homotopy hypothesis for 1-types to other pages: fundamental groupoid of a cubical set and the cubical nerve of a groupoid (newly created), and cubical truncation, skeleton, and co-skeleton (some minor additions). I also now have an idea for addressing the point that I discussed here, which I hope to write up this evening.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeApr 25th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexRight now [[homotopy hypothesis for 1-types]] is looking pretty broken, e.g., the notation references. Please let us know when you have reached a resting spot where you are at momentarily satisfied.

   Right now homotopy hypothesis for 1-types is looking pretty broken, e.g., the notation references. Please let us know when you have reached a resting spot where you are at momentarily satisfied.

6. • CommentRowNumber6.
   • CommentAuthorRichard Williamson
   • CommentTimeApr 25th 2016
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexYes, sorry about that, I did not find time after all yesterday evening to work on the entry. I will post here when I have made the next update (probably this evening).

   Yes, sorry about that, I did not find time after all yesterday evening to work on the entry. I will post here when I have made the next update (probably this evening).

7. • CommentRowNumber7.
   • CommentAuthorRichard Williamson
   • CommentTimeApr 27th 2016
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexHave now fixed the broken stuff at [[homotopy hypothesis for 1-types]] as far as I can see, and made the notation consistent with the changes announced [here](https://nforum.ncatlab.org/discussion/7083/fundamental-groupoid-of-a-cubical-set-and-the-cubical-nerve-of-a-groupoid/?Focus=57217#Comment_57217). Also in light of those changes, added Corollary 2. I am looking forward to writing the other direction of the equivalence, but will not have time this evening. To add to my instiki TODO list: add a \ref{} which works across pages.

   Have now fixed the broken stuff at homotopy hypothesis for 1-types as far as I can see, and made the notation consistent with the changes announced here. Also in light of those changes, added Corollary 2.

   I am looking forward to writing the other direction of the equivalence, but will not have time this evening.

   To add to my instiki TODO list: add a \ref{} which works across pages.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeApr 27th 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexPlease consider relative URLs for cross-links between pages: instead of [Notation 3](https://ncatlab.org/nlab/show/fundamental+groupoid+of+a+cubical+set+and+the+cubical+nerve+of+a+groupoid#NotationFundamentalGroupoid) better to code [Notation 3](fundamental+groupoid+of+a+cubical+set+and+the+cubical+nerve+of+a+groupoid#NotationFundamentalGroupoid) For one its shorter. But also it's more robust: should the domain of the nLab ever change (again), then these relative links will stay intact.

   Please consider relative URLs for cross-links between pages: instead of

     [Notation 3](https://ncatlab.org/nlab/show/fundamental+groupoid+of+a+cubical+set+and+the+cubical+nerve+of+a+groupoid#NotationFundamentalGroupoid)
   

   better to code

     [Notation 3](fundamental+groupoid+of+a+cubical+set+and+the+cubical+nerve+of+a+groupoid#NotationFundamentalGroupoid)
   

   For one its shorter. But also it’s more robust: should the domain of the nLab ever change (again), then these relative links will stay intact.

9. • CommentRowNumber9.
   • CommentAuthorRichard Williamson
   • CommentTimeApr 27th 2016
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexDone, thanks!

   Done, thanks!

10. • CommentRowNumber10.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 27th 2016
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItexMostly as a note for myself, I would also like more details of Corollary 2, eventually.

    Mostly as a note for myself, I would also like more details of Corollary 2, eventually.

11. • CommentRowNumber11.
    • CommentAuthorRichard Williamson
    • CommentTimeMay 5th 2016
    • (edited May 5th 2016)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItexI'm struggling a bit for time, and am unhappy with [[homotopy hypothesis for 1-types]] being in its current state. I will try here to outline how I think a nice proof can be given. Maybe somebody would be so kind as to try to help out with putting it on the nLab page, if they are sufficiently interested. Here is the outline. 1) Replace $\mathsf{Grpd}$ by a category of algebraic structures which I'll denote by $\mathsf{2-CubeGprd}$, which is the same as a strict cubical 2-category also known as edge-symmetric double categories), but where we also have operations which provide certain 2-arrows: one which gives us inverses of 1-arrows 'up to homotopy', for instance. (The category of topological spaces admits the same kind of structural homotopies). 2) Construct an adjunction between 2-truncated cubical sets and $\mathsf{2-CubeGrpd}$ whose left adjoint is as follows: on the 1-truncation, it is the usual free category construction (we will need the explicit description using chains of 1-cubes), and on 2-cubes we do a similar kind of thing, after first throwing in the additional 2-arrows mentioned in 1). Let us denote the left and right adjoints by $L$ and $R$ respectively. 3) We show that the geometric realisation (to topological spaces) of the adjunction morphism $id \rightarrow RL$ is a homotopy equivalence as follows. We first define a morphism $RL(X) \rightarrow S|X|$, which takes a zig-zag to the path obtained by composing together in $|X|$ all the paths in the zig-zag; and does something similar on 2-arrows. Because there is no equivalence relation on the arrows of $L(X)$, this is well-defined. The required homotopy inverse is then the geometric realisation of this morphism post-composed with the co-unit $|S|(X)| \rightarrow |X|$. One constructs the required homotopies using a similar trick, and some structural homotopies which exist in $\mathsf{Top}$. 4) The category $\mathsf{2-CubeGrpd}$ has a Gray-like monoidal structure. One defines a homotopy equivalence in $\mathsf{2-CubeGrpd}$ using this and the obvious interval. One shows that the adjunction morphism $LR \rightarrow id$ is a homotopy equivalence in this sense by the same kind of argument as in 3) (indeed, this kind of argument can be probably be carried out in a purely abstract setting where the required structural homotopies exist). 5) From this, one should be able to deduce the more conventional statement of the homotopy hypothesis, by using the 2-coskeleton. That will then be enough to demonstrate the homotopy hypothesis at the level of homotopy categories. If we get this written up, I can explain how to bring model structures into the picture, etc. I will be doing my best to put this in the entry myself. But I would be exceptionally happy if somebody would be interested in getting into this too. I do promise that there is a very rich and rewarding vein of ideas here! Of course, what I have written here is very sketchy, but I'm happy to elaborate on anything. If people spur me to do so by asking questions, it will probably help the writing up go much faster! If one wishes to give a more conventional argument, one can stick to $\mathsf{Grpd}$ and use homotopy groups. But I prefer the above!

    I’m struggling a bit for time, and am unhappy with homotopy hypothesis for 1-types being in its current state. I will try here to outline how I think a nice proof can be given. Maybe somebody would be so kind as to try to help out with putting it on the nLab page, if they are sufficiently interested.

    Here is the outline.

    1) Replace $\mathsf{Grpd}$ by a category of algebraic structures which I’ll denote by $\mathsf{2-CubeGprd}$, which is the same as a strict cubical 2-category also known as edge-symmetric double categories), but where we also have operations which provide certain 2-arrows: one which gives us inverses of 1-arrows ’up to homotopy’, for instance. (The category of topological spaces admits the same kind of structural homotopies).

    2) Construct an adjunction between 2-truncated cubical sets and $\mathsf{2-CubeGrpd}$ whose left adjoint is as follows: on the 1-truncation, it is the usual free category construction (we will need the explicit description using chains of 1-cubes), and on 2-cubes we do a similar kind of thing, after first throwing in the additional 2-arrows mentioned in 1). Let us denote the left and right adjoints by $L$ and $R$ respectively.

    3) We show that the geometric realisation (to topological spaces) of the adjunction morphism $id \rightarrow RL$ is a homotopy equivalence as follows. We first define a morphism $RL(X) \rightarrow S|X|$, which takes a zig-zag to the path obtained by composing together in $|X|$ all the paths in the zig-zag; and does something similar on 2-arrows. Because there is no equivalence relation on the arrows of $L(X)$, this is well-defined. The required homotopy inverse is then the geometric realisation of this morphism post-composed with the co-unit $|S|(X)| \rightarrow |X|$. One constructs the required homotopies using a similar trick, and some structural homotopies which exist in $\mathsf{Top}$.

    4) The category $\mathsf{2-CubeGrpd}$ has a Gray-like monoidal structure. One defines a homotopy equivalence in $\mathsf{2-CubeGrpd}$ using this and the obvious interval. One shows that the adjunction morphism $LR \rightarrow id$ is a homotopy equivalence in this sense by the same kind of argument as in 3) (indeed, this kind of argument can be probably be carried out in a purely abstract setting where the required structural homotopies exist).

    5) From this, one should be able to deduce the more conventional statement of the homotopy hypothesis, by using the 2-coskeleton. That will then be enough to demonstrate the homotopy hypothesis at the level of homotopy categories. If we get this written up, I can explain how to bring model structures into the picture, etc.

    I will be doing my best to put this in the entry myself. But I would be exceptionally happy if somebody would be interested in getting into this too. I do promise that there is a very rich and rewarding vein of ideas here!

    Of course, what I have written here is very sketchy, but I’m happy to elaborate on anything. If people spur me to do so by asking questions, it will probably help the writing up go much faster!

    If one wishes to give a more conventional argument, one can stick to $\mathsf{Grpd}$ and use homotopy groups. But I prefer the above!