Skip to main content
Try Wikispaces Classroom now.
Brand new from Wikispaces.
Pages and Files
Categorical Semantics WG
Coq for UF
Coq Working Group
Formalized Homotopy Theory
Higher Inductive Types
Homotopy Type System
how to add a plugin
IAS program participants
Informal Type Theory
Math in HoTT
Modal type theory
Notation and terminology
Add "All Pages"
One interesting open problem (considered by VV and others): define
in Homotopy Type Theory.
for a proposed definition.)
in a category is like a simplicial object, but without degeneracy maps; i.e. a contravariant functor from the category
, of finite nonempty ordinals and just injections between them.
Can we define these internally to the type theory?
: here is a
note by Hugo Herbelin
on a proposed construction.
A note on semisimplicial sets
by Benno van den Berg.
A note on a presheaf model for simplicial sets
by Marc Bezem and Thierry Coquand
: Accompanying files to Update 4/15:
, the prover for coherent logic (requires
, a formalization of the model in coherent logic
, the edges, fill1 and fill2, day by day, generated by the prover from input X.in
, a Coq script verifying the proof that no homotopy equivalence between the fibers can exist in the model
For small values of
, it is straightforward to define
A 0-semi-simplicial type is just a type
_0 : Type.
A 1-semi-simplicial type:
_0 : Type, and X_1 : X_0 -> X_0 -> Type.
A 2-semi-simplicial type:
_0 : Type;
X_1 : X_0 -> X_0 -> 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 (tetrahedral configurations from X_0…X_2), Type
And so on.
Each of these can be tupled up as a single type.
Can we define a function “Semi-simplicial : nat -> Type”, such that for
= 0,1,2,3, Semi-simplicial
is (equivalent to) the objects explicitly defined here?
Can we define a type of semi-simplicial types (i.e. infinity-semi-simplicial types, with
-simplicies for all
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
? Giving a reasonable definition of
is not too hard: the objects [
] 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
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 (
In homotopy-theoretic terms, this is because
i is a
help on how to format text
Turn off "Getting Started"