Two Queries about Univalent Foundations

[Timothy Y. Chow]

On Fri, 17 Feb 2023, JOSEPH SHIPMAN wrote:
> but this seems to ignore that a combinatorial definition of homotopy 
> groups was already given by Kan in 1958.

You're referring to Kan's paper, "A combinatorial definition of homotopy 
groups," Ann. Math. 2 (1958), 282-312.  This definition starts with a 
c.s.s. complex, which is not a homotopy-invariant concept.

Basically, anything whose starting point is a set-theoretical definition 
of a topological space isn't going to be completely homotopy-invariant. 
You've got a bunch of unequal things and you have to explain when these 
unequal, a priori non-homotopy-equivalent things are equivalent up to 
homotopy.

Tim