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 -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 -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 -space consists of
A coherent associative H-space or coherent -space is a non-coherent associative H-space which additionally has the coherence condition
since and are elements of the identity type .
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 and is a function 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 of the left unitor of .
Similarly, the right unitor is preserved, i.e. there is a specified homotopy identifying the concatenation of identifications
with the image of the right unitor of .
The associator is preserved in an analogous way.
A homomorphism of coherent associative H-spaces between two coherent associative H-spaces and is a homomorphism of non-coherent associative H-spaces 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 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 -group (although this is difficult to express in type theory).
The type of endofunctions has the structure of an associative H-space, with basepoint , operation function composition. Once again the operation is coherent, so this is an -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.