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.
See the perhaps amusing, perhaps sad, discussion here on the fom mailing list about what Frenkel might have meant when he was referring in a NYT article to HoTT.
It seems that despite all the good publicity efforts, there are people who have no idea what it’s about. I’m just waiting till the hard-bitten veterans weigh in…
It’s nice that you weighed in, but I wouldn’t worry too much about those guys (especially the “veterans”, not naming any names for the moment). Those who wish to understand will make an effort to do so, and it will become quickly clear who is really serious about that and who is not. I expect HoTT is here to stay; those who are part of the forward momentum should just keep pressing forward and not get distracted by protests of those who are feeling “left behind”. (It’s very good that you mentioned François, since he is intimately familiar with the reverse mathematics culture which is dominant at FOM and would probably be able to communicate the message, more effectively than most in the nLab/HoTT community, to anyone at FOM who is serious about learning more.)
I was amazed that Goldblatt was one person’s first choice to name as being in ’categorical foundations’. But I will let them chunter away now I’ve said my bit and keep quiet. I’m not looking for a repeat of the big late 90s discussion about structural vs material foundations.
Maybe I am not seeing all messages (I see the original question and five replies listed here) but what I see looks not too bad. All replies give some reasonable (if maybe very brief and cursory) idea of what Frenkel must have been referring to. Only Sulzberger concludes by saying that he finds it all very much unclear.
I must say I am glad to learn (I had missed the piece earlier) that Frenkel wrote in the NYT a sensible reaction to the inane “MUH”-thing and did so by almost explicitly pointing to category theory and homotopy type theory. That’s something quite positive, to my mind. (He might have mentioned category theory and homotopy type theory explicitly, but then maybe he thought it wouldn’t help his point to start mentioning technical terms which close to no readers could be expected to have the first idea of.)
Agreed, nothing that is too bad there as we speak. Michael Carroll had the notion it was topos theory (i.e., 1-topos theory), and the others think it’s HoTT. There is a bit of garbling but nothing to worry about particularly.
The work by Feferman on unlimited category theory is cited on FOM. Did anyone read this? Does universe polymorphism give an answer to these questions? I don’t have the time to look into this now, but someone may have looked at it already.
I’ve read it, Bas, but universe polymorphism is not really what Sol is after here. Rather, he wonders about systems where we literaly have U in U, but restrict things in some other way so as to make things work. It’s not likely there’s a good solution to this. (NFU and anti-foundation have their own problems.)
Sol had previously discussed a kind of universe polymorphism in his paper, Typical Ambiguity: Trying to Have Your Cake and Eat it too. The advantage of the approach there in comparison with the usual hierarchy of universes is that he builds a system with hierarchy of universes over ZF(C) that is nevertheless conservative over ZF(C). I don’t know whether it’s possible to do anything similar in type theory, but the advantage is that each universe is “typical”: it satisfies the same properties as the “full” universe. (Edit to clarify: with respect to properties not involving universes, of course.)
I don’t know whether it’s possible to do anything similar in type theory,…
Have you seen Mike Shulman’s post Universe Polymorphism and Typical Ambiguity?
I don’t know whether it’s possible to do anything similar in type theory,… Have you seen Mike Shulman’s post Universe Polymorphism and Typical Ambiguity?
I have (and I just skimmed it again), but while it’s a great introduction to universe polymorphism, I don’t think it addresses the issues of
It’s my impression that there would be obstacles to having these in dependent type theories. For instance, regarding 2, we have that universe n is not an n-type.
Also note that Mike plays on the other meaning of “typical” – as having to do with types – which I’m sure was also Russell’s intention way back when.
For instance, regarding 2, we have that universe n is not an n-type.
Yes, but the universe type really should be an -type anyway, so I don’t think this is a serious problem.
For instance, regarding 2, we have that universe n is not an n-type. Yes, but the universe type really should be an -type anyway, so I don’t think this is a serious problem.
Right.
Suppose that we work in a version of Feferman’s theory ZFC/S with an infinite number of reflective models of ZFC, which is conservative over ZFC. I would speculate that we can use those “universes” to build a model of type theory with a hierarchy of universes in the usual way, modulo a bit of care to avoid second-order replacement. It seems that the universes in the resulting model should be “generic” in some sense, although I don’t know immediately how to express that inside type theory.
1 to 12 of 12