Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 15, 2024

Semi-Simplicial Types, Part II: The Main Results

Posted by Mike Shulman

(Jointly written by Astra Kolomatskaia and Mike Shulman)

This is part two of a three part series of expository posts on our paper Displayed Type Theory and Semi-Simplicial Types. In this part, we cover the main results of the paper.

The Geometric Intuition

The central motivating definition of our paper is the following:

A semi-simplicial type XX consists of a type X 0X_0 together with, for every x:X 0x:X_0, a displayed semi-simplicial type over XX.

The purpose of the 100+ pages is to formulate a type theory in which we can make sense of this as a kind of “coinductive definition”. The key is to figure out what “displayed semi-simplicial type over XX should mean. Intuitively, it should be an “indexed” reformulation of a morphism of semi-simplicial types YXY \to X, but how do we do that?

The idea behind our new type theory, Displayed Type Theory (dTT), is that if X:TypeX : \mathsf{Type} is any notion of mathematical object (such as a group, category, or semi-simplicial type), then there should exist a notion of displayed elements of XX living over the elements of XX. Thus, for example, if 𝒞:Cat\mathcal{C} : \mathsf{Cat} is a category, then there should be a type Cat d𝒞\mathsf{Cat^d}\;\mathcal{C} of categories displayed over 𝒞\mathcal{C}, or alternatively dependent categories over 𝒞\mathcal{C}. The particular case of displayed categories was introduced by Ahrens and Lumsdaine in an eponymous 2019 paper, and the idea has since been generalized to bicategories by Ahrens, Frumin, Maggesi, Veltri, and van der Weide; dTT posits that such displayed structures exist for any kind of mathematical object, with a definition that can be derived algorithmically from the definition of the object.

We will return to this below; but first, as suggested above, we explain how such a notion enables a coinductive definition of semi-simplicial types. Indeed, we say that a semi-simplicial type AA consists of the following: First, AA defines a type ZA:Type\mathsf{Z}\;A : \mathsf{Type}, called the 00-simplices of AA. Second, each 00-simplex x:ZAx : \mathsf{Z}\;A defines a semi-simplicial type SAx:SST dA\mathsf{S}\;A\;x : \mathsf{SST^d}\;A displayed over AA, called the slice of AA over xx.

We can phrase this in Agda-esque syntax for dTT as follows:

codata SST : Type where
  Z : SST → Type
  S : (X : SST) → Z X → SSTᵈ X

To see why this definition is correct, we have to understand what, in general, a semi-simplicial type BB displayed over AA consists of. The first part of this answer is that BB defines a type of 00-simplices of BB displayed over 00-simplices of AA, i.e. a family Z dB:ZAType\mathsf{Z^d}\;B : \mathsf{Z}\;A \to \mathsf{Type}. Then, every displayed 00-simplex z:Z dByz : \mathsf{Z^d}\;B\;y over a 00-simplex y:ZAy : \mathsf{Z}\;A should define S dByz\mathsf{S^d}\;B\;y\;z, a doubly displayed semi-simplicial type, for whatever this means.

Now, instead of working out the definition of a doubly dependent semi-simplicial type, let’s circle back and think geometrically. Semi-simplicial types should have families of nn-simplex types. If A:SSTA : \mathsf{SST}, then we write that

A 0:Type A 0ZA \begin{aligned} &A_0 : \mathsf{Type} \\ &A_0 \equiv \mathsf{Z}\;A \end{aligned}

is the type of 00-simplices in AA. Similarly, if B:SST dAB : \mathsf{SST^d}\;A is semi-simplicial type displayed over AA, then for y:A 0y : A_0, we write

B 0:A 0Type B 0yZ dBy \begin{aligned} &B_0 : A_0 \to \mathsf{Type} \\ &B_0\;y \equiv \mathsf{Z^d}\;B\;y \end{aligned}

for the type of 00-simplices of BB displayed over the 00-simplex yy of AA. Putting this together, if we have two 00-simplices x 00x 10:A 0x_{00}\;x_{10} : A_0 of AA, then we may form

