Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory & logic

Topic: weak homotopy equivalence of types

Matteo Capucci (he/him) (Nov 25 2020 at 15:50):

Is there a notion of weak homotopy equivalence in HoTT, i.e. of a function which induces an equivalence of all homotopy groups? Is it true that such a function is automatically an equivalence, since types in HoTT are always finite CW-complexes?

Reid Barton (Nov 25 2020 at 15:54):

Yes, and no. See section 8.8 of the HoTT book, which calls the statement "a map is an equivalence if it induces an isomorphism on all possible homotopy groups" "Whitehead's principle". (Though I find this term somewhat confusing, and would rather call it something like "hypercompleteness".)

Kenji Maillard (Nov 25 2020 at 15:58):

:thinking: Why would types in HoTT be finite CW-complexes ? (for instance $\mathbb{N}$ is not-finite but it's usually constructible in HoTT)

Reid Barton (Nov 25 2020 at 16:00):

Indeed, types need be finite neither in cardinality (e.g. $\mathbb{N}$) nor in the range in which their homotopy groups are nontrivial.

Valery Isaev (Nov 25 2020 at 16:09):

nor in the range in which their homology groups are nontrivial.

Matteo Capucci (he/him) (Nov 25 2020 at 16:34):

Ugh, yes, finite is not the right word. What I meant is 'inductively definable'.

Matteo Capucci (he/him) (Nov 25 2020 at 16:41):

Thanks for the reference @Reid Barton, that's exactly what I was after.
Here's what Reid is referring to:

Whitehead’s theorem is not provable. In fact, there are known models of type theory in which it fails to be true, although for entirely different reasons than its failure for ill-behaved topological spaces. [...] From a foundational point of view, therefore, we may speak of Whitehead’s principle as a “classicality axiom”, akin to LEM and AC. It may consistently be assumed, but it is not part of the computationally motivated type theory, nor does it hold in all natural models. But when working from set-theoretic foundations, this principle is invisible: it cannot fail to be true in a world where ∞-groupoids are built up out of sets (using topological spaces, simplicial sets, or any other such model).

Dan Doel (Nov 25 2020 at 16:50):

What does 'inductively definable' mean? Not all types are inductively defined. Function/pi types are the usual example, but some type theories add others.

Reid Barton (Nov 25 2020 at 16:51):

Moreover, a variable type is not inductively definable

Dan Doel (Nov 25 2020 at 16:52):

Yeah, even if all the ways of forming types were inductive, adding a principle to the language that recognized that might have odd consequences.

Reid Barton (Nov 25 2020 at 16:53):

It would rule out the simplicial set model, for sure

Dan Doel (Nov 25 2020 at 16:53):

Like trying to add 'Church's thesis' (or whatever people call it) to the language merely because all the functions you can write down are computable.

Cody Roux (Dec 04 2020 at 16:11):

Dan Doel said:

What does 'inductively definable' mean? Not all types are inductively defined. Function/pi types are the usual example, but some type theories add others.

Well, in some sense, they are... the meta-theory gets messier though.