4
$\begingroup$

It's often said that homotopy type theory should be interpretable in any $\infty$-topos. But really it should be interpretable in any "predicative $\infty$-topos". I'm not quite sure what this means, but the prime example to me of an $\infty$-category which is "almost, but not quite, an $\infty$-topos" is the unstable motivic category $H(S)$ over a base scheme $S$.

The category $H(S)$ is locally cartesian closed, and locally presentable so that it presumably has any kind of higher inductive type one could want. I think it doees not have a subobject classifier, but probably that just means that it won't admit propositional resizing.

The failure of $H(S)$ to be an $\infty$-topos can be seen in the fact that $\Omega B$ is not the identity on grouplike $A_\infty$ objects, where $B$ is the bar construction; in particular, colimits indexed by $\Delta^{op}$ are not van Kampen. I'm not sure what to make of this type-theoretically, since it's not clear how to even define what a simplicial object is, let along an $A_\infty$ object. Should one expect that, given a definition of $A_\infty$ object in HoTT, it will be the case that every grouplike $A_\infty$ space is a loopspace, as is the case in any $\infty$-topos? Or would that be a statement analogous to Whitehead's theorem, not expected to hold in all models?

If we assume arbitrarily large Grothendieck universes, then I would have to think that $H(S)$ will admit type-theoretic universes. But perhaps they won't be univalent?

$\endgroup$
  • $\begingroup$ Why would you "have to think" that it would admit type-theoretic universes? $\endgroup$ – Mike Shulman Jun 25 '18 at 2:29
  • $\begingroup$ @MikeShulman I'm thinking that with a construction like this one one should be able to get universes closed under $\Sigma$-types. I'm wishfully thinking that with a bit more work the universe could also be closed under $\Pi$-types. I should admit I don't quite know what the usual requirements on a universe are, but those should be the main things, right? $\endgroup$ – Tim Campion Jun 25 '18 at 2:32
  • $\begingroup$ Ah, I see; a sort of inductive universe of codes for types. $\endgroup$ – Mike Shulman Jun 25 '18 at 4:05
  • 1
    $\begingroup$ For context: ncatlab.org/nlab/show/… $\endgroup$ – Bas Spitters Jun 25 '18 at 12:44
  • 1
    $\begingroup$ As an aside, there's is apparently a variant of the unstable motivic category which is an infinity topos: Raptis & Strunk, " Model topoi and motivic homotopy theory". I guess it's an open question as to whether their variant is a good replacement for the usual motivic category. $\endgroup$ – Charles Rezk Jun 25 '18 at 17:21
6
$\begingroup$

When you say "really it should be interpretable in any predicative $\infty$-topos", well it depends on what you mean by "homotopy type theory". Homotopy type theory is not a fixed system, but a subject that studies many different type theories. Some of those are conjectured to correspond to $(\infty,1)$-toposes, others to predicative variants, and so on.

One of the most precise statements we know is that any locally cartesian closed locally presentable $(\infty,1)$-category can be presented by a "$\Pi$-tribe" that has various kinds of higher inductive types. The latter is the conjectural semantics of Martin-Lof type theory with function extensionality and HITs, but no universes at all.

I don't know the details of in what cases a non-univalent universe can be constructed. There are various problems with making a universe (of any kind) sufficiently strict to correspond to a type-theoretic universe, but if we ignore those, then it seems possible that a non-univalent universe could be constructed in many models. I don't know anything about the motivic category, but it could well be such a model.

A subobject classifier is, in addition to propositional resizing, a univalent universe of $(-1)$-types. So this is part of the same problem. Predicativity is basically about propositional resizing or not, but in the absence of univalence the problems are more basic; even a "predicative $(\infty,1)$-topos" should satisfy univalence.

Univalence of the universe corresponds fairly closely to having colimits satisfying descent, or which are "van Kampen". It's not necessary to mess around with simplicial objects and $A_\infty$ stuff; as Christian Sattler recently reminded me, by Remark 6.1.3.11 of Higher Topos Theory, a locally cartesian closed locally presentable $(\infty,1)$-category is an $(\infty,1)$-topos as soon as pushouts are van Kampen. This property is certainly visible in the finitary syntax of type theory, even in the absence of a universe; it means that HIT pushouts (and other HITs as well) satisfy a "univalence-inspired large elimination rule". Of course if there is a univalent universe, then such a rule is derivable, but in the absence of a universe it can be postulated separately, and I believe that if there is a (not known to be univalent) universe then this elimination rule turns out to be equivalent to univalence of that universe.

So I think the answer to your question is that such a category models a version of homotopy type theory with $\Sigma, \Pi, \mathrm{Id}$ types, with function extensionality, and higher inductive types without large elimination rules, and (possibly) non-univalent universes.

$\endgroup$
  • $\begingroup$ Thanks, this is great! I will try to work out a non-van Kampen pushout example in $H(S)$. Could you expand a bit on the connection between univalence and van Kampen colimits? I know that for a locally presentable locally cartesian closed $\infty$-category, van Kampen colimits / object classifiers are each equivalent to being an $\infty$-topos. But I don't understand how univalence plays into the usual notion of an object classifier. Also, having van Kampen colimits is an "external" condition -- what does it mean to say that you can derive in type theory that pushouts are van Kampen? $\endgroup$ – Tim Campion Jun 25 '18 at 11:46
  • 1
    $\begingroup$ An object classifier $U$ is defined by the property that $\hom(X,U) \to \mathrm{core}(\mathbf{H}/X)$ is an equivalence of $\infty$-groupoids. This means that homotopies with codomain $U$ (i.e. paths in $U$) are equivalent to homotopy equivalences, which is what univalence says. Some more precise statements of the relationship can be found in section 4.8 of the HoTT book and in arxiv.org/abs/1208.1749. $\endgroup$ – Mike Shulman Jun 25 '18 at 16:45
  • 1
    $\begingroup$ @TimCampion (sorry, forgot to @ on the first comment) For your second question, in type theory with a universe, external statements about objects in a category can be internalized by quantifying over the universe. In general the relationship between the "external meaning" of such internal statements and the original external statement can be complicated, but in simple cases like this, the internal statement is a strengthening of the external one that essentially makes it "true stably over all base objects". $\endgroup$ – Mike Shulman Jun 25 '18 at 16:48
  • 1
    $\begingroup$ Most of the internal proof of van-Kampen-ness of pushouts is contained in the "flattening lemma", section 6.12 in the HoTT book. $\endgroup$ – Mike Shulman Jun 25 '18 at 16:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.