Two Queries about Univalent Foundations
Timothy Y. Chow
tchow at math.princeton.edu
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