Contents

# Contents

## 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 the discussion at (IAS).

## Properties

### Directedness

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

## References

### 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

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 May 12, 2014 at 02:07:45. See the history of this page for a list of all contributions to it.