Schreiber
Some thoughts on the future of modal homotopy type theory

Contents

A talk that I once gave:



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.

Contents

Solved problems

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

Formalization of torsion-free GG-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:

A revised and extended version is given in

Formalization of the differential hexagon

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


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)id id | Rh \ & | ʃ / * \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)

Rh \ & \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)XX. \overset{\rightsquigarrow}{\Im X} \;\simeq\; \Im X \,.

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

(3)X AAη X AA X f (pb) f Y AAη Y AA Y \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 XfY\overset{\rightsquigarrow}{X} \overset{\overset{\rightsquigarrow}{f}}{\longrightarrow} \overset{\rightsquigarrow}{Y} is formally étale.

(This implies immediately that for XX a VV-manifold in the axiomatic sense (here), then X\overset{\rightsquigarrow}{X} is a V\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 XX under \rightsquigarrow is naturally equivalent to the \Im-unit of X\overset{\rightsquigarrow}{X}:

(4)η X η X \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

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 Σ,X\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

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

of embeddings inside the function type.

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

Knots Σ(X)|ʃ[Σ,X] emb| 0 Knots_\Sigma(X) \;\coloneqq\; \big\vert ʃ [\Sigma,X]_{emb} \big\vert_0

should be the type of knots of form Σ\Sigma inside XX.

\,

\,

Last revised on October 14, 2021 at 11:33:28. See the history of this page for a list of all contributions to it.