Two Queries about Univalent Foundations
Timothy Y. Chow
tchow at math.princeton.edu
Sun Feb 19 08:27:58 EST 2023
On Thu, 16 Feb 2023, I wrote:
> This depends on what you mean by "new insight." The most basic new
> insight is that homotopy groups of spheres can be *defined* in a purely
> homotopy-invariant way. The classical definition using singular
> homology, for example, appeals to the concept of the set of singular
> cochains, and that is not a homotopy-invariant concept.
Someone pointed out that what I wrote above is garbled, a result of too
much editing and not enough proofreading. What I meant to say is that the
classical development of algebraic topology involves defining auxiliary
objects such as topological spaces and singular (co)chains, and even if
the things you're primarily interested in---homology/homotopy groups, for
example---are homotopy-invariant, their definitions rely on auxiliary
definitions that are not homotopy-invariant. One of the main points of
homotopy type theory is to make everything homotopy-invariant from the
ground up.
Sorry for any confusion.
Tim
More information about the FOM
mailing list