A 1:(x 01:A 0)(x 10:A 0)Type A 1x 01x 10Z d(SAx 01)x 10, \begin{aligned} &A_1 : (x_{01} : A_0)\;(x_{10} : A_0) \to \mathsf{Type} \\ &A_1\;x_{01}\;x_{10} \equiv \mathsf{Z^d}\;(\mathsf{S}\;A\;x_{01})\;x_{10}, \end{aligned}

which is the type of 11-simplices in AA joining x 01x_{01} to x 10x_{10}.

It therefore stands to reason that BB should have a type of dependent 11-simplices living over the 11-simplices of AA. Thus if β 11:A 1y 01y 10\beta_{11} : A_1\;y_{01}\;y_{10}, then given dependent endpoints z 01:B 0y 01z_{01} : B_0\;y_{01} and z 10:B 0y 10z_{10} : B_0\;y_{10}, we should get a type B 1y 01z 01y 10z 10β 11B_1\;y_{01}\;z_{01}\;y_{10}\;z_{10}\;\beta_{11}. The formula for this happens to take the following form:

B 1:(y 01:A 0)(z 01:B 0y 01)(y 10:A 0)(z 10:B 0y 10)(β 11:A 1y 00y 10)Type B 1y 01z 01y 10z 10β 11Z dd(S dBy 01z 01)y 10z 10β 11, \begin{aligned} &B_1 : (y_{01} : A_0)\;(z_{01} : B_0\;y_{01})\;(y_{10} : A_0)\;(z_{10} : B_0\;y_{10})\;(\beta_{11} : A_1\;y_{00}\;y_{10}) \to \mathsf{Type} \\ &B_1\;y_{01}\;z_{01}\;y_{10}\;z_{10}\;\beta_{11} \equiv \mathsf{Z^{dd}}\;(\mathsf{S^d}\;B\;y_{01}\;z_{01})\;y_{10}\;z_{10}\;\beta_{11}, \end{aligned}

which mirrors the formula for A 1A_1.

Then, putting all of this together again, if we have a 00-simplex x 001:A 0x_{001} : A_0, then we take BSAx 001B \equiv \mathsf{S}\;A\;x_{001}. For x 010:A 0x_{010} : A_0, we have that B 0x 010Z d(SAx 001)x 010A 1x 001x 010B_0\;x_{010} \equiv \mathsf{Z^d}\;(\mathsf{S}\;A\;x_{001})\;x_{010} \equiv A_1\;x_{001}\;x_{010}. We thus get that:

A 2:(x 001:A 0)(x 010:A 0)(β 011:A 1x 001x 010)(x 100:A 0) (β 101:A 1x 001x 100)(β 110:A 1x 010x 100)Type A 2x 001x 010β 011x 100β 101β 110Z dd(S d(SAx 001)x 010β 011)x 100β 101β 110 \begin{aligned} &A_2 :(x_{001} : A_0)\;(x_{010} : A_0)\;(\beta_{011} : A_1\;x_{001}\;x_{010})\;(x_{100} : A_0) \\ &\quad\quad(\beta_{101} : A_1\;x_{001}\;x_{100})\;(\beta_{110} : A_1\;x_{010}\;x_{100}) \to \mathsf{Type} \\ &A_2\;x_{001}\;x_{010}\;\beta_{011}\;x_{100}\;\beta_{101}\;\beta_{110} \equiv \mathsf{Z^{dd}}\;(\mathsf{S^d}\;(\mathsf{S}\;A\;x_{001})\;x_{010}\;\beta_{011})\;x_{100}\;\beta_{101}\;\beta_{110} \end{aligned}

In general, this pattern continues in higher dimensions and the process described lets us extract nn-simplex types.

We can visualise what’s going on in two different ways. The first visualisation shows how the nn-simplices of the slice of AA over xx live dependently over simplices of AA.


For example, if z 1z_1 is a 00-simplex of the slice of AA over xx displayed over the zero simplex y 1y_1 of AA, then z 1z_1 is a 11-simplex of AA joining xx to y 1y_1. Similarly, suppose z 01z_{01} and z 10z_{10} are 00-simplices of the slice of AA over xx displayed over y 01y_{01} and y 10y_{10}, respectively, and β 11\beta_{11} is a 11-simplex of AA joining y 01y_{01} to y 11y_{11}. Then if γ 11\gamma_{11} is a 11-simplex of the slice of AA over xx displayed over β 11\beta_{11} and joining z 01z_{01} to z 10z_{10}, then γ 11\gamma_{11} is a 22-simplex of AA with the specified boundary.

