Homotopy Type Theory semi-simplicial types > history (Rev #6, changes)

(Here is Vladimir Voevodsky’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 $\Delta{}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:

• CL.pl, the prover for coherent logic (requires SWI-Prolog)
• X.in, a formalization of the model in coherent logic
• X.model, the edges, fill1 and fill2, day by day, generated by the prover from input X.in.
• X.v, a Coq script verifying the proof that no homotopy equivalence between the fibers can exist in the model.

Finite-dimensional parts

For small values of n, it is straightforward to define n-semi-simplicial types.

A 0-semi-simplicial type is just a type $X_0\,:\,Type$.

A 1-semi-simplicial type: $X_0\,:\,Type$, and $X_1\,:\,X_0 \rightarrow X_0 \rightarrow Type$.

A 2-semi-simplicial type:

$X_0\,:\,Type$;
$X_1\,:\, X_0 \rightarrow X_0 \rightarrow Type$;
$X_2\,:\,forall\:(x y z\,:\,X_0)\:(f\,:\,X_1 x y)\:(g\,:\,X_1 y z)\:(h\,:\,X_1 x z), Type$

A 3-semi-simplicial type:

$(X_0,X_1,X_2)$ as before; and
$X_3:\,forall (\text{tetrahedral configurations from} X_0 \ldots X_2), Type$

And so on.

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

• Can we define a function “$\text{Semi-simplicial}\,:\,nat \rightarrow Type$”, such that for $n = 0,1,2,3$, $\text{Semi-simplicial} n$ is (equivalent to) the objects explicitly defined here?

• Can we define a type of semi-simplicial types (i.e. infinity-semi-simplicial types, with $n$-simplicies for all $n$?

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 $\Delta{}i$? Giving a reasonable definition of $\Delta{}i$ is not too hard: the objects [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 $\Delta{}i$ is a direct category, while $\Delta$ is not.

Semi-simplicial Types in Logic-enriched Homotopy Type Theory Fedor Part, Zhaohui Luo (Submitted on 16 Jun 2015)