The n-Category Café

The Geometric Intuition

The central motivating definition of our paper is the following:

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

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 $X$” should mean. Intuitively, it should be an “indexed” reformulation of a morphism of semi-simplicial types $Y \to X$, but how do we do that?

The idea behind our new type theory, Displayed Type Theory (dTT), is that if $X : \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 $X$ living over the elements of $X$. Thus, for example, if $\mathcal{C} : \mathsf{Cat}$ is a category, then there should be a type $\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 $A$ consists of the following: First, $A$ defines a type $\mathsf{Z}\;A : \mathsf{Type}$, called the $0$-simplices of $A$. Second, each $0$-simplex $x : \mathsf{Z}\;A$ defines a semi-simplicial type $\mathsf{S}\;A\;x : \mathsf{SST^d}\;A$ displayed over $A$, called the slice of $A$ over $x$.

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 $B$ displayed over $A$ consists of. The first part of this answer is that $B$ defines a type of $0$-simplices of $B$ displayed over $0$-simplices of $A$, i.e. a family $\mathsf{Z^d}\;B : \mathsf{Z}\;A \to \mathsf{Type}$. Then, every displayed $0$-simplex $z : \mathsf{Z^d}\;B\;y$ over a $0$-simplex $y : \mathsf{Z}\;A$ should define $\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 $n$-simplex types. If $A : \mathsf{SST}$, then we write that

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

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

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

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

$$\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 $1$-simplices in $A$ joining $x_{01}$ to $x_{10}$.

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

$$\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_1$.

Then, putting all of this together again, if we have a $0$-simplex $x_{001} : A_0$, then we take $B \equiv \mathsf{S}\;A\;x_{001}$. For $x_{010} : A_0$, we have that $B_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:

$$\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 $n$-simplex types.

We can visualise what’s going on in two different ways. The first visualisation shows how the $n$-simplices of the slice of $A$ over $x$ live dependently over simplices of $A$.

For example, if $z_1$ is a $0$-simplex of the slice of $A$ over $x$ displayed over the zero simplex $y_1$ of $A$, then $z_1$ is a $1$-simplex of $A$ joining $x$ to $y_1$. Similarly, suppose $z_{01}$ and $z_{10}$ are $0$-simplices of the slice of $A$ over $x$ displayed over $y_{01}$ and $y_{10}$, respectively, and $\beta_{11}$ is a $1$-simplex of $A$ joining $y_{01}$ to $y_{11}$. Then if $\gamma_{11}$ is a $1$-simplex of the slice of $A$ over $x$ displayed over $\beta_{11}$ and joining $z_{01}$ to $z_{10}$, then $\gamma_{11}$ is a $2$-simplex of $A$ with the specified boundary.

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

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

Note that, to form each successive slice, you have to provide $2^n$ simplex data points. The true dependent $n$-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 $\Gamma\;\mathsf{ctx}$, the fibrations over a context $\Gamma$ as types, denoted $\gamma : \Gamma \vdash A\;\gamma\;\mathsf{type}$, and sections of a type $A$ as terms, denoted by $\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 $\gamma : \Gamma \vdash \mathsf{Type}\;\gamma \;\mathsf{type}$, as well as $\gamma : \Gamma, \;A : \mathsf{Type}\;\gamma \vdash \mathsf{El}\;A\;\gamma\;\mathsf{type}$. This has the property that any “small” fibration $\gamma : \Gamma \vdash A\;\gamma\;\mathsf{type}$ gives rise to a code in the universe $\gamma : \Gamma \vdash \mathsf{Code}\;A\;\gamma : \mathsf{Type}\;\gamma$, such that the pullback of the $\mathsf{El}$ fibration along that section exactly yields the type $A$, that is: $$\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 $\cdot \vdash \mathsf{SST}\;\mathsf{type}$, along with a simplicial diagram tower of the form:

$$\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 $\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 $\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 $\mathcal{C}^{\Delta^{\mathrm{op}}_+}$. Then, there is a universally characterised diagram $\mathsf{SST}$ in $\mathcal{C}^{\Delta^{\mathrm{op}}_+}$, of which the desired classifier in $\mathcal{C}$ was the discrete part, denoted $\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 $\mathsf{SST}$ is naturally characterised in the model $\mathcal{C}^{\Delta^{\mathrm{op}}_+}$, which is the setting for homotopy theory in which “everything is an augmented triangle.” In a sense, then, $\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 $\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 $X$ 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^{\mathsf{D}})_{n} = X_{n+1}$. The face operators that we threw away now assemble into a map of semi-simplicial diagrams $\rho_X : X^{\mathsf{D}} \to X$.

If we convert this fibred formulation to an indexed one, this means that any object $X$ comes with an object $X^d$ over itself, such that $X^{\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:

$$\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 $\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)$-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:

$$\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 $(\,)^\mathsf{D} \equiv (\,)$. Ignoring this and other subtleties involving telescopes, we can now state more formally the universal property of $\mathsf{SST}$. Suppose that $Y$ 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:

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

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

$$\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 $\mathsf{Z}: \mathsf{SST} \to \mathsf{Type}$ and $\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

Parametricity

The model structure on $\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:

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

$$((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 $C$ is a category with object set $C_0$ and homs $\hom_C : C_0 \to C_0 \to \mathsf{Type}$, a displayed category has a dependent family of objects $D_0 : C_0 \to \mathsf{Type}$ and dependent hom-types lying over those of $C$, with composition and identity operations lying over those of $C$ 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 $f$ are constructions that transform computability witnesses of an input $a$ into computability witnesses of the corresponding output $(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 : \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 $\mathsf{id}$ is a proof that $\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 $\mathsf{Nat}$, at which it is the constant at $2$ 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 $\mathsf{SST}$ yields a type at the simplicial mode, i.e. an object of $\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)$-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 $\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 $\mathcal{C}^{\Delta^{\mathrm{op}}_+}$.

Simplices, cubes, and symmetry

It is a curious fact that to give a universal property to the type $\mathsf{SST}$ of semi-simplicial types, we find ourselves needing to work in the model $\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 $n$-dimensional cube has $2n$ faces of dimension $(n-1)$, arising by choosing one of the $n$ dimensions and then an endpoint in that dimension. However, essentially the same formal construction works for an “interval” having $k$ endpoints for any natural number $k$. We can visualize the case $k=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=1$, it turns out that the faces of a “unary” $n$-cube have exactly the same combinatorial structure as those of an augmented $(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)$ or ray $[0,\infty)$ with only one endpoint, and there is a face-respecting embedding of the $(n-1)$-simplex in the first $n$-orthant $[0,\infty)^n$ as $\{ (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 $k$-ary parametricity for any $k$. 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 $k$-ary parametricity has semantics in $k$-ary cubical diagrams (having degeneracies as well as faces), and one might expect that there is an analogous sort of “$k$-ary dTT” with semantics in $k$-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^{\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 $\mathcal{C}^{\Delta^{\mathrm{op}}_+}$, but may ultimately be a limitation: in particular, it seems that we cannot give a useful universal property to $\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 $(-)^\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 $\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 $\mathsf{SST}$ as consisting of the classifiers for $n$-truncated semi-simplicial types, so that the limit object $\mathsf{SST}$ is, indeed, a classifier of semi-simplicial types.

Intriguingly, this leaves open the question of models of dTT and $\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 $\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 $(\infty,1)$-topos”.