Schreiber Some thoughts on the future of modal homotopy type theory

A talk that I once gave:

---

• Urs Schreiber

  Some thoughts on the future of modal homotopy type theory

  talk at

  Homotopy Type Theory and Univalent Foundations - Mini-Symposium,

  within the

  German Mathematical Society meeting 2015

  21st - 25th Sept 2015, Hamburg

  (talk notes pdf)

---

Abstract. In 1991 William Lawvere suggested a) that the future of category theory revolves around toposes equippped with an adjoint system of idempotent (co-)monads (1) and that b) this is formalization of what the ancients had called the “objective logic” (2). While for 1-toposes this seems inconclusive, one finds (3) that internal to ∞-toposes equipped with such adjoint systems much of higher differential geometry and of modern physics has a succinct and useful synthetic formalization. But here the syntax of this internal language is modal homotopy type theory (4). In this talk I survey the immensely rich semantics and the potential prospects of its full syntactic formalization, in the hope to motivate the type theory community to further look into this fascinating but under-explored aspect of their theory.

Solved problems

Of the three open formalization problems that I had proposed in “Some thoughts…”, two have meanwhile been solved:

• Formalization of G-structure

• Formalization of the differential hexagon

Formalization of torsion-free $G$-Structures

Formalization of torsion-free G-structures on geometry of physics – manifolds and orbifolds (the first of the three open problems posed in the talk) was solved in:

• Felix Wellen,

  Formalizing Higher Cartan Geometry in Modal Homotopy Type Theory,

  PhD thesis, KIT 2017

  (thesis pdf, achived version: web, talk slides: pdf, HoTT-Agda code: DCHoTT-Agda).

A revised and extended version is given in

• Felix Wellen,

  Cartan Geometry in Modal Homotopy Type Theory,

  (arXiv:1806.05966, talk video).

Formalization of the differential hexagon

Formalization of the differential cohomology hexagon in cohesive homotopy type theory has been achieved in:

• David Jaz Myers, Modal Fracture of Higher Groups, talk at CMU-HoTT Seminar, 2021 (pdf, pdf)

• David Jaz Myers, Modal Fracture of Higher Groups (arXiv:2106.15390)

Open problems

In continuation of the above, here are further open problems of interest in cohesive modal homotopy type theory.

The overall problem is to establish the running hypothesis: that a progression (this Def.) of adjoint modalities (this Def.) of the form

(1)$$\array{ id &\dashv& id \\ \vee &\vert& \vee \\ \rightrightarrows &\dashv& \rightsquigarrow &\dashv& Rh \\ && \vee &\backslash& \vee \\ && \Re &\dashv& \Im &\dashv& \& \\ && && \vee &\vert& \vee \\ && && ʃ &\dashv& \flat &\dashv& \sharp \\ && && && \vee &/& \vee \\ && && && \emptyset &\dashv& \ast }$$

(cohesion, elasticity, solidity see here) provides a good working foundation for higher differential supergeometry with differential cohomology.

But the problems listed below are meant to be low-hanging concrete problems that should be comparatively straightforward to tackle, while still being of interest. The overall problem will be solved by solving a sufficiently large network of such concrete problems.

Fundamental theorem of calculus (Stokes’ theorem)

Formalization of the fundamental theorem of calculus/Stokes theorem as indicated there remains open.

The same key point as for the differential hexagon (above) needs to be solved.

Bosonic body of supermanifold is manifold

Consider the solid adjoint modalities with Aufhebung and focus on the following fragment of (1)

$$\array{ \rightrightarrows &\dashv& \rightsquigarrow &\dashv& Rh \\ && \vee &\backslash& \vee \\ && \Re &\dashv& \Im &\dashv& \& }$$

Here the backslash indicates “Aufhebung to the left” (this Def.), hence that coreduced objects are bosonic:

(2)$$\overset{\rightsquigarrow}{\Im X} \;\simeq\; \Im X \,.$$

Problem: Show that if $X \overset{f}{\longrightarrow} Y$ is a formally étale morphism, hence that the naturality square

