semi-simplicial object



Homotopy theory

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



Paths and cylinders

Homotopy groups

Basic facts




A semi-simplicial object is like a simplicial object, but without degeneracy maps. In Set it is a semi-simplicial set.


In terms of functors

For 𝒞\mathcal{C} a category or (∞,1)-category, a semi-simplicial object XX in 𝒞\mathcal{C} is a functor or (∞,1)-functor

X:Δ + op𝒞 X \colon \Delta_+^{op} \to \mathcal{C}

from Δ +\Delta_+, the wide subcategory of the simplex category on the injective functions (the co-face maps).

In homotopy type theory

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.


For more references see also at semi-simplicial set and semi-Segal space.

Semi-simplicial bundles

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 kk-bundle map (pdf)

In homotopy type theory

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

Last revised on February 2, 2021 at 23:19:39. See the history of this page for a list of all contributions to it.