Let be a set, and consider the HIT with constructors
This is the “wedge of circles”. It can also be defined as the suspension of .
If has decidable equality?, then the loop space is the free group on .
For general , it is probably still true that the fundamental group is the free group on .
For a general set without decidable equality, is even a 1-type? What can be said about ?
In the classical simplicial set model?, is a 1-type for all , since classically all sets have decidable equality. Moreover, since 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 being a 1-type can be found in such models, but it is also not clear how to prove that is a 1-type.