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
symmetric monoidal (∞,1)-category of spectra
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
In dependent type theory, an associative H-space (cf. BCFR23) or $A_3$-space is a naive translation of the notion of monoid. If the underlying type is an h-set (such as if the type theory is extensional), then it yields a correct notion of monoid. Otherwise, it is only a “partly-coherent” notion of “homotopy monoid”: a type-theoretic version of the notion of $A_3$-space from homotopy theory.
Similar to the definition of H-spaces, there are coherent and non-coherent versions of associative H-spaces:
A non-coherent associative H-space or non-coherent $A_3$-space consists of
A coherent associative H-space or coherent $A_3$-space is a non-coherent associative H-space $A$ which additionally has the coherence condition
since $\lambda(e)$ and $\rho(e)$ are elements of the identity type $\mu(e, e) = e$.
There are also two different notions of homomorphisms between associative H-spaces, depending on whether the H-space is coherent or not.
A homomorphism of non-coherent associative H-spaces between two non-coherent associative H-spaces $A$ and $B$ is a function $\phi:A \to B$ such that
The basepoint is preserved, i.e. there is a specified identification
The binary operation is preserved, i.e. there is a specified dependent function
The left unitor is preserved, i.e. there is a specified homotopy identifying the concatenation of identifications
with the image $\mathrm{ap}_{\phi}(\lambda_A(x)):\phi(\mu_A(e_A,x)) = \phi(x)$ of the left unitor of $A$.
Similarly, the right unitor is preserved, i.e. there is a specified homotopy identifying the concatenation of identifications
with the image $\mathrm{ap}_{\phi}(\rho_A(x)):\phi(\mu_A(x,e_A)) = \phi(x)$ of the right unitor of $A$.
The associator is preserved in an analogous way.
A homomorphism of coherent associative H-spaces between two coherent associative H-spaces $A$ and $B$ is a homomorphism of non-coherent associative H-spaces $\phi:A \to B$ in which the coherence condition is preserved.
The integers are an associative H-space under addition, as are the natural numbers. More generally, as noted above, any h-set monoid is an associative H-space, and is coherent.
Every loop space type $\Omega_x(X) \equiv (x=_X x)$ is naturally an associative H-space, with path concatenation as the operation. In this case, the operation is in fact coherent, and indeed every loop space is a $\infty$-group (although this is difficult to express in type theory).
The type of endofunctions $A \to A$ has the structure of an associative H-space, with basepoint $id_A$, operation function composition. Once again the operation is coherent, so this is an $\infty$-monoid (inverses need not exist).
The type of coherent H-space structures on a central type is a coherent associative H-space.
Last revised on December 20, 2023 at 15:08:07. See the history of this page for a list of all contributions to it.