I'm a big fan of [synthetic differential geometry](http://home.math.au.dk/kock/SGM-final.pdf) (or smooth infinitesimal analysis), as developed by Anders Kock and Bill Lawvere. It's a beautiful and intuitive geometric theory, which gives justification for the infinitesimal methods used by many of the pioneers of analysis and differential geometry, like Sophus Lie. 


I have also occasionally come across the notion of [differential cohesion](https://ncatlab.org/nlab/show/differential+cohesive+%28infinity%2C1%29-topos), which seems to be another sort of synthetic approach to differential geometry. Unfortunately, while I'm pretty comfortable with 1-category theory, I don't know much homotopy theory or higher category theory, so the language used is pretty foreign to me. There is also a lot of talk of [modalities](https://ncatlab.org/nlab/show/modality), which I don't really have any intuition for.



> 
> **Question:** What is the relationship between differential cohesion and synthetic differential geometry (in the sense of Kock & Lawvere)? 
> 
> 
> 



Relationship between synthetic differential geometry and differential cohesion?
I'm a co-author on the abstract linked in the comments but I'm coming from the computer science side so I'm not an expert on the models and I know very little classical differential geometry.


I had the same question and my current understanding is that 


1. Differential Cohesion and Synthetic Differential Geometry have the same "canonical model": the SDG people use the Cahiers topos and Diff Cohesion people use the $\infty$-sheaves on the same site.
2. They are by no means equivalent: for instance Synthetic Differential Geometry axiomatizes a real line object $R$ and the Kock-Lawvere axiom uses it, whereas in differential cohesion the notion of "infinitesimal" distance is more "formal" in that it is just derived from abstract modalities. For instance there are very simple models of DC like [this one](https://ncatlab.org/nlab/show/infinitesimally+thickened+Sierpinski+topos) that have a very strange notion of "infinitesimally close".


It's a matter of ongoing research how much differential geometry can be done using just differential cohesion, but clearly if you want to get all of the classical theorems you need to at some point axiomatize the reals (unfortunately any internal definition of the reals via Dedekind cuts will give you the wrong reals because you want to only have the smooth functions).


On the other hand Differential Cohesion is more "categorical" which syntactically means we hope to get well-behaved type-theoretic connectives instead of uninterpreted axioms, like how having the identity type in HoTT is much nicer than axiomatizing the n-spheres.


The main source for what can be formalized in (solid, differential) cohesion is [Urs' book](https://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos), look for the sections on the differential cohesion modalities to see some comparisons to SDG, but also note that much of that book can be formalized with just a cohesive topos.


For some shorter/simpler examples, see [Felix Wellen's thesis](https://ncatlab.org/schreiber/show/thesis+Wellen) if you want to see what some of differential geometry looks like using just one of the modalities from differential cohesion.
Also maybe check out [Mike Shulman's paper](https://arxiv.org/abs/1509.07584) for (non-differential) cohesion plus some axioms for a more hybrid style.


Also, when it comes to the infinity-stuff, I have been assured by experts that you can just ignore the word infinity when you are looking for intuition.
A big takeaway from infinity-category theory and Homotopy Type Theory is that infinity groupoids act a lot like sets. 


