homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
This page considers the homotopy type of the loop space of a wedge sum of circles. For the moment, the following is entirely geared towards the language of homotopy type theory.
Let $A$ be a set, and consider the HIT $W_A$ with constructors
This is the “wedge of $A$ circles”. It can also be defined as the suspension of $A+1$.
If $A$ has decidable equality, then the loop space $\Omega W_A$ is the free group on $A$.
For general $A$, it is probably still true that the fundamental group $\pi_1 W_A$ is the free group on $A$.
For a general set $A$ without decidable equality, is $W_A$ even a 1-type? What can be said about $\Omega W_A$?
In the classical simplicial set model?, $W_A$ is a 1-type for all $A$, since classically all sets have decidable equality. Moreover, since $W_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_A$ being a 1-type can be found in such models, but it is also not clear how to prove that $W_A$ is a 1-type.
Last revised on June 6, 2022 at 20:14:33. See the history of this page for a list of all contributions to it.