[Administrative note: I have merged this thread with one named ’tangent (oo,1)-category’, where most of the previous discussion had taken place; the present thread is the one which is picked up by the edit announcer. I took the liberty of deleting a comment of Urs’ suggesting that the present thread be used instead of the one named ’tangent (oo,1)-category’, since it would now be a bit confusing (and didn’t have other content that needed preserving).]

]]>Was the construction of taking the tangent $(\infty, 1)$-topos for the whole $(\infty, 2)$-category (∞,1)Topos ever considered around these parts?

]]>The gulf between devising things and having them be taken up is vast, and without constantly being on the case of promoting them, it seems that credit often goes missing. I await 2050 when modal HoTT becomes everyday in analytic philosophy.

]]>An $n$Lab entry stating their basic idea (here) exists since 2013 (rev 1).

I had tried to advertize formalizing this in HoTT in Paris 2014. Back then the chairman (vv) shut down my talk after I mentioned Prop. 2.5, which he claimed was false. While that was silly and abusive of him, I can see how it was pointless to try to give that talk to that audience at that time. Maybe in 10 years from now I’ll try again.

I think stable Cohomotopy – whose role in the scheme of things I didn’t appreciate back then – will lend itself to constructive formalization. So that might be a topic for 2031.

]]>Re #25, and now the article has appeared:

- Mitchell Riley, Eric Finster, Daniel R. Licata,
*Synthetic Spectra via a Monadic and Comonadic Modality*, (arXiv:2102.04099)

Hmm, that’s pretty outrageous not to have mentioned your work - dcct, Quantization via Linear homotopy types, etc.

]]>Redirect: tangent ∞-category, tangent ∞-topos.

]]>Redirect: tangent ∞-category.

]]>Some rewording to emphasise what’s different in

- {#BauerBurkeChing21} Kristine Bauer, Matthew Burke, Michael Ching,
*Tangent $\infty$-categories and Goodwillie calculus*(arXiv:2101.07819)

I was just quoting from the paper

The goal of this note is to introduce two further examples of tangent ∞-categories…

So maybe better to choose the second option. But certainly no time at the moment.

]]>Thanks for adding. But let me suggest that we need to change the wording:

If I understand well (have only skimmed the articles) these recent articles talk about a notion of “tangent structure” on $\infty$-categories which subsumes the notion discussed on our page here (which they maybe call “Goodwillie tangent structure”), but has other examples, too.

It is only in this sense that it makes sense to write articles on new examples for “tangent structures”, I suppose.

So I think the line

Two further examples of tangent $(\infty,1)$-categories

needs to be changed to something like

Two further examples of tangent structures on infinity-categories.

That, or we need to change the title and content of this page here, generalizing it all appropriately. I guess the first option is less tedious.

[edit: so I made that change in wording. But I don’t have the time now to do this any justice at the moment. Please feel invited to adjust this edit.]

]]>Added

]]>Two further examples of tangent $(\infty,1)$-categories on (∞,1)-Topos and its opposite:

- Michael Ching,
Dual tangent structures for infinity-toposes, (arXiv:2101.08805)

Added

]]>Two further examples of tangent $(\infty,1)$-categories on (∞,1)-Topos and its opposite:

- Michael Ching,
Dual tangent structures for infinity-toposes, (https://arxiv.org/abs/2101.08805)

It would be good to get to see how all this work connects.

]]>Thanks for the pointer, I had not seen that.

On the other hand, the observation that the tangent $\infty$-category of parametrized spectra is infinitesimally cohesive (dcct, Prop. 4.1.9) is used by Riley-Licata-Finster, around their slide 18. (Without any attribution, but then it’s not such a deep observation…)

]]>]]>we might speculate on how the Goodwillie tangent structure fits into the much bigger programme of ‘higher differential geometry’ developed by Schreiber [Sch13, 4.1], or into the framework of homotopy type theory [Pro13],though we don’t have anything concrete to say about these possible connections.

Thanks. I have added it here.

]]>Something to follow up when I have a moment. A paper from the talk at #19

- Kristine Bauer, Matthew Burke, Michael Ching,
*Tangent infinity-categories and Goodwillie calculus*, (arXiv:2101.07819)

Infinitesimal univalence says that infinitesimally close objects in $\text{Type}$ are types whose reductions are the same.

]]>I think I found the condition: it’s that $(U_{red} \times_X Y)_{red} \rightarrow (U \times_X Y)_{red}$ is an isomorphism.

Take $U : X \vdash F(U) : \text{Scheme}$. Infinitesimally close shapes/points $U \sim U_{red}$ are sent to infinitesimally close schemes $F(U_{red}) = U_{red} \times_X Y \sim U \tmes_X Y = F(U)$ (their reductions are the same). This is gives us what the “univalence axiom” should be.

]]>Now I’m convinced that the right lifting property is against $\text{Red}(X) \rightarrow X$.

For each $X$, and each commutative triangle $\text{Red}(X) \rightarrow Y \rightarrow X = \text{Red}(X) \rightarrow X$ with $Y \rightarrow X$ a fibration (smooth map), there is a retract $X \rightarrow Y$. That’s the same as being formally smooth.

I just need to make sense of context extension. $x : X \vdash Y(x) : \text{Scheme}$ should be a certain kind of sheaf that works well with reduction and glues to a smooth cover of $X$. The property I want to require should also be analogous to univalence.

]]>I also have the goal of making sense of a “map $X \rightarrow \text{Scheme}$ for a scheme $X$, which sends infinitesimal intervals to infinitesimal intervals”. Such a map will glue via dependent sum to a smooth map, I think. This would also formalize the intuition of “continuously varying fibers”.

$x : X \vdash Y(x) : \text{Scheme}$ goes to $\sum_{x : X} Y(x) : \text{Scheme}$, with the canonical map $\sum_{x : X} Y(x) \rightarrow X$ being a smooth map; I intend the smooth maps to be the fibrations. The reason I expect this is that they satisfy the infinitesimal lifting property, which is exactly analogous to the path lifting property for fibrations.

Anyhow, I understand you must be pretty busy. Thanks for all the time you’ve spent helping me with these “geometric type theory” ideas.

]]>One statement roughly in this direction is: A tangent $\infty$-topos is infinitesimally cohesive over its base (scroll down to the third example in the list there).

That’s the property that was recently used by somebody in the HoTT community to axiomatize spectra via modal HoTT (around slide 18 here. (Of course not attributing it this way.)

]]>Maybe a tangent category $T(C)$ is an infinitesimal path space object $C^D$, just like one considers the path space object $\text{Type}^I$ in type theory to get homotopies.

]]>added pointer to

- Vincent Braunack-Mayer,
*Combinatorial parametrised spectra*(arXiv:1907.08496)