Geometrically, we are using the fact that the nn-simplex is the cone of the (n1)(n-1)-simplex. Thus, with the above definition, assuming we know inductively that every semi-simplicial type has a type of (n1)(n-1)-simplices, then for every 0-simplex xx, the displayed semi-simplicial type SAx\mathsf{S}\; A \; x has a type of “displayed (n1)(n-1)-simplices” over this. Such a displayed (n1)(n-1)-simplex depends in xx (the cone vertex) as well as on an (n1)(n-1)-simplex of AA (the base face, opposite the cone vertex) and thus can be viewed geometrically as an nn-simplex.

The second visualisation explains our formulas in terms of iterated slicing.


Note that, to form each successive slice, you have to provide 2 n2^n simplex data points. The true dependent nn-simplices of a slice may then be viewed as matching objects.

The Homotopical Problem of Constructing a Semi-Simplicial Classifier

Now, to motivate the construction of “display”, let us return to classical homotopy theory. Suppose that we are working in 𝒞\mathcal{C}, some setting for homotopy theory. This could be a model category or a fibration category, which we usually think of as representing a Grothendick \infty-topos. In our paper (section 4.1) we refer to the objects of 𝒞\mathcal{C} as contexts, denoted Γctx\Gamma\;\mathsf{ctx}, the fibrations over a context Γ\Gamma as types, denoted γ:ΓAγtype\gamma : \Gamma \vdash A\;\gamma\;\mathsf{type}, and sections of a type AA as terms, denoted by γ:Γtγ:Aγ\gamma : \Gamma \vdash t\;\gamma : A\;\gamma.

We assume that this setting has an object classifier. This means that in any context Γ\Gamma, there is γ:ΓTypeγtype\gamma : \Gamma \vdash \mathsf{Type}\;\gamma \;\mathsf{type}, as well as γ:Γ,A:TypeγElAγtype\gamma : \Gamma, \;A : \mathsf{Type}\;\gamma \vdash \mathsf{El}\;A\;\gamma\;\mathsf{type}. This has the property that any “small” fibration γ:ΓAγtype\gamma : \Gamma \vdash A\;\gamma\;\mathsf{type} gives rise to a code in the universe γ:ΓCodeAγ:Typeγ\gamma : \Gamma \vdash \mathsf{Code}\;A\;\gamma : \mathsf{Type}\;\gamma, such that the pullback of the El\mathsf{El} fibration along that section exactly yields the type AA, that is: γ:ΓEl(CodeA)γAγ.\gamma : \Gamma \vdash \mathsf{El}\;(\mathsf{Code}\;A)\;\gamma \equiv A\;\gamma.

We then consider the problem of constructing a classifier for semi-simplicial diagrams. Specifically, we are interested in Reedy fibrant semi-simplicial diagrams, which are the homotopical counterpart of the indexed formulation in syntax. Thus, such a classifier would consist of a generic fibration in the empty context SSTtype\cdot \vdash \mathsf{SST}\;\mathsf{type}, along with a simplicial diagram tower of the form:

A:SSTEl 0Atype A:SST,a 01:El 0A,a 10:El 0AEl 1Aa 0a 1type A:SST,a 001:El 0A,a 010:El 0A,a 011:El 1Aa 001a 010 a 100:El 0A,a 101:El 1Aa 100a 100,a 110:El 1Aa 100a 010 El 2Aa 001a 010a 011a 100a 101a 110type \begin{aligned} & A : \mathsf{SST} \vdash \mathsf{El}_0\;A\;\mathsf{type} \\\\ & A : \mathsf{SST},\; a_{01} : \mathsf{El}_0\;A,\; a_{10} : \mathsf{El}_0\;A\vdash \mathsf{El}_1\;A\;a_0\;a_1\;\mathsf{type} \\\\ & A : \mathsf{SST},\; a_{001} : \mathsf{El}_0\;A,\; a_{010} : \mathsf{El}_0\;A,\; a_{011} : \mathsf{El}_1\;A\;a_{001}\;a_{010} \\\\ &\quad\quad a_{100} : \mathsf{El}_0\;A,\; a_{101} : \mathsf{El}_1\;A\;a_{100}\;a_{100},\; a_{110} : \mathsf{El}_1\;A\;a_{100}\;a_{010} \\\\ &\quad\quad \vdash \mathsf{El}_2\;A\;a_{001}\;a_{010}\;a_{011} \;a_{100}\;a_{101}\;a_{110}\;\mathsf{type} \\ &\ldots \end{aligned}

