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
Sometimes we can equip a type with a certain structure, called an -algebra structure, allowing us to derive some nice properties about the type and 0-truncate it to form monoids.
An -space is a homotopy associative H-space (but no coherence is required of the associator).
An -monoid is a monoid internal to the classical homotopy category of topological spaces Ho(Top), or in the homotopy category of pointed topological spaces, which has a unit up to homotopy.
Both notions coincide in homotopy type theory. An -space or H-monoid consists of
A homomorphism of -spaces between two -spaces and consists of
A function such that
A function
such that the left unitor is preserved:
such that the right unitor is preserved:
such that the associator is preserved:
The integers are an -space.
Every loop space is naturally an -space with path concatenation as the operation. In fact every loop space is a -group.
The type of endofunctions has the structure of an -space, with basepoint , operation function composition.
A monoid is a 0-truncated -space.
Created on June 9, 2022 at 10:21:02. See the history of this page for a list of all contributions to it.