nLab semi-simplicial types in homotopy type theory

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Homotopy 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

Contents

Idea

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 Δ i\Delta_i, 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 Δ i\Delta_i to a type universe UU 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”.

Semi-simplicial types as families of families of nn-semi-simplices

Small semi-simplicial types

To illustrate the idea of semi-simplicial types as families of families of nn-semi-simplices, let us consider the finite-dimensional parts of such semi-simplicial type:

Let UU be a type universe. Then,

  • A UU-small 0-semi-simplicial type is just a UU-small type X 0:UX_0:U.

  • A UU-small 1-semi-simplicial type is UU-small 0-semi-simplicial type X 0X_0 with a family of UU-small types

    x 0:X 0,x 1:X 0X 1(x 0,x 1):Ux_0:X_0, x_1:X_0 \vdash X_1(x_0, x_1):U
  • A UU-small 2-semi-simplicial type is a UU-small 1-semi-simplicial type (X 0,X 1)(X_0, X_1) with a family of UU-small types

    x:X 0,x 1:X 0,x 2:X 0,x 0,1:X 1(x 0,x 1),x 1,2:X 1(x 1,x 2),x 0,2:X 1(x 0,x 2)X 2(x 0,x 1,x 2,x 0,1,x 1,2,x 0,2):Ux:X_0, x_1:X_0, x_2:X_0, x_{0, 1}:X_1(x_0, x_1), x_{1, 2}:X_1(x_1, x_2), x_{0, 2}:X_1(x_0, x_2) \vdash X_2(x_0, x_1, x_2, x_{0, 1}, x_{1, 2}, x_{0, 2}):U

    representing triangular configurations from X 0X_0 and X 1X_1.

  • A UU-small 3-semi-simplicial type is a UU-small 2-semi-simplicial type (X 0,X 1,X 2)(X_0, X_1, X_2) with a family of UU-small types

    x:X 0,x 1:X 0,x 2:X 0,x 3:X 0, x 0,1:X 1(x 0,x 1),x 1,2:X 1(x 1,x 2),x 2,3:X 1(x 2,x 3), x 0,2:X 1(x 0,x 2),x 1,3:X 1(x 1,x 3),x 0,3:X 1(x 0,x 3), x 0,1,2:X 2(x 0,x 1,x 2,x 0,1,x 1,2,x 0,2),x 0,1,3:X 2(x 0,x 1,x 3,x 0,1,x 1,3,x 0,3), x 0,2,3:X 2(x 0,x 2,x 3,x 0,2,x 2,3,x 0,3),x 1,2,3:X 2(x 1,x 2,x 3,x 1,2,x 2,3,x 1,3), X 2(x 0,x 1,x 2,x 3,x 0,1,x 1,2,x 2,3,x 0,2,x 1,3,x 0,3,x 0,1,2,x 0,1,3,x 0,2,3,x 1,2,3):U\begin{array}{l} x:X_0, x_1:X_0, x_2:X_0, x_3:X_0, \\ x_{0, 1}:X_1(x_0, x_1), x_{1, 2}:X_1(x_1, x_2), x_{2, 3}:X_1(x_2, x_3), \\ x_{0, 2}:X_1(x_0, x_2), x_{1, 3}:X_1(x_1, x_3), x_{0, 3}:X_1(x_0, x_3), \\ x_{0, 1, 2}:X_2(x_0, x_1, x_2, x_{0, 1}, x_{1, 2}, x_{0, 2}), x_{0, 1, 3}:X_2(x_0, x_1, x_3, x_{0, 1}, x_{1, 3}, x_{0, 3}), \\ x_{0, 2, 3}:X_2(x_0, x_2, x_3, x_{0, 2}, x_{2, 3}, x_{0, 3}), x_{1, 2, 3}:X_2(x_1, x_2, x_3, x_{1, 2}, x_{2, 3}, x_{1, 3}), \\ \vdash X_2(x_0, x_1, x_2, x_3, x_{0, 1}, x_{1, 2}, x_{2, 3}, x_{0, 2}, x_{1, 3}, x_{0, 3}, x_{0, 1, 2}, x_{0, 1, 3}, x_{0, 2, 3}, x_{1, 2, 3}):U \end{array}

    representing tetrahedral configurations from X 0X_0, X 1X_1 and X 2X_2.

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 UU,

  • Can we define a function “Semi-simplicial:U\text{Semi-simplicial}:\mathbb{N} \to U”, such that for n=0,1,2,3n = 0,1,2,3, the UU-small type Semi-simplicial(n)\text{Semi-simplicial}(n) is (equivalent to) the objects explicitly defined here?

  • Can we define a type of UU-small semi-simplicial types (i.e. infinity-semi-simplicial types) with nn-simplices for all nn?

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 Δ i\Delta_i with face maps d id_i. 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:

Other approaches

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 Δ i\Delta{}_i? Giving a reasonable definition of Δ i\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 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.

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\Delta{}_i is a direct category, while the simplex category Δ\Delta is not.

About the original page on the wiki of the Univalent Foundations year

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:

  • 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.

See also

References

Last revised on June 26, 2023 at 16:20:43. See the history of this page for a list of all contributions to it.