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
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
More information about the FOM
mailing list