Yeah, I was wondering about that. Maybe I should.

]]>Urs, would you mind uploading the second version to the arXiv? I see a lot of people referencing the first version on the arXiv, instead of the second version on your home page.

]]>I am (or so I sincerly hope) slowly climbing out of the black hole that my time budget collapsed into when with enlarged family the fact that I am not working in the same country in which I live finally turned from curious into deadly. (This maybe as an excuse for the immense delay between this and the previous post.)

I have now implemented the fixes pointed out above and added attribution. In particular I briefly fixed the issue pointed out by Marc Hoyois and added a pointer to his MO post for the fix. (That’s just the bare minimum one should do, I know, but at least it’s that.)

Looking back at the document, there are a thousand things I should and would want to improve on (besides eventually adding a genuine section on quantization via linear cohesive homotopy types). I have to see what the gods decided how this is going to work out.

Until the next arXiv version (which may take a while) I’ll keep a document with the latest changes at

]]>Thanks for all this!

I am still intensely busy with some other tasks. Will get back to this as soon as there is a free slot. Thanks for all the input, everyone!

]]>p. 198

]]>$\infty$-Lie algrboid

Now, more scientific question. I am sure you thought it through when I was not following those threads in $n$Forum, but the usage of shape theory in the paper confuses me. Page 243 says

If by “size” we mean “nontriviality of homotopy groups”, hence nontriviality of shape of a > space, there is the notion of

• shape of an ∞-topos ([L-Topos], section 7.1.6);

which coincides with the topological shape of X in the case that H = Sh∞ (X), as above.

This is very confusing. The shape theory is made precisely to study the topological spaces which are not CW complexes and for which homotopy groups are not useful, nor contain useful information. The classical example, Warsaw circle has all homotopy groups $0$, but its shape is not the shape of a point, but the shape of a circle. Thus the topological shape of $X$ is by no means about “nontriviality of homotopy groups”, i.e. not about its weak homotopy type.

]]>Few bibliography corrections. First general one: many references miss comma after the title name, before the journal name, e.g. HeTe92, KaKrMi87, Mur96, Sc13a, Schw84, Sha97, Stee67, Stol96, Stre04, Zan05, Zi04, Wei89 etc.

Some other bib typoi:

Wi87 Wittem instead of Witten

Hor89 Exactly soluable

Law91, comma after Lawvere

Toppan page number *probably* 518–583 (dash missing)

I am very surprised that among the listed papers of B. Toën, G. Vezzosi, the most important one (from the point of view of this paper, I think), the HAG I paper, which is the first paper which proves in great detail and with systematic theory and rather clean exposition (in Segal category model) the Giraud’s theorem for (infinity,1)-topoi is missing. HAG II is however listed, as well as shorter proceedings version of Segal topoi theory. HAG II, full reference is Mem. Amer. Math. Soc. 193 (2008), no. 902.

]]>Thanks! I’ll get back to editing dcct from next week, Wednesday on. No chance before that.

]]>Typos on p. 196:

]]>to be regared

as a generally covarnat,

supporessing

ah, p. 44, right, I’ll change that.

and I’ll try to make me think about what I’ll do with the conflating-seeming section titles (but not tonight, and maybe not this week)

]]>Re: connectedness, I’m looking at and around the top of p44.

I’ve never heard anyone say “homotopy-type theory”. The word used to be “algebraic topology”, then “homotopy theory”, and now “$\infty$-category theory”. Have you actually heard people say “homotopy-type theory” to mean that subject?

]]>Hey, I don’t say “$\infty$-connected” the way that makes you sad. At least not in def. 3.3.1 where it is introduced and not in def. 3.4.1 where it is picked up in the context of cohesion.

Maybe I got careless elsewhere? I’ll fix it if you point me to it.

Concerning conflation: I did by now well realize that the feeling in the HoTT community about this changed, but as you were once among the first to be fond of, the old homotopy-type theory is usually written without that hyphen and it’s a lucky coincidence, not an unfortunate one.

