Cool question. =P
]]>Oh, wow, thanks for that detective work.
I have fixed them all now. Thanks for looking into this.
]]>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.
]]>Thanks! (I am also in the category of people you mention.)
]]>Should this link up to classifying (infinity,1)-topos, given the connection between forcing and classifying topos?
]]>on the off-chance that there is anyone besides me who checks MathOverflow less frequently than the 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 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.
]]>