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