Formal smooth sets are one possible model of the Kock-Lawvere axioms

of synthetic differential geometry.

This talk will explain the toposes of smooth sets and formal smooth sets.

A smooth set is a sheaf on the site with objects

{ℝⁿ | n∈ℕ}

and all smooth maps as morhpisms.

This is a site with the Grothendieck topology

generated by good open covers, i.e. it is a collection of

open subset inclusions {Uᵢ → ℝⁿ} such that all non-empty finite intersections

are diffeomorphic to ℝⁿ. Sheaves on this site are called smooth sets.

Formal smooth sets are sheaves on an extension of this site.

The goals are:

- support synthetic differential geometry

- admit construction of 'formal schemes', e.g. the formal neighbourhood of 0 ∈ ℝ, containing all infinitesimals of all orders.

There is an article on synthetic PDEs by Urs Schreiber and Igor Khavkine which introduces and uses this topos.

Depending on demand, this talk might also cover the differential cohesive structure of this topos and its higher variant,

which is expected to provide a model for differential cohesive HoTT as it is used by David Jaz Myers in the articles:

- Modal Fracture of Higher Groups

- Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory

This talk will also introduce constructive reasoning.

The main slogan/feature of higher toposes is, that any cohomology theory can be expressed using hom-spaces and truncation in some higher topos.

Since HoTT is known to interpret in higher toposes, this yields an easy way to define cohomology internally:

Hⁿ(X,ℱ):≡∥ (x : X) → K(ℱₓ,n) ∥₀

Since this implies Hⁿ(X,ℱ)=πₖ((x : X) → K(ℱₓ,n+k)), exact sequences can be constructed using the long exact sequence for homotopy fibers F → E → B:

… → πₖ₊₁(B) → πₖ(F) → πₖ(E) → πₖ(B) → πₖ₋₁(F) → …