The study of abstract differential structure for categories was initiated by Thomas Ehrhard who discovered a number of models of differential structures arising from his work in linear logic. These are interesting models which have computational content which appears to be related to the semantics of distributed systems.

This work exposed the purely algebraic structure underlying differentiation. In 2008, together with Robert Seely and Rick Blute, we introduced Cartesian differential categories. An important way in which these arise is as the coKleisli category of a models of differential linear logic (as mentioned above). However, significantly, they also arise much more directly from standard (algebraic and synthetic) models of the ordinary differential calculus (on the real line). \

Given these of purely algebraic/categorical descriptions of differentiation, the possibility of capturing abstractly some of the basic ideas of differential geometry (e.g. smooth manifolds etc.) came within reach. To this end we introduced the notion of a differential restriction category: this adds partiality (and therefore topology) to the differential structure. From there one can use the manifold construction of Marco Grandis to obtain categories of "smooth manifolds". Furthermore, one can axiomatize the structure which arises using tangent spaces -- here called tangential structure.

An important example of all this structure, which I will discuss, is central to algebraic geometry.

Using an obstruction theory of Blanc-Dwyer-Goerss, we will describe the moduli space of realizations of certain 2-stage $\Pi$-algebras. This is better than a classification: The moduli space provides information about realizations as well as their higher automorphisms.

These model structures are special cases of model structures for presheaf-valued diagrams $X$ defined on a fixed presheaf of categories $E$ which is enriched in simplicial sets.

Simultaneously varying the parameter category object $E$ (or parameter space $S$) along with the diagrams $X$ up to weak equivalence is more interesting, and requires new model structures for $E$-diagrams having weak equivalences defined by homotopy colimits, as well as a generalization of Thomason's model structure for small categories to a model structure for presheaves of simplicial categories. These new model structures exist for arbitrary presheaves of simplicial categories $E$ and their categories of diagrams.

In type theory, many important objects are defined inductively: for instance, the natural numbers are defined as the type freely generated by an element ‘0’ and an endofunction ‘suc’. This gives the principles of induction and recursion which characterise $\mathbb{N}$. More general “inductive type definitions” form the most important construction principle in various type theories.

What if one similarly defines the circle to be the type freely generated by a single point and a path from that point to itself? This gives induction/recursion principles for the circle; it turns out many facts of classical algebraic topology are directly provable in the type theory using this definition.

More generally, adding these “higher inductive types”, which may be freely generated not only by points but also by paths, homotopies, and so on, gives a very powerful construction principle. Using these, one can reconstruct many topological constructions type-theoretically: spheres, more general cell complexes, mapping cylinders, truncations, and much more.