such that for any “small” simplicial diagram data over a context Γ\Gamma, this data arises uniquely as the appropriate series of pullbacks constructed from some term γ:ΓAγ:SST\gamma : \Gamma \vdash A\;\gamma : \mathsf{SST}.

Note that, stated in this way, this is an infinitary or non-elementary universal property: it refers to infinite diagrams indexed by the external set of natural numbers (as opposed to any internal natural-numbers object that may exist in 𝒞\mathcal{C}). The problem of defining semi-simplicial types can roughly be thought of as one of giving a finitary universal property for such an object, so that it could be characterized and even constructed in a finitary syntactic type theory.

A Finitary Universal Property for the Classifier

We have not, strictly speaking, solved this problem as originally stated. Indeed, we suspect that the classifier SST\mathsf{SST} does not, on its own, have a finitary universal characterisation. However, we discovered that there is an enhancement of it that does have a finitary universal property, if we change the setting 𝒞\mathcal{C} in which we were working to the augmented semi-simplicial diagram model 𝒞 Δ + op\mathcal{C}^{\Delta^{\mathrm{op}}_+}. Then, there is a universally characterised diagram SST\mathsf{SST} in 𝒞 Δ + op\mathcal{C}^{\Delta^{\mathrm{op}}_+}, of which the desired classifier in 𝒞\mathcal{C} was the discrete part, denoted SST\lozenge\;\mathsf{SST}.

If we playfully refer to the problem of categorically constructing a classifier for semi-simplicial objects as answering the question “what is a triangle?”. then we discovered that SST\mathsf{SST} is naturally characterised in the model 𝒞 Δ + op\mathcal{C}^{\Delta^{\mathrm{op}}_+}, which is the setting for homotopy theory in which “everything is an augmented triangle.” In a sense, then, SST\mathsf{SST} is the “augmented triangle of triangles.”

Intuitively, by working in the setting of infinitely coherent diagrams, the desired augmented diagram of diagrams can be assembled in a way that accounts for all the coherences. This at first may appear as a convenient but inessential strengthening of the inductive hypothesis. However, passing to the world of augmented diagrams seems to play a much more essential role than this because the finitary universal characterisation of SST\mathsf{SST} uses properties of augmented diagrams in an essential way.

Specifically, the world of augmented diagrams is the place where we can make sense of the general notion of a “displayed element” of a type. This happens through the existence of an operation known as décalage, which is a kind of backwards shift operation. It’s very classical in homotopy theory — you can read much more about it starting on the nLab — but the basic idea is just that if you take a (fibred) semi-simplicial diagram XX and throw away the bottom object and the last face operators in each dimension, and relabel, you get another semi-simplicial diagram. In other words, on objects we have (X D) n=X n+1(X^{\mathsf{D}})_{n} = X_{n+1}. The face operators that we threw away now assemble into a map of semi-simplicial diagrams ρ X:X DX\rho_X : X^{\mathsf{D}} \to X.

If we convert this fibred formulation to an indexed one, this means that any object XX comes with an object X dX^d over itself, such that X D x:XX dxX^{\mathsf{D}} \cong \sum_{x:X} X^d\, x. In practice, we keep the fibred formulation for contexts, but use the indexed version for types, and call it display. This gives the following rule:

