natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
Note: This page is an update of a page initially posted on the wiki of the special year on Univalent Foundations at IAS in 2012-13.
One interesting open problem (considered by Vladimir Voevodsky and others): define semi-simplicial types in Homotopy Type Theory.
Classically, a semi-simplicial object in some category is much like a simplicial object, but without any degeneracy maps; i.e. it is a contravariant functor from the category , of finite nonempty ordinals and just injections between them as morphisms.
Can we define these internally to type theory, that is as a functor from to a type universe in homotopy type theory, in some way?
The initial idea, proposed at IAS, was to represent semi-simplicial types not as a contravariant functor but, iterating the correspondence between fibrations and families, as a family of families, what could be called an “indexed” presentation of semi-simplicial types based on “iterated dependencies”.
To illustrate the idea of semi-simplicial types as families of families of -semi-simplices, let us consider the finite-dimensional parts of such semi-simplicial type:
Let be a type universe. Then,
A -small 0-semi-simplicial type is just a -small type .
A -small 1-semi-simplicial type is -small 0-semi-simplicial type with a family of -small types
A -small 2-semi-simplicial type is a -small 1-semi-simplicial type with a family of -small types
representing triangular configurations from and .
A -small 3-semi-simplicial type is a -small 2-semi-simplicial type with a family of -small types
representing tetrahedral configurations from , and .
And so on.
Each of these can be packed up in single type through product types and dependent function types. Thus, given a type universe ,
Can we define a function “”, such that for , the -small type is (equivalent to) the objects explicitly defined here?
Can we define a type of -small semi-simplicial types (i.e. infinity-semi-simplicial types) with -simplices for all ?
A first sketch of a definition was given in by Voevodsky (2012), suggesting that defining such families requires to define restrictions, then to prove that restrictions of restrictions commute, but then also to prove higher-dimensional coherence conditions on restrictions.
Hugo Herbelin worked at the IAS on a formalization in Coq based on the presentation of with face maps . In Herbelin (2014) he describes the construction in Coq extended with the principle of uniqueness of identity proofs (UIP). UIP was used to cut down the need for higher-dimensional coherence, so morally, it meant that types were actually h-sets. What the construction shows is how to define in all details such alternative presentation of semi-simplicial sets based on iterated dependencies, what can also be seen as an effective and generic construction of matching object representatives in a semi-simplicial set.
To cut the need for higher-dimensional coherences, several extensions of homotopy type theory were considered:
Vladimir Voevodsky proposed Homotopy Type System (HTS), a homotopy type theory extended with non-fibrant types and with an extra equality which is extensional in the sense of extensional type theory;
Part & Luo (2015) proposed a “Logic-enriched Homotopy Type Theory”, in particular, they formalized a construction of semi-simplicial types in this logic using the Plastic proof assistant;
Altenkirch, Capriotti & Kraus (2016) proposed a two-level type theory generalizing HTT, leading to 2LTT by Dannil Annenkov?, Paolo Capriotti, Nicolai Kraus and Christian Sattler, providing another construction of semi-simplicial types in an extended type theory;
According to Kraus (2018), semi-simplicial types can also be constructed in Angiuli-Harper-Wilson’s computational higher-dimensional type theory.
The “indexed” approach as families of families with iterated dependencies is only one possible approach! Other approaches to the problem are also possible, and may be better.
An alternative idea is 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”.
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 [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 go away; but then one has again only defined semi-simplicial h-sets, which are (presumably) strictly less general.
Another approach is to extend type theory with streams typed by streams of types as in a HoTTEST talk by Astra Kolomatskaia.
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 is a direct category, while the simplex category is not.
The original page about semi-simplicial types on the wiki of the Univalent Foundations year contained also material related to semi-simplicial sets in general though not to semi-simplicial types properly speaking. It is kept here for historical reasons.
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:
Vladimir Voevodsky, sketch of a definition (2012) [Coq code]
Hugo Herbelin, A dependently-typed construction of semi-simplicial types, Mathematical Structures in Computer Science, Vol 25 (special issue 05), 2015 [pdf] [Coq code]
Fedor Part?, Zhaohui Luo: Semi-simplicial Types in Logic-enriched Homotopy Type Theory [arXiv:1506.04998] (Submitted on 16 Jun 2015) [Plastic code]
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus: Extending Homotopy Type Theory with Strict Equality [arXiv:1604.03799] (Submitted on Apr 2016) [Agda code simulating semi-simplicial types in HoTT with strict equality]
Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler: Two-Level Type Theory and Applications [arXiv:1705.03307] (Submitted on May 2017)
Nicolai Kraus, Christian Sattler: Space-valued diagrams, type-theoretically (extended abstract) [arXiv:1704.04543] (Submitted on Apr 2017)
Nicolai Kraus: On the Role of Semisimplicial Types, 2018 [pdf]
Astra Kolomatskaia, Semi-Simplicial Types, Homotopy Type Theory Electronic Seminar Talks, 15 December 2022 (slides, video)
Last revised on June 26, 2023 at 16:20:43. See the history of this page for a list of all contributions to it.