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 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 limit 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 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 subobject 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).
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeOct 4th 2013

    In the HoTT book, there's all these great slick proofs of classical results from homotopy theory in Chapter 8, but then there's this tricky stuff about constructive definitions of the real numbers in Chapter 11. And they don't have much to do with each other. But historically, these subjects have been closely related: not only does the definition of the fundamental group involve the unit interval in the real line; knowing the fundamental group of the circle allows us to prove the Brouwer fixed point theorem (and thence the Jordan curve theorem), for example. I could some algebraic topologists might claim that the subject matter of Chapter 8, while interesting, simply is not their subject matter.

    Has any work been done on constructing classical homotopy theory (which is about homotopy 0-types equipped with subframes of their power frames) in HoTT and then showing that this is an internal model of HoTT itself, allowing the results of Chapter 8 to be reflected in results about analysis?

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 4th 2013

    Presumably there will be parts of classical homotopy theory which are due to the specificity of the ((,1)(\infty, 1))-category they’re working in.

    Is something relevant here the way Eckmann-Hilton duality fails in Top, because of a lack of arrow-reversing duality in the latter

    …a pullback of a cofibration by a fibration is a cofibration, but a pushforward of a fibration by a cofibration is not a fibration.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeOct 7th 2013

    Presumably there will be parts of classical homotopy theory which are due to the specificity of the ((,1)(\infty, 1))-category they’re working in.

    Certainly strict homotopy will not show up in HoTT. But there is a lot of classical homotopy theory (for example, the result π 1(S 1)\pi_1(S^1) \cong \mathbb{Z}) that is also true in HoTT's native homotopy theory, but we still don't know (or at least I don't) how to conclude the classical theorem (about functions between the set of real numbers and related sets) from the native one. (For simplicity, let us work in HoTT + EM, to obviate any considerations about the correct constructive notion of continuous map.)

    • CommentRowNumber4.
    • CommentAuthorjim_stasheff
    • CommentTimeOct 7th 2013
    ``In the HoTT book'' - has anyone had experience with the systems Git and GitHub.com used to create the book?
    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeOct 7th 2013

    If you’re willing to work in HoTT+AC, then all of classical homotopy theory can be developed internally and shown to be a model of HoTT, in exactly the same way that classical homotopy theory inside ZFC can be shown to be a model of HoTT. No one has written this out explicitly, but if you believe that ETCS(perhaps +R) is as good a foundation for mathematics as ZFC, then you should believe this, because chapter 10 shows that the hsets in HoTT satisfy ETCS. I should point out, though, that even in ZFC, it’s not topological spaces that model HoTT directly, but rather simplicial sets.

    On the other hand, the existence of any constructive model of HoTT is a topic of current research. Simplicial sets don’t seem to work without at least LEM; I don’t know whether they work with LEM but without AC. Thierry and Marc have recently claimed that cubical sets do work constructively, at least if you give up judgmental computation for identity types. If this is right, then you could perform their proof inside the hsets of HoTT to construct an internal model of HoTT. (I do think some work would be required to conclude that HoTT still looks mostly familiar even without judgmental Id-computation.)

    Relating simplicial or cubical sets to topological spaces constructively is another question. It seems clear that any space will still have a singular simplicial or cubical set. Will it be sufficiently fibrant?

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeOct 7th 2013

    @jim: I have some experience with both (including helping to write the book). What do you want to know? (Although maybe this would be better as a separate thread.)

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeOct 7th 2013

    Thanks, Mike! It's interesting that people even want to use AC, since such elementary results as π 1(S 1)\pi_1(S^1) \cong \mathbb{Z} seem pretty constructive (requiring at most the fan theorem). Still, I can imagine that general results would need more.

    If we wished to prove the Brouwer fixed point theorem in HoTT + AC using the homotopy-theoretic argument, would it be shorter to do a proof purely in the ETCS fragment, or to use the slick homotopy-theoretic results from HoTT together with the reflection of this in simplicial h-sets? I'm guessing the former.

    I suppose that the bottom line is that there's still a lot of work to do.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeOct 8th 2013

    I expect it’s probably less that people want to use AC as that algebraic topologists are classical mathematicians and it doesn’t even occur to them to try to avoid it.

    There may be another level of confusion going on, by the way: my #5 was about building a model of HoTT inside of HoTT, but another thing you could do is stay with only one model of HoTT and ask how spaces (i.e. hsets with subframes of their power frames) give rise to “fundamental types” in that same model of HoTT. Your second paragraph seems to me to suggest that approach, which we don’t even exactly know how to do yet — the fundamental type should be a HIT of some sort, but there’d have to be some way to package up its a-priori infinitely many constructors.

    In any case, however, I think you’re right that there’s going to be some amount of work in connecting topological spheres to homotopical ones. It’s not even obvious to me that, say, the fundamental type of the topological nn-sphere, for n>1n\gt 1, is (constructively) the HIT nn-sphere.

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeOct 8th 2013

    stay with only one model of HoTT and ask how spaces (i.e. hsets with subframes of their power frames) give rise to “fundamental types” in that same model of HoTT

    This would be ideal. The constructors would be simplices (in the concrete classical-analytic sense: pointwise continuous functions from a power of the h-set of real numbers).

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 9th 2013

    I guess if all you want is to prove the Brouwer fixed point theorem, then you only need the fundamental 1-type, and that won’t be hard to define. But I still don’t see an immediate way to identify the fundamental 1-type of the topological circle with the HIT circle.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeOct 9th 2013

    It seems to me that such an identification ought to be doable, at the level of homotopy equivalence between types, or something is wrong. They both ought to be equivalent to the one-object groupoid whose automorphism group is \mathbb{Z}.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeOct 9th 2013

    Yes, certainly; I spoke confusingly. I meant, I don’t yet see a way to identify them without first proving that each of them is equivalent to that. In other words, I don’t see how to use the calculation of π 1\pi_1 of the HIT circle to tell us something that we didn’t already know about the topological one.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeOct 9th 2013
    • (edited Oct 9th 2013)

    A slightly off-topic but related remark and question:

    I heard from the recent meeting in Oxford that some of the non-logician big shots attending showed irritation upon being exposed to enthusiastic advertizement of the existence of a computation of π 1\pi_1 of the circle in HoTT.

    In Barcelona I experienced what is maybe the converse of this: HoTT theorists jumping at me for calling some classical fact “simple”, emphasising that in HoTT it takes a hundred lines of Coq code and hence is not at all simple.

    I know some big names in homotopy theory who look down on the whole HoTT program based on this impression that it’s just simple facts being rederived in a seemingly inappropriate way.

    In these conversations, I am trying to argue for HoTT. I am trying to point out that computing the homotopy group of the circle is not meant to be a big deal in itself (even if the concrete code that accomplishes is a genuine accomplishment which these critics wouldn’t be able to reproduce without considerable effort), but rather a proof-of-principle that is meant to open the door to a source of genuinely new insights in homotopy theory.

    I noticed that the announcement of the Peter Lumsdaine et al. proof of Blakers-Massey theorem goes in this direction.

    But my question is: did anyone try to write an exposition “Why should pure homotopy theorists care about HoTT?” Is there a section in the book dedicated to this, maybe? (I had once started that nLab page HoTT methods for homotopy theorists but it doesn’t quite get to this point yet.)

    I think a good explanation of why pure homotopy theorists should get excited about the existence of a constructive proof of π 1(S 1)=\pi_1(S^1) = \mathbb{Z} would have considerable sociological value. I was pleased to see homotopy theorist Jack Morava attend the HoTT meeting in Bacelona, but he is clearly an exception in his broadness of appreciation of ideas. It would be great fun if the next HoTT conferences had more and more pure homotopy theorists attending. but I think that will take some more convincing. Of course that will eventually happen by itself as the field proceeds. But maybe an advertizement right now might help a lot.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 9th 2013

    If we wanted to look at a case we already now much more about, why not compare

    1. Construction of proofs in higher-order intuitionistic logic
    2. Study of topos theory
    3. Work within a particular topos, e.g., Set.

    Could we say that convincing a homotopy theorist of the benefits of HoTT, will be like convincing (3) that (1) is important? Might they not think that to they extent they want any general theory, and this may not be great, they can receive it from (2)?

    Similarly, won’t a homotopy theorist look first to Higher Topos Theory and Higher Algebra before The HoTT Book, if they look anywhere at all? I guess one should distinguish between a homotopy theorist who just cares about the homotopy of spaces, and one interested in seeing homotopic constructions applied more generally.

    Perhaps the first task is to persuade people that (2) profits from (1), so that any credit due to (2) is shared with (1).

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeOct 12th 2013

    I think the answer to your question, Urs, is “no, not yet”. Personally, I haven’t tried to write such a thing partly because I’m not sure that we have a very good case yet. I feel that it would consist mostly of “the fact that we can do A suggests that maybe someday we’ll be able to do B, and that might be useful to you”. And maybe the people able to appreciate such an argument aren’t the ones we have a problem reaching out to anyway.