**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 $X_\ast$ could be called *linear* (following the terminology of *linear model category*) if the canonical morphism

$\Sigma \Omega X \longrightarrow X$

from the suspension object of its loop space object is an equivalence.

By Goodwillie calculus the tangent (∞,1)-topos $T\mathbf{H}$ of some (∞,1)-topos $\mathbf{H}$ is the localization of the classifying (∞,1)-topos $\mathbf{H}[X_\ast]$ (of pointed objects), that regard each pointed finite powering $X_\ast^\bullet$ of the generic pointed object $X_\ast$ as a linear homotopy type.

See at excisive functor – Characterization via the generic pointed object.

Therefore a pointed homotopy type $X_\ast$ such that all its finite pointed powers are linear could be called a *stable homotopy type*.

For $\mathbf{H}$ an (∞,1)-topos and $T \mathbf{H}$ its tangent (∞,1)-topos, then all homotopy types in $T_\ast \mathbf{H} \hookrightarrow T \mathbf{H}$ are stable in this sense, these are equivalently the spectrum objects in $\mathbf{H}$.

An account using modal homotopy type theory is in

- Mitchell Riley, Eric Finster, Daniel Licata,
*Synthetic Spectra via a Monadic and Comonadic Modality*, (arXiv:2102.04099)

Last revised on June 8, 2022 at 06:21:11. See the history of this page for a list of all contributions to it.