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
The concept of a homotopy type (homotopy n-type) all of whose homotopy groups are finite groups does not have an established name. Sometimes it is called $\pi$-finiteness. In the context of groupoid cardinality “tameness” is used. In homological algebra “of finite type” is used, which in homotopy theory however badly clashes with the concept of finite homotopy type which is crucially different from homotopy type with finite homotopy groups.
see at K(n)-local stable homotopy theory (…)
∞Grpd is a coherent (∞,1)-topos and a locally coherent (∞,1)-topos. An object $X$, hence an ∞-groupoid, is an n-coherent object precisely if all its homotopy groups in degree $k \leq n$ are finite. Hence the fully coherent objects here are the homotopy types with finite homotopy groups.
(Lurie SpecSchm, example 3.13)
G. J. Ellis, Spaces with finitely many non-trivial homotopy groups all of which are finite, Topology, 36, (1997), 501–504, ISSN 0040-9383.
Jean-Louis Loday, Spaces with finitely many non-trivial homotopy groups (pdf)
Last revised on August 15, 2017 at 10:28:15. See the history of this page for a list of all contributions to it.