(3)$$\array{ X &\overset{ \phantom{AA}\eta^{\Im}_X\phantom{AA} }{\longrightarrow}& \Im X \\ {}^{\mathllap{f}}\Big\downarrow &{}^{(pb)}& \Big\downarrow{}^{\mathrlap{ \Im f }} \\ Y &\underset{ \phantom{AA}\eta^{\Im}_Y\phantom{AA} }{\longrightarrow}& \Im Y }$$

is an (∞,1)-pullback, then also the bosonic part $\overset{\rightsquigarrow}{X} \overset{\overset{\rightsquigarrow}{f}}{\longrightarrow} \overset{\rightsquigarrow}{Y}$ is formally étale.

(This implies immediately that for $X$ a $V$-manifold in the axiomatic sense (here), then $\overset{\rightsquigarrow}{X}$ is a $\overset{\rightsquigarrow}{V}$-manifold, hence that the bosonic body of a supermanifold is an ordinary smooth manifold.)

Here is a classical proof:

First observe that the image of an $\Im$-unit on $X$ under $\rightsquigarrow$ is naturally equivalent to the $\Im$-unit of $\overset{\rightsquigarrow}{X}$:

(4)$$\overset{\rightsquigarrow}{\eta^{\Im}_X} \;\simeq\; \eta^{\Im}_{\overset{\rightsquigarrow}{X}}$$

With this, the claim follows by applying $\rightsquigarrow$ to the pullback diagram (3) and using that, being a right adjoint, it preserves pullbacks.

Here is a classical proof of (4):

$\,$

Further directions

The following is a list of subjects that would seem to naturally lend themselves to formalization in cohesive homotopy theory, but where I don’t know yet what exactly a concrete proposition would be that one might aim to prove.

The h-principle in PDE theory

h-principle in partial differential equations (PDE theory)

Focus on the differential cohesion (elasticity) fragment of (1)

$$\array{ && \Re &\dashv& \Im &\dashv& \& \\ && && \vee && \vee \\ && && ʃ &\dashv& \flat &\dashv& \sharp }$$

Using $\Im$, one may synthetically speak about partial differential equations, as in

• Igor Khavkine, Urs Schreiber, Synthetic geometry of differential equations (arXiv:1701.06238, v2, talk slides, talk video)

Using also $ʃ$ one may then state the h-principle, as discussed here.

Just defining this should be immediate. Maybe there is a theorem here waiting to be proven.

Knot theory

knot theory

The very idea of equivalence classes of knots (embeddings of smooth manifolds up to smooth isotopy) is one in differential cohesion (“elastic homotopy theory”), combining concepts of differential geometry (embeddings of smooth manifolds) with homotopy (a smooth isotopy between embeddings being a smooth homotopy/path in the smooth space of embeddings).

This should lend itself to formalization in the differential cohesion (elasticity) fragment of (1)

$$\array{ && \Re &\dashv& \Im &\dashv& \& \\ && && \vee && \vee \\ && && ʃ &\dashv& \flat &\dashv& \sharp }$$

Using the infinitesimal shape modality $\Im$ we may speak about smooth manifolds $\Sigma, X$, as in Wellen 17.

Using in addition the sharp modality we may speak of embedding of smooth manifolds (as discussed here), hence form a homotopy type

$$[\Sigma,X]_{emb} \hookrightarrow [\Sigma,X]$$

of embeddings inside the function type.

Then using the shape modality $ʃ$ we obtain $ʃ [\Sigma,X]_{emb}$. A path in this type is a smooth isotopy. Hence the 0-truncation

$$Knots_\Sigma(X) \;\coloneqq\; \big\vert ʃ [\Sigma,X]_{emb} \big\vert_0$$

should be the type of knots of form $\Sigma$ inside $X$.

Related talks

• Equivariant Super Homotopy Theory

• Modern Physics formalized in Modal Homotopy Type Theory

• Differential generalized cohomology in Cohesive homotopy type theory

• Differential cohomology is Cohesive homotopy theory

• The (co-)reflective categories of supergravity

• Higher Cartan Geometry

$\,$

$\,$