γ:ΓAγtypeγ +:Γ D,a:A(ρ Γγ +)A dγ +atype\frac{\gamma : \Gamma \vdash A\;\gamma\;\mathsf{type}}{\gamma^+ : \Gamma^\mathsf{D},\; a : A\;(\rho_\Gamma\;\gamma^+) \vdash A^\mathsf{d}\; \gamma^+\;a\;\mathsf{type}}

The fact that display alters the context is the source of much technical difficulty, which we deal with in the paper using a modal type theory. We have two modes, the simplicial one corresponding to 𝒞 Δ + op\mathcal{C}^{\Delta^{\mathrm{op}}_+}, and the discrete one corresponding to 𝒞\mathcal{C} itself. Then we have three basic modalities. The first, denoted \lozenge, picks out the (1)(-1)-simplices of an augmented semi-simplicial diagram, mapping the simplicial mode to the discrete mode. The second, denoted \triangle, builds a constant augmented semi-simplicial diagram, mapping the discrete mode to the simplicial mode. And the third, denoted \Box, takes the limit of a semi-simplicial diagram, mapping the simplicial mode to the discrete mode. Then décalage and display act only on types at the simplicial mode, but we can avoid décalaging the context if it comes from the discrete mode, giving a rule something like:

γ:ΓAγtypeγ:Γ,a:AγA dγatype\frac{\gamma : \triangle \Gamma \vdash A\;\gamma\;\mathsf{type}}{\gamma : \triangle\Gamma,\; a : A\;\gamma \vdash A^\mathsf{d}\; \gamma\;a\;\mathsf{type}}

To be more precise, here Γ\triangle\Gamma refers to a “modal context lock”, and we actually allow part of the context to be simplicial and get décalaged. However, for the present we can ignore these modal issues and just work in the empty context ()(\,), for which we have () D()(\,)^\mathsf{D} \equiv (\,). Ignoring this and other subtleties involving telescopes, we can now state more formally the universal property of SST\mathsf{SST}. Suppose that YY is a type in the empty context (at the simplicial mode), a.k.a. a “closed type”. We define an endofunctor on closed types (at the simplicial mode) by:

F(Y) υ:Y A:Type(AY dυ).\mathsf{F}(Y) \equiv \sum_{\upsilon : Y} \sum_{A : \mathsf{Type}} ( A \to Y^\mathsf{d}\;\upsilon).

This endofunctor comes with an evident copointing ϵ Y:F(Y)Y\epsilon_Y : \mathsf{F}(Y) \to Y by way of projection. Our proposed characterization of SST\mathsf{SST} is that it is a terminal (copointed) coalgebra of the copointed endofunctor (F,ϵ)(\mathsf{F},\,\epsilon). Thus, it is the universal object equipped with a map

SST X:SST A:Type(ASST dX)\mathsf{SST} \to \sum_{X : \mathsf{SST}} \sum_{A : \mathsf{Type}} ( A \to \mathsf{SST}^\mathsf{d}\;X)

whose first component is the identity. What remains, therefore, is two components Z:SSTType\mathsf{Z}: \mathsf{SST} \to \mathsf{Type} and S:(X:SST)ZXSST dX\mathsf{S} : (X : \mathsf{SST}) \to \mathsf{Z}\;X \to \mathsf{SST}^{\mathsf{d}}\;X, exactly as proposed above. Once again, this corresponds to the following Agda-esque dTT code:

codata SST : Type where
  Z : SST → Type
  S : (X : SST) → Z X → SSTᵈ X


The model structure on 𝒞 Δ + op\mathcal{C}^{\Delta^{\mathrm{op}}_+} is well known in the literature as the Reedy model structure. However, in the dTT paper, we present an explicit construction in the case of the augmented semi-simplex category. This presentation defines the relevant concepts mutually with décalage and display, and allows for definitionally strict commutation laws for display without the use of coherence theorems. These computation laws, for example, say that:

Type dAAType\mathsf{Type}^\mathsf{d}\;A \equiv A \to \mathsf{Type}

((a:A)B[a])df(a:A ρ)(a:A da)B d[a,a](fa)((a : A) \to B\;[\,a\,]){^\mathsf{d}}\;f \equiv (a : A^\rho)\,(a' : A^\mathsf{d}\;a) \to B^\mathsf{d}\;[\,a\,,\,a'\,]\;(f\;a)

