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.
on the off-chance that there is anyone besides me who checks MathOverflow less frequently than the $n$Forum:
there was a question on forcing in homotopy type theory. I took the liberty of sharing some thoughts.
My comment reflects topics that we have discussed here at some length already. Nevertheless, when sending this I noticed that some of these discussions need to be better reflected in the $n$Lab. And in particular better than I have commented on them for the moment.
I won’t further look into this right now as I am busy with something else. But later I’d like to come back to this.
Should this link up to classifying (infinity,1)-topos, given the connection between forcing and classifying topos?
Thanks! (I am also in the category of people you mention.)
Urs, post 1, could you possibly change the tag from mistyped homtopy-type-theory to homotopy-type-theory ?
The same typos in 4 other discussions http://nforum.mathforge.org/discussion/4191/autvaction-on-vx, http://nforum.mathforge.org/discussion/4682/liouvillepoincare-cocycle-in-cohesive-homotopy-type-theory, http://nforum.mathforge.org/discussion/4759/atiyah-and-courant-lie-nalgebroids-in-homotopy-type-theory and http://nforum.mathforge.org/discussion/4926/cauchy-real-number.
Similarly wrong tag homtopy-theory instead of homotopy-theory in entries http://nforum.mathforge.org/discussion/4570/axiom-uip, http://nforum.mathforge.org/discussion/5339/differentiable-infinity1category and http://nforum.mathforge.org/discussion/5292/blakersmassey-theorem. The owner of the last tag (Blakers-Massey) is Todd.
If we correct a word in all 8 entries than both spurious tags will hopefully not appear in menu any more, confusing with the correct ones. Thanks.
Oh, wow, thanks for that detective work.
I have fixed them all now. Thanks for looking into this.
Cool question. =P
1 to 6 of 6