5
$\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?

Improve this question
$\endgroup$
7
  • $\begingroup$ Why would you "have to think" that it would admit type-theoretic universes? $\endgroup$ Commented Jun 25, 2018 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$ Commented Jun 25, 2018 at 2:32
  • $\begingroup$ Ah, I see; a sort of inductive universe of codes for types. $\endgroup$ Commented Jun 25, 2018 at 4:05
  • 1
    $\begingroup$ For context: ncatlab.org/nlab/show/… $\endgroup$ Commented Jun 25, 2018 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$ Commented Jun 25, 2018 at 17:21

1 Answer 1

Reset to default
7
$\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.

Improve this answer
$\endgroup$
4
  • $\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$ Commented Jun 25, 2018 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$ Commented Jun 25, 2018 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$ Commented Jun 25, 2018 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$ Commented Jun 25, 2018 at 16:49

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.