These laws provide the promised algorithmic computation of displayed structures in terms of ordinary ones. If X denotes a kind of mathematical structure, the first law above says that for any type appearing in an X, a displayed X has a type dependent on that type, and the second says that similarly any function appearing in an X is tracked in a displayed X by a function lying above it. Thus, for instance, if CC is a category with object set C 0C_0 and homs hom C:C 0C 0Type\hom_C : C_0 \to C_0 \to \mathsf{Type}, a displayed category has a dependent family of objects D 0:C 0TypeD_0 : C_0 \to \mathsf{Type} and dependent hom-types lying over those of CC, with composition and identity operations lying over those of CC and so on, exactly as in the original definition of displayed category.

However, these are also the classical observational computation laws for “unary parametricity”! These say that in a unary relational model, computability witnesses for a type are predicates on the type, and computability witnesses for a function ff are constructions that transform computability witnesses of an input aa into computability witnesses of the corresponding output (fa)(f\;a). This basic structure is what underlies, for example, the normalisation proof for STLC in Pierce’s Types and Programming Languages.

Consider the type of polymorphic identity functions. We have that:

((A:Type)AA)did(A:Type)(P:AType)(a:A)PaP(ida)((A : \mathsf{Type}) \to A \to A){^\mathsf{d}}\;\mathsf{id} \equiv (A : \mathsf{Type})\,(P : A \to \mathsf{Type})\,(a : A) \to P\;a \to P\;(\mathsf{id}\;a)

Hence a computability witness of a polymorphic identity function id\mathsf{id} is a proof that id\mathsf{id} preserves arbitrary predicates. In displayed type theory, then, we have (with some abuse of notation for the modalities that we are ignoring):

id-thm : (f : △□ ((A : Type) → A → A)) (A : Type) (a : A) → f A a ≡ a
id-thm (△ (□ f)) A a = fᵈ A (λ x → x ≡ a) a refl

Thus any closed term of polymorphic identity function type is indeed an identity function at all types.

Parametricity means that, for example, the simplicial mode of dTT is incompatible with the existence of features such as universal decidable equality. Indeed, suppose that we had decidable equality on the universe. Then one could construct a bad polymorphic identity function which is everywhere the identity function, except at the type Nat\mathsf{Nat}, at which it is the constant at 22 function. Such a construction would violate the theorem above. Indeed, the spirit of most parametricity violating results is either classical or non-constructive. This is because, morally, if you do everything constructively, then any definition that you write down should be natural and respect all relations.

Using the Universal Property

Note that our definition/construction of SST\mathsf{SST} yields a type at the simplicial mode, i.e. an object of 𝒞 Δ + op\mathcal{C}^{\Delta^{\mathrm{op}}_+}. But the classical homotopy theorist is interested in our original homotopy theory 𝒞\mathcal{C}. Thus, recalling that \lozenge picks out the (1)(-1)-simplices of an augmented semi-simplicial diagram, from the classical perspective the question of interest in working with semi-simplicial types is:

Given a context Γ\Gamma in the model being studied (i.e. the discrete mode), construct a term γ:ΓAγ:SST\gamma : \Gamma \vdash A\;\gamma : \lozenge\;\mathsf{SST} representing the desired semi-simplicial type.

But in order to solve this problem, we have to work in the simplicial mode, where the universal property is stated. This means that we have to find a context Γ˜\widetilde{\Gamma} at the simplicial mode such that Γ˜Γ\lozenge\;\widetilde{\Gamma} \equiv \Gamma, i.e. to extend Γ\Gamma to a diagram of which it is the discrete part. Doing so is always possible as we may consider Γ\triangle\;\Gamma, which extends Γ\Gamma coskeletally. However, the issue is that any categorical universal properties that held of Γ\Gamma in the discrete mode will not necessarily continue to hold of Γ\triangle\;\Gamma as a diagram; in particularly, any properties of Γ\Gamma that are expressed in the syntax of type theory vanish. It is thus necessary to extend Γ\Gamma to a diagram in a bespoke way such that the relevant properties that discretely hold of Γ\Gamma continue to simplicially hold of Γ˜\widetilde{\Gamma}.

