I haven’t thought at all about this thickening business; I need to spend some time looking at it. A priori, “differential cohesion” seems a reasonable name.

I’m not quite sure that “∞-connected and locally ∞-connected” is what you want to say, though. When its codomain isn’t $\infty Gpd$, having a left adjoint to the inverse image isn’t sufficient to make a geometric morphism locally connected. And if it isn’t locally connected, then being connected (i.e. the inverse image functor being fully faithful) isn’t equivalent to the left adjoint preserving the terminal object. And of course, an embedding can never be connected (in the usual sense) without being an equivalence.

]]>So these axioms are at least a tad more general than what is strictly subsumed by “infinitesimal” theory, but in a good way:

I think these axioms also capture “germ structure” and in fact can resolve the full hierarchy:

first order infintiesimals

second order infinitesimals

…

orbitrary order infinitesimals

germs

To which corresponds the hierarchy

Lie algebra / Lie algebroid

…

formal group

local group

So that’s good. All of this can be captured by a hierarchy of differential cohesion structures

$CohesiveType \hookrightarrow FirstOrderInfThickenedCohesiveType \hookrightorder SecondOrderInfThickenedCohesiveType \hookrightarrow \cdots \hookrightarrow \cdots \hookrightarrow FormallyThickenedCohesiveType \hookrightarrow LocallyThickenedCohesiveType$ ]]>While working at *geometry of physics* on the next chapter *Differentiation* I am naturally led back to think again about how to best expose/introduce infinitesimal cohesion. To the reader but also, eventually, to Coq.

First the trivial bit, concerning terminology: I am now tending to want to call it *differential cohesion*, and *differential cohesive homotopy type theory*. What do you think?

Secondly, I have come to think that the extra right adjoint in an infinitesimally cohesive neighbourhood need not be part of the axioms (although it happens to be there for $Sh_\infty(CartSp) \hookrightarrow Sh_\infty(CartSp_{th})$ ).

So I am now tending to say

**Definition.** A *differential structure* on a cohesive topos is an ∞-connected and locally ∞-connected geometric embedding into another cohesive topos.

And that’s it. This induces a homotopy cofiber sequence

$\array{ CohesiveType &\hookrightarrow& InfThickenedCohesiveType &\to& InfinitesimalType \\ & \searrow & \downarrow & \swarrow \\ && DiscreteType }$Certainly that alone is enough axioms to say in the model of smooth cohesion all of the following:

- reduced type, infinitesimal path ∞-groupoid, de Rham space, jet bundle, D-geometry, ∞-Lie algebra (synthetically), Lie differentiation, hence “Formal Moduli Problems and DG-Lie Algebras” , formally etale morphism, formally smooth morphism, formally unramified morphism, smooth etale ∞-groupoid, hence ∞-orbifold etc.

So that seems to be plenty of justification for these axioms.

We should, I think, decide which name is best (“differential cohesion”?, “infinitesimal cohesion”?) and then get serious about the “differential cohesive homotopy type theory” or “infinitesimal cohesive homotopy type theory” or maybe just “differential homotopy type theory” respectively.

]]>