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
This entry is about the formulation of sequential spectra in homotopy type theory, specifically of sequential spectra that need not be genuine stable homotopy types in the sense of Omega-spectra and thus may be regarded as “pre-spectra” (they become genuine spectra under spectrification).
In homotopy type theory, a prespectrum or sequential spectrum is a dependent bi-infinite sequence of types $n:\mathbb{Z} \vdash E_n\;\mathrm{type}$ with a dependent bi-infinite sequence of types $n \colon \mathbb{Z} \vdash *_n \colon E_n$ and a dependent bi-infinite sequence of functions $n \colon \mathbb{Z} \vdash e_n \colon E_n \to \Omega E_{n+1}$ which preserves the point, where $\Omega A$ is the loop space type of $A$.
In Coq pseudocode, this becomes
Definition prespectrum :=
{X \colon int -> Type &
{ pt \colon forall n, X n &
{ glue \colon forall n, X n -> pt (S n) == pt (S n) &
forall n, glue n (pt n) == idpath (pt (S n)) }}}.
sequential spectrum (in contrast to an Omega-spectrum)
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Floris van Doorn (2018), On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, (arXiv:1808.10690, web)
Last revised on June 8, 2022 at 23:37:04. See the history of this page for a list of all contributions to it.