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
A semi-simplicial object is like a simplicial object, but without degeneracy maps. In Set it is a semi-simplicial set.
For $\mathcal{C}$ a category or (∞,1)-category, a semi-simplicial object $X$ in $\mathcal{C}$ is a functor or (∞,1)-functor
from $\Delta_+$, the wide subcategory of the simplex category on the injective functions (the co-face maps).
One may try to formulate semi-simplicial types in homotopy type theory. See the discussion at (IAS).
As opposed to the simplex category $\Delta$, the subcategory $\Delta_+$ is a direct category.
in Sets: semisimplicial set:
in SimplicialSets: semi-Segal space (if extra conditions are met)
semi-simplicial object
Homotopy Type System (“HTS”)
For more references see also at semi-simplicial set and semi-Segal space.
Discussion of semi-simplicial fiber bundles is in
M. Barratt, V. Gugenheim and J. C. Moore, On semisimplicial fibre bundles, Amer. J. Math. 81 (1959), 639-657.
S. Weingram, The realization of a semisimplicial bundle map is a $k$-bundle map (pdf)
Discussion of formulation of semsiplicial types in the context of homotopy type theory (for use as discussed at category object in an (infinity,1)-category) is in
Coq-code for semi-simplicial types in homotopy type theory had been proposed in
but its execution requires augmenting homotopy type theory with an auxilirary extensional identity type, discussed in
See at Homotopy Type System (“HTS”) for more on this.
More along these lines is in
Hugo Herbelin, A dependently-typed construction of semi-simplicial types (March 2013) (pdf)
Bruno Barras, Thierry Coquand, Simon Huber, A generalization of Takeuti-Gandy Interpretation (pdf)
Last revised on June 25, 2021 at 10:15:36. See the history of this page for a list of all contributions to it.