Fortunately, every construction of constructive intensional type theory (e.g. Π\Pi-types, universes, and inductive types) make sense of diagrams. Thus, metatheoretically, one can construct Γ˜\widetilde{\Gamma} of a purely syntactic entity by structural recursion on the definition of Γ\Gamma via replacing all discrete syntax with its simplicial counterpart. However, from the perspective of the homotopy theorist, the model category can have many semantic entities not captured by the syntax of type theory. For example, the semantics of dTT are compatible with the model for the discrete mode having universal decidable equality. If Γ\Gamma were to use such a parametricity violating construction in an essential way in its definition, then the obstacle would be that Γ\Gamma could not be lifted to Γ˜\widetilde{\Gamma} in a way that reflected all of the same categorical properties.

Parametricity thus serves as a kind of filter regarding what categorical universal properties of Γ\Gamma can be invoked when applying the universal property of semi-simplicial types. The categorical meaning of parametricity is then the question of what universal constructions in an arbitrary model category 𝒞\mathcal{C} exist in the diagram model 𝒞 Δ + op\mathcal{C}^{\Delta^{\mathrm{op}}_+}.

Simplices, cubes, and symmetry

It is a curious fact that to give a universal property to the type SST\mathsf{SST} of semi-simplicial types, we find ourselves needing to work in the model 𝒞 Δ + op\mathcal{C}^{\Delta^{\mathrm{op}}_+} whose objects are augmented semi-simplicial types in 𝒞\mathcal{C} — curious that the two are closely related and yet not identical. It’s possible there is something deeper going on here, but one explanation is that this is a coincidence arising from another coincidence: the fact that the augmented semi-simplex category coincides with the unary semi-cube category.

Normally when we think of a cubical set we think of cubes as powers of an interval object that has two endpoints. Thus, an nn-dimensional cube has 2n2n faces of dimension (n1)(n-1), arising by choosing one of the nn dimensions and then an endpoint in that dimension. However, essentially the same formal construction works for an “interval” having kk endpoints for any natural number kk. We can visualize the case k=3k=3, for instance, as consisting of powers of an interval with its midpoint also distinguished along with its endpoints, so that a 2-cube looks like a window subdivided into four panes.

In the case k=1k=1, it turns out that the faces of a “unary” nn-cube have exactly the same combinatorial structure as those of an augmented (n1)(n-1)-simplex. We can even see this geometrically: the unary cubes can be thought of as powers of a half-open interval [0,1)[0,1) or ray [0,)[0,\infty) with only one endpoint, and there is a face-respecting embedding of the (n1)(n-1)-simplex in the first nn-orthant [0,) n[0,\infty)^n as {(x 1,,x n)x 1++x n=1}\{ (x_1,\dots,x_n) \mid x_1+\cdots+x_n = 1\}. Thus, we can equivalently think of dTT as having semantics in the model of unary semi-cubical diagrams.

This point of view is also suggested by the connection to parametricity, where one can consider also kk-ary parametricity for any kk. Indeed, binary parametricity seems to be more useful than unary parametricity: many of the “free theorems” arising from parametricity require the binary version. (Nullary parametricity is also possible, and is closely related to nominal sets.) Ordinary internal kk-ary parametricity has semantics in kk-ary cubical diagrams (having degeneracies as well as faces), and one might expect that there is an analogous sort of kk-ary dTT” with semantics in kk-ary semi-cubical diagrams.

For those having experience with cubical type theories, we should emphasize that unlike the cubes often used there, these cubes do not have diagonals or connections. This is essential to get the correct behavior of Π\Pi-types, for instance. (However, cubes without diagonals and connections were used in the first BCH cubical model of homotopy type theory, and also in the more recent Higher Observational Type Theory.)

