Two Queries about Univalent Foundations

[JOSEPH SHIPMAN]

You wrote:
***
> 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."
***
but this seems to ignore that a combinatorial definition of homotopy groups was already given by Kan in 1958. 

— JS


Sent from my iPhone

> On Feb 17, 2023, at 8:07 PM, Timothy Y. Chow <tchow at math.princeton.edu> wrote:
> 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