Two Queries about Univalent Foundations

[Timothy Y. Chow]

Joe Shipman wrote:
> My second question was specifically about whether Homotopy Type Theory 
> has given any new INSIGHT into homotopy groups of spheres, where "allows 
> some to be computed that could not previously be computed" is a good 
> proxy for "new insight". Independently of caring about foundations and 
> logical strength, I care about homotopy groups of spheres for purely 
> mathematical reasons!

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.  The definition using 
homotopy-type theory, by contrast, allows you to develop constructions and 
proofs that are completely homotopy-invariant, and in particular are 
independent of how you define a "topological space."

The insistence on absolute homotopy-invariance does come at a price, and 
computational complexity is one of the things that suffers.  Asking 
whether homotopy type theory yields improved computational complexity is 
therefore stacking the deck against homotopy type theory in a rather 
unfair way.  It's like asking if a synthetic proof of a theorem in 
Euclidean geometry can be executed faster on a computer than if one 
converts to Cartesian coordinates and runs a highly optimized Groebner 
basis algorithm.  Maybe it can and maybe it can't, but either way, that 
misses the point of why one might seek a synthetic proof.

If you want to read more, then Brunerie's thesis might be a good place to 
start.

https://arxiv.org/abs/1606.05916

David Roberts pointed out to me that pi_4(S^3) = Z/2Z was fully formalized 
in homotopy type theory last year.

https://homotopytypetheory.org/2022/06/09/the-brunerie-number-is-2/

If you adopt the mindset that computational speed is the best measure of 
conceptual understanding, then homotopy type theory might seem to be a 
giant step *backward* in our understanding, since pi_4(S^3) = Z/2Z is an 
old and not especially difficult classical result.  But as I said, this is 
not a helpful way to think about the conceptual insights that homotopy 
type theory offers.

Tim