Another question this perspective emphasizes is the presence or absence of symmetries. Here the simplest sort of symmetry in dTT would be an isomorphism A ddxy 0y 1A ddxy 1y 0A^{\mathsf{dd}}\,x\,y_0\,y_1 \cong A^{\mathsf{dd}}\,x\,y_1\,y_0. Our current theory does not admit such operations, in contrast to internal parametricity and cubical type theories where they have been found essential. The modal guards on the display operation allow us to omit them. This makes certain things easier, such as our explicit construction of the diagram model 𝒞 Δ + op\mathcal{C}^{\Delta^{\mathrm{op}}_+}, but may ultimately be a limitation: in particular, it seems that we cannot give a useful universal property to SST d\mathsf{SST}^{\mathsf{d}} without symmetries.

Conclusion and Vistas

In conclusion, therefore, what we achieve is to specify a new type theory, displayed type theory (dTT), which contains a unary parametricity operator () d(-)^\mathsf{d} that behaves “observationally” (computes on type-formers), and which is “modally guarded” so that it can only be applied to types in the empty context or more generally in a modal context. Inside this type theory, we specify a general notion of “displayed coinductive type”, of which our proposed definition of SST\mathsf{SST} is an instance.

We then construct, from any model of type theory having limits of countable towers of fibrations, a model of dTT, and show that in this model displayed coinductive types are modeled by terminal coalgebras of copointed endofunctors, which can be constructed as countable inverse limits. Moreover, we identify the corresponding tower for SST\mathsf{SST} as consisting of the classifiers for nn-truncated semi-simplicial types, so that the limit object SST\mathsf{SST} is, indeed, a classifier of semi-simplicial types.

Intriguingly, this leaves open the question of models of dTT and SST\mathsf{SST} without countable limits. We conjecture that there are models of dTT, perhaps obtained from realizability, in which an object satisfying our universal property for SST\mathsf{SST} exists, but is not an external classifier of semi-simplicial types. Instead, we expect it should be a classifier of “internal” or “uniform” semi-simplicial types, which is exactly what one would hope to be able to talk about in a realizability model. If this were true, then our universal property for semi-simplicial types would be more general than the classical external infinitary one, with possible implications for the notion of “elementary (,1)(\infty,1)-topos”.

Posted at April 15, 2024 2:41 AM UTC

TrackBack URL for this Entry:

2 Comments & 0 Trackbacks

Re: Semi-Simplicial Types, Part II: The Main Results

Nice reading! Can I ask to elaborate on the connection between nullary parametricity and nominal sets?

Posted by: Matteo Capucci on April 24, 2024 3:39 PM | Permalink | Reply to this

Re: Semi-Simplicial Types, Part II: The Main Results

Sure! Nominal sets are the objects of the Schanuel topos, which is the category of sheaves for a Grothendieck topology on FinSet mono opFinSet_{mono}^{op}. Whereas, the natural semantics of nullary parametricity is in the category of presheaves on FinSet monoFinSet_{mono}. Specifically, the “nullary cube category”, which has degeneracies but no faces, is equivalent to FinSet monoFinSet_{mono}.

The syntax of internal nullary parametricity is also similar to that of nominal type theory. There is a “nullary bridge type” that we can think of as classifying terms of a given type that depend on an extra free variable: thus terms of type AA are closed, terms of type BrABr A depend on one free variable, terms of type Br(BrA)Br (Br A) depend on two free variables, and so on. There are degeneracy operations like ABrAA \to Br A that intuitively weaken a term to depend trivially on more variables, and symmetry automorphisms like Br(BrA)Br(BrA)Br (Br A) \cong Br (Br A) that intuitively permute the variables.

I am not entirely clear on the reason people generally pass to a sheaf subtopos of nullary cubical sets. It may be partly historical, as early papers on nominal sets used the Fraenkel-Mostowski model of ZFC instead, which is more closely related to the sheaves than the presheaves (by way of the equivalence between the sheaf topos and the topos of continuous actions of Aut()Aut(\mathbb{N})). It may also involve wanting to remain consistent with classical logic. If so, another way to do that would be to use nullary displayed type theory instead, which would have natural semantics in presheaves on FinSet iso opFinSet_{iso}^{op}, i.e. the category of species. But I don’t know whether nullary displayed type theory would suffice for what people do with nominal type theory.

Posted by: Mike Shulman on April 24, 2024 3:59 PM | Permalink | Reply to this

Post a New Comment