UF IAS 2012 Archive Semi-simplicial types

One interesting open problem (considered by VV and others): define semi-simplicial types in Homotopy Type Theory. (Here is VV's code for a proposed definition.) Classically, a semi-simplicial object in a category is like a simplicial object, but without degeneracy maps; i.e. a contravariant functor from the category **Δ**i, of finite nonempty ordinals and just injections between them. Can we define these internally to the type theory?

Update 3/20: here is a note by Hugo Herbelin on a proposed construction.

Update 4/12: A note on semisimplicial sets by Benno van den Berg.

Update 4/15: A note on a presheaf model for simplicial sets by Marc Bezem and Thierry Coquand

Update 6/24: Accompanying files to Update 4/15:

Finite-dimensional parts

For small values of nn, it is straightforward to define nn-semi-simplicial types. A 0-semi-simplicial type is just a type X 0X_0 : Type. A 1-semi-simplicial type: X 0X_0 : Type, and X_1 : X_0 -> X_0 -> Type. A 2-semi-simplicial type:

A 3-semi-simplicial type:

And so on. Each of these can be tupled up as a single type.

Note: this is only one possible approach! Other approaches to the problem are also possible, and may be better.

More precise success criteria

Obviously, the above specifications admit trivial solutions. Can we give a precise formulation of the goal? Idea: something like “in the simplicial model, or more generally in other homotopy-theoretic model, they should be equivalent to coherent (possibly: Reedy-fibrant) semi-simplicial objects”.

Difficulties with some approaches

Why not imitate the classical definition, using internal functors from the internally-defined category **Δ**i? Giving a reasonable definition of **Δ**i is not too hard: the objects [n][n] are very well-behaved. But defining functors out of it is problematic, because there are coherence issues. One would have to specify the functoriality laws using equations, i.e. inhabitants of equality types, which homotopically we treat as paths. But specified paths in homotopy theory have to be coherent to define a useful notion of functor; thus we need equations between our equations (associativity pentagons, etc), then higher equations between those, and so on forever. Thus we end up with the same problem we had before of specifying infinitely much data using a finite description in type theory.

If one restricts the types involved to h-sets, then this problem should go away; but then one has only defined semi-simplicial h-sets, which are (presumably) strictly less general.

Why semi-simplicial, not simplicial?

With semi-simplicial sets, the “iterated dependency” approach gives us at least a candidate approach for tackling coherence issues. With simplicial sets, it’s hard to see how one might tackle or avoid them. (Comparing it to the semi-simplicial approach, one requires degeneracy maps and equations between them, which lets loose the spectre of coherence again.) Furthermore, reasoning about Kan simplicial sets seems to insist on classical logic. For example, the classical result stating the homotopy equivalence of fibers of a Kan fibration cannot be proved constructively (pdf).

In homotopy-theoretic terms, this is because **Δ**i is a direct category, while **Δ** is not.

Created on April 19, 2018 at 21:16:58 by Univalent foundations special year 2012