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
A pointed homotopy type could be called linear (following the terminology of linear model category) if the canonical morphism
from the suspension object of its loop space object is an equivalence.
By Goodwillie calculus the tangent (∞,1)-topos of some (∞,1)-topos is the localization of the classifying (∞,1)-topos (of pointed objects), that regard each pointed finite powering of the generic pointed object as a linear homotopy type.
See at excisive functor – Characterization via the generic pointed object.
Therefore a pointed homotopy type such that all its finite pointed powers are linear could be called a stable homotopy type.
For an (∞,1)-topos and its tangent (∞,1)-topos, then all homotopy types in are stable in this sense, these are equivalently the spectrum objects in .
An account using modal homotopy type theory is in
Last revised on June 8, 2022 at 06:21:11. See the history of this page for a list of all contributions to it.