Two Queries about Univalent Foundations

Timothy Y. Chow tchow at
Thu Feb 16 09:13:28 EST 2023

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 

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

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.


More information about the FOM mailing list