Other people complain when there are too many “$\infty$“-signs thrown around, especially in headlines. They say it “scares” them. For them I think saying “geometric homotopy theory” instead of “$\infty$-topos theory” is a real treat.

I am drowned this week in other tasks, but then I will work on editing dcct again. I’ll see what I can do. But let’s all try generally not to be “saddened” and “scared” by mathematics too much. Let’s go for the good feelings. Life outside maths is sad and scary enough…

]]>I do wish that you wouldn’t conflate “homotopy type theory” with “$\infty$-topos theory”. They are different, though related, subjects. E.g. section 2 should really be called “$\infty$-topos theory”.

Also I’m a bit sad that you’ve decided to say “$\infty$-connected” for what should really be “locally $\infty$-connected and $\infty$-connected”.

]]>I don’t see a need to restrict the axioms. I invoke hypercompleteness just as a means of computing with my models.

]]>The hypothesis of 7.2.1.12 can actually be weakened a bit: you only need $\mathcal{X}$ to be locally of finite homotopy dimension to show that every object is the limit of its Postnikov tower, hence hypercomplete. On the other hand, to show that $\mathcal{X}=\lim_{n}\mathcal{X}_{\leq n}$, you need $\mathcal{X}$ to be locally of homotopy dimension $\leq n$ for some *fixed* $n$.

So, do you plan to restrict the definition of cohesion, or should the theory include infinite-dimensional examples like this?

]]>Ah, you are right. I dropped the “locally” from the assumption in HTT cor. 7.2.1.12. (At *homotopy dimension* I still got it right…) Luckily this can be fixed. I’ll update the file later this week. Thanks.

I think the following is an example of a cohesive (∞,1)-topos which is not hypercomplete.

Let $Cubes$ be the full subcategory of topological spaces that are homeomorphic to

$\prod_{n\in \mathbb{N}} X_n$where each $X_n$ is either $pt$, $(0,1)$, $[0,1)$, or $[0,1]$. Let

$\mathbf{H} \coloneqq Sh_\infty(Cubes).$Any $Q\in Cubes$ has a base of open sets $B\subset Cubes$ which is moreover closed under finite intersections, so that $Sh_\infty(Q)\simeq Sh_\infty(B)$, and it is clear that the embedding $i\colon B\hookrightarrow Cubes_{/Q}$ is continuous and cocontinuous. We therefore have an essential geometric morphism

$i_! \dashv i^* \dashv i_*\colon Sh_\infty(Q)\to \mathbf{H}_{/Q}$with $i_!$ and $i_*$ fully faithful. From this we deduce that $\mathbf{H}$ is not hypercomplete, since $Q$ can be the Hilbert cube. We also deduce that

$Shape(\mathbf{H}_{/Q})\simeq Shape(Sh_\infty(Q))$which is contractible since $Q$ is paracompact and contractible (HA, A.1.4). In particular, $\mathbf{H}$ is ~~totally~~ strongly ∞-connected. Finally, $\Gamma\colon \mathbf{H}\to \infty Grpd$ preserves colimits because the final object $pt\in Cubes$ has a unique covering sieve.

Also, in Prop. 4.3.7 and 4.4.9 (and maybe also 4.5.10), there’s no need to take the hypercompletion on the right-hand side: see this mathoverflow answer.

]]>@Urs:

I think Prop. 3.2.2 (3) is wrong (“local implies hypercomplete”). Your definition of a *locally local* (∞,1)-topos is basically a condition on the final object, so there’s no reason to expect that it would imply hypercompleteness (which is a local condition, unlike that of being locally local!). For example, the (∞,1)-topos of étale sheaves on all $k$-schemes, for $k$ an algebraically closed field, is local but it’s not always hypercomplete.

Lucky the typo wasn’t in the title :-P

]]>Gee, thanks. I’ll fix that with the next replacement. Grr.

]]>The arXiv abstract contains the word “**caracteristic**”.

Bookmarked for later reading: Differential cohomology in a cohesive infinity-topos (lspace).

]]>Fixed! :-)

Yes, as long as you have the energy, I’ll definitely appreciate being told about more typos.

]]>