On the relationship between QTT and STC [0094]

I have been thinking again about the relationship between quantitative type theory and synthetic Tait computability and other approaches to type refinements. One of the defining characteristics of QTT that I thought distinguished it from STC was the treatment of types: in QTT, types only depend on the “computational” / unrefined aspect of their context, whereas types in STC are allowed to depend on everything. In the past, I mistakenly believed that this was due to the realizability-style interpretation of QTT, in contrast with STC’s gluing interpretation. It is now clear to me that (1) QTT is actually glued (in the sense of q-realizability, no pun intended), and (2) the nonstandard interpretation of types in QTT corresponds to adding an additional axiom to STC, namely the tininess of the generic proposition.

It has been suggested to me by Neel Krishnaswami that this property of QTT may not be desirable in all cases (sometimes you want the types to depend on quantitative information), and that for this reason, graded type theories might be a better way forward in some applications. My results today show that STC is, in essence, what you get when you relax the QTT’s assumption that types do not depend on quantitative information. This suggests that we should explore the idea of multiplicities within the context of STC — as any monoidal product on the subuniverse spanned by closed-modal types induces quite directly a form of variable multiplicity in STC, I expect this direction to be fruitful.

My thoughts on the precise relationship between the QTT models and Artin gluing will be elucidated at a different time. Today, I will restrict myself to sketching an interpretation of a QTT-style language in STC assuming the generic proposition is internally tiny.

Let \(\mathscr {Q}\) be an elementary topos equipped with a subterminal object \(\P \hookrightarrow \mathbf {1}\) inducing an open subtopos \(\mathscr {E}\simeq {\mathscr {Q}}_{/\P }\hookrightarrow \mathscr {Q}\) and its complementary closed subtopos \(\mathscr {F}\hookrightarrow \mathscr {Q}\). This structure is the basis of the interpretation of STC; if you think of STC in terms of refinements, then stuff from \(\mathscr {E}\) is “computational” and stuff from \(\mathscr {F}\) is “logical”.

We now consider the interpretation of a language of (potentially quantitative) refinements into \(\mathscr {Q}\). A context \(\Gamma \) is interpreted by an object of \(\mathscr {Q}\); a type \(\Gamma \vdash A\) is interpreted by a family \(A\to \bigcirc {\Gamma }\); a term \(\Gamma \vdash a : A\) is interpreted as a map \(\Gamma \to A\) such that \(\Gamma \to A \to \bigcirc \Gamma \) is the unit of the monad.

So far we have not needed anything beyond the base structure of STC in order to give an interpretation of types in QTT’s style. But to extend this interpretation to a universe, we must additionally assume that \(\P \) is internally tiny, in the sense that the exponential functor \({\mathopen {}\left (-\right )\mathclose {}}^\P \) is a left adjoint. Under these circumstances, the idempotent monad \(\bigcirc \equiv j_*j^* : \mathscr {Q}\to \mathscr {Q}\) corresponding to the open immersion \(j : \mathscr {E}\hookrightarrow \mathscr {Q}\) has a right adjoint \(\square : \mathscr {Q}\to \mathscr {Q}\), an idempotent comonad.

Proof. 

As \(\bigcirc \equiv j_*j^*\) is the exponential functor \({\mathopen {}\left (-\right )\mathclose {}}^\P \), its right adjoint \(\square \) is therefore the “root functor” \({\mathopen {}\left (-\right )\mathclose {}}_\P \) that exhibits \(\P \) as an internally tiny object.

Although \(\square \) lifts to each slice of \(\mathscr {Q}\), these liftings do not commute with base change; this will, however, not be an obstacle for us.

We will now see how to use the adjunction \(\bigcirc \dashv \square \) to interpret a universe, either for the purpose of interpreting universes of refinement types, or for the purpose of strictifying the model that we have sketched. Let \(\mathcal {V}\) be a (standard) universe in \(\mathscr {Q}\), e.g. a Hofmann–Streicher universe; we shall then interpret the corresponding universe of refinements as \(\mathcal {U}:\equiv \square \mathcal {V}\). To see that \(\mathcal {U}\) classifies \(\mathcal {V}\)-small families of refinements, we compute as follows:

  1. A code \(\Gamma \vdash \hat {A} : \mathcal {U}\) amounts to nothing more than a morphism \(\hat {A}:\Gamma \to \square {\mathcal {V}}\).
  2. By adjoint transpose, this is the same as a morphism \(\hat {A}^\sharp : \bigcirc {\Gamma }\to \mathcal {V}\).

Thus we see that if \(\mathcal {V}\) is generic for \(\mathcal {V}\)-small families of (arbitrary) types in \(\mathscr {Q}\), then \(\mathcal {U} \equiv \square \mathcal {V}\) is generic for \(\mathcal {V}\)-small families of type refinements, i.e. types whose context is \(\bigcirc \)-modal.

Finally, we comment that the tininess of \(\P \) is satisfied in many standard examples, the simplest of which is the Sierpiński topos \(\mathbf {Set}^{\to }\).