nLab semi-simplicial object

Idea

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

Definition

In terms of functors

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

$$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 semi-simplicial types in homotopy type theory and see the discussion at (IAS).

Properties

Directedness

As opposed to the simplex category $\Delta$, the subcategory $\Delta_+$ is a direct category.

Examples

• in Sets: semisimplicial set:

• in TopologicalSpaces: semi-simplicial topological space

• in SimplicialSets: semi-Segal space (if extra conditions are met)

• in type theory: semi-simplicial types

Related concepts

• simplicial object

  • simplicial set

  • simplicial object in an (∞,1)-category

• semi-simplicial object

  • semisimplicial set

• semi-category

  • semi-Segal space

• Homotopy Type System (“HTS”)

References

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 $k$-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

• UF-IAS-2012, Semi-simplicial types

Coq-code for semi-simplicial types in homotopy type theory had been proposed in

• Vladimir Voevodsky, semisimplicial.v

but its execution requires augmenting homotopy type theory with an auxilirary extensional identity type, discussed in

• Vladimir Voevodsky, A type system with two kinds of identity types (Feb. 2013) [pdf]

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]