Homotopy Type Theory
loop space of a wedge of circles (Rev #4)

Let AA be a set, and consider the HIT W AW_A with constructors

  • base:W Abase:W_A
  • loop:A(base=base)loop : A \to (base = base).

This is the “wedge of AA circles”. It can also be defined as the suspension of A+1A+1.

Known facts

  • If AA has decidable equality?, then the loop space ΩW A\Omega W_A is the free group on AA.

  • For general AA, it is probably still true that the fundamental group π 1W A\pi_1 W_A is the free group on AA.

An open problem

For a general set AA without decidable equality, is W AW_A even a 1-type? What can be said about ΩW A\Omega W_A?

In the classical simplicial set model?, W AW_A is a 1-type for all AA, since classically all sets have decidable equality. Moreover, since W AW_A is definable as a colimit, and being a 1-type is a finite-limit property, this fact is inherited by all Grothendieck (infinity,1)-topoi. Thus, no counterexample to W AW_A being a 1-type can be found in such models, but it is also not clear how to prove that W AW_A is a 1-type.

category: homotopy theory

Revision on September 6, 2018 at 16:37:23 by Richard Williamson?. See the history of this page for a list of all contributions to it.