Two Queries about Univalent Foundations

Timothy Y. Chow tchow at
Sat Feb 18 08:19:16 EST 2023

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 


More information about the FOM mailing list