Two Queries about Univalent Foundations

[Timothy Y. Chow]

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