the HoT-theoretic circle is noncontractible—but it really feels like it should be contractible, because there’s only one point in there, and it’s definitely equal to itself, so why not just choose one of those equalities? just assign the point to one of the equalities to itself that it enjoys!
but you can’t choose that equality, because functions in type theory don’t actually come from “making assignments”—they only come from the inference rules we put in place when setting up our type (plus any other function-creating inference rules we’ve got floating around). You’ve got to go to the inference rule like it’s a vendor at a bazaar, and trade in some initial data for some final data. we can’t purchase a function from the points in the circle without trading in both what the value should be at that point and what the path that lies over the other equality (loop) should be.
(i still need to work out the details of why we can’t actually find a path lying over loop to trade in, though…)
anyway, this makes me a little skeptical about HoTT as a foundation for math…don’t get me wrong, I think it’s super cool if we can swing it! but is this really how equality and function-creation “ought” to work? are we calling things “the right names”? or…maybe we do need to just accept a fundamental shift in our capabilities, and the foundations of math will be better and more general in certain ways for doing so?
