Modern Physics formalized in Modal Homotopy Type Theory


Abstract Where plain homotopy type theory provides a formal concept-logic, adding adjoint modal operators to it (Shulman 12, Schreiber-Shulman 14, Licata-Shulman 15, Shulman 15) serves to encode determinations of further qualities. Following (Lawvere 9x-0x), these categories of being naturally organize themselves in a progressive system of oppositions and resolutions which the inclined philosopher might enjoy to compare to the informal “Science of Logic”. This formal substance subsumes modal predicate logic but is immensely more expressive. The talk surveys how (Schreiber 13) externalizing this idea into natural models gives rise to the modern mathematics of space in higher/derived geometry and to modern physics of local prequantum field theory in supergravity/string theory.


For full technical details glossed over in the following see:




We survey axioms for a system of modal operators that may naturally be added to homotopy type theory; and we survey how these induce a synthetic formalizaton of differential cohomology, higher differential geometry and of key structures in fundamental physics, notably Einstein-Cartan higher gauge prequantum field theory (dcct).

\;\;\;\;\;\;\;\;\;\; the process

Formalization. The following is written in the pseudocode formerly known as mathematics. Parts of this have been fully formalized in computer-verified code (Shulman), the rest is in a form that should lend itself to such full formalization.

Synthetic axioms. Here synthetic axiomatics is meant in contrast with the following analytic axiomatics: The restriction of homotopy type theory to homotopy 0-types (“h-sets”) is a constructive set theory. A traditional assumption is that in principle and with enough patience it is possible to fullly formalize all rigorous mathematics in set theory, and with a little bit of extra care added also in constructive set theory. This way one could imagine to formalize, in principle and with much patience, first standard simplicial homotopy theory within the h-sets, then formalize the homotopy theory of simplicial presheaves, hence of infinity-stacks, to obtain a full formalization of homotopy toposes, then impose axioms on these to formalize the particular examples of, say, smooth infinity-groupoids, formal smooth infinity-groupoids and super formal smooth infinity-groupoids that are the necessary backdrop for, finally, formalizing modern physics.

While this program already sounds hardly tractable in practice, its practical usefulness is arguably even more remote. One is reminded of the fully formal proof of 1+1=21+1 = 2 which in the Principia Mathematica takes 300 pages. Nobody ever did or will ever do any useful mathmatics (as opposed to metamathematics) based on this.

But in both cases type theory and homotopy type theory, respectively, comes to the rescue. In type theory the proof of 1+1=21+1 = 2 is as trivial as it should be, thanks to the natural concept of inductive types. Similarly, in homotopy type theory the concept of infinity-stacks is already built in: every type in homotopy type theory has the generic interpretation of an infinity-stack. Instead of throwing that away by restricting to homotopy 0-types (whose interpretation is as mere sheaves of sets) and then tediously analytically rebuilding the informaltion thus lost, it is clearly advisable to retain that structure and make use of it synthetically. This is what we do below.

Modern physics. Our axioms owe a lot to William Lawvere, who had long ago suggested ( Toposes of laws of motion ) that some suitable elementary axioms imposed on toposes should provide a good context for formalization of physics. Lawvere’s axioms of synthetic differential geometry allow to formalize differential equations and hence much of classical field theory (his motivation is drawn from continuum mechanics). However, modern physics is considerably richer than that, being based on local higher gauge quantum field theory, including fermions, hence supergeometry, and including boundary conditions such as branes in string theory. Our axioms serve to formalize considerable chunks of this, and they do so naturally in that these structures follow from just a few lines of universal constructions involving the axioms.

Metaphysics. The following indulges in idealistic jargon of “subjective and objective logic”, following (Lawvere 92, Lawvere-Rosebrugh 03, section C.1). This is meant as a suggestion for a kind of pre-mathematical meaning explanation of the axioms. Dies zu wissen ist nicht not.

Expanded talk notes



Homotopy type theory as such (UFP 13) is a logic of types, of (mathematical) concepts (Martin-Löf 73, 1.1, Ladyman&Presnel 14). (References which recall that the modern “type” is a contraction of “type of mathematical concepts” include for instance also (Sale 77, p. 6).

With the univalence axiom for weakly Tarskian type universes included – which says that this essence appears properly reflected within itself – then its interpretation via categorical semantics is in elementary homotopy toposes (Shulman 12a, Shulman 12b, Shulman 14). These are the models of homotopy type theory. Conversely, homotopy type theory is the internal language of homotopy toposes, hence the latter are its “externalization”. This way homotopy type theory overlaps much with (higher) categorical logic. See at relation between type theory and category theory for more background on this.

Accordingly, since it is more immediately readable, we display mostly categorical expressions in the following, instead of the pure type theoretic syntax.


The earliest formulation of a logic of concepts is arguably Aristotle's logic, which famously meant to reason about the relation of concepts such as “human” and “mortal”. We consider now a natural formalization of at least the core intent of Aristotle’s logic in dependent homotopy type theory.

Formalizations of Aristotle’s logic in categorical logic or type theory has previously been proposed in (LaPalmeReyes-Macnamara-Reyes 94, 2.3) and in (Pagnan 10, def. 3.1). The formalization below agrees with these proposal in the identification of the Aristotlean judgement “All BB are AA” with the type-theoretic judgement “f:BA\vdash f \colon B\to A”, and with the identification of syllogisms with composition of fuch function terms.

All BB are AA.

If CC is a concept, a type, then a judgement

c:C c \colon C

says that cc is an instance of the concept CC, or that cc is a term of type CC.

For instance if \mathbb{N} is the concept of natural numbers, then the judgement n:n \colon \mathbb{N} says that nn is a natural number. Clearly here the “concept” \mathbb{N} may just as well be thought of as the set of all its instances.

Given concepts/types AA and BB, there is the concept of maps between them, the function type BAB\to A. In the categorical semantics this is the internal hom.

The judgement that there is a function, hence an instance ff of the concept of functions

f:BA f \colon B \longrightarrow A

says that ff is a rule that takes instances/terms of BB to instances/terms of AA. At least if this is a monomorphism f:BAf \colon B \hookrightarrow A (so that the corresponding a:Af 1(a)a\colon A \vdash f^{-1}(a) is a proposition) then this says in words that ff witnesses the fact that

All instances of BB are instances of AA.

or for short just

All BB are AA

hence that if AA is das Allgemeine (general, universal) concept then BB is das Besondere (special, particular) concept.

This formalization of Aristotle’s “All BB are AA” in categiorical logic/type has been proposed in (LaPalmeReyes-Macnamara-Reyes 94, 2.3), where it is attributed to William Lawvere, and in (Pagnan 10, def. 3.1).

Notice that the choice of ff here is an important part of the formalization which is missing in Aristotle’s informal logic and causing ambiguity there.

For instance all natural numbers are real numbers, but there are many inequivalent subgroup inclusions \mathbb{Z}\hookrightarrow \mathbb{R} realizing this. For the purposes of prequantum field theory these choices correspond to the choice of Planck's constant (see the discussion there).

Similarly, once we have that the informal “All BB are AA.” is formalized by a map of types, we see further refinement of the ancient logical notion.

First, the meaning of BB,AA may depend on some context CC. Leaving that implicit is arguably the greatest source of ambiguity in Aristotle’s logic. But it is easily fixed while staying true to the original intention: in general BB and AA are to be taken as CC-dependent types. Then the intended meaning of All BB are AA. is expressed by the dependent product over the function type formed in context CC

f:C(BA). f\colon \underset{C}{\prod} (B \longrightarrow A) \,.

Second, if ff is not a monomorphism it still expresses the fact that for every instance of BB there is a corresponding instance of AA. Hence in general, we should further specify if ff is an n-truncated morphism. This is a general phenomenon in passing to higher homotopy types: the (epi, mono) factorization system on homotopy 0-types refines to a tower of (n-epi, n-mono) factorization systems for all natural numbers nn.

Individual EE is BB.

There is the unit type

E=* E = \ast

of which there is a unique instance, das Einzelne (individual). As a concept, this may be regarded as the concept of pure being: since any two instances of the concept EE just purely are, there is no distinction and hence there is a unique instance.

Hence a function of the form EBE \longrightarrow B is equivalently an instance/term bb of BB. In words this says that

The individual bb is an instance of the general concept BB.

of for short just

Individual bb is BB.

There is the identity type b=bb = b, which expresses the concept that bb is equivalent to itself.

The single introduction rule for identity types gives for all XX the statement that there is indeed an instance of this concept

r b:b=b. r_b \colon b = b \,.

The categorical semantics of (b=b)(b = b) is the loop space object Ω bB\Omega_b B, which is canonically a pointed object via the constant loop id n:*Ω bBid_n \colon \ast \to \Omega_b B.

Under composition of loops, this object canonically carries the structure of an infinity-group.


In any homotopy topos H\mathbf{H}, the operation of forming loop space objects constitutes an equivalence of (infinity,1)-categories

Grp(H)BΩH 1 */ Grp(\mathbf{H}) \stackrel{\overset{\Omega}{\longleftarrow}}{\underset{\mathbf{B}}{\longrightarrow}} \mathbf{H}^{\ast/}_{\geq 1}

between infinity-groups in H\mathbf{H} and pointed connected objects in H\mathbf{H}.

The inverse equivalence B\mathbf{B} is called delooping. See at looping and delooping for more.

Now in homotopy type theory and in elementary (infinity,1)-toposes, the definition of infinity-groups as grouplike A-infinity algebras is not available, since the latter is not a finitary concept. But by prop. the concept also has a simple finitary equivalent incarnation, which is available in homotopy type theory: we may identify an infinity-group GG with its pointed connected delooping type BG\mathbf{B}G.

Indeed this is most useful: homotopy type theory in the context of BG\mathbf{B}G is the infinity-representation theory of GG:

representation theory and equivariant cohomology in terms of (∞,1)-topos theory/homotopy type theory (FSS 12 I, exmp. 4.4):

homotopy type theoryrepresentation theory
pointed connected context BG\mathbf{B}G∞-group GG
dependent type on BG\mathbf{B}GGG-∞-action/∞-representation
dependent sum along BG*\mathbf{B}G \to \astcoinvariants/homotopy quotient
context extension along BG*\mathbf{B}G \to \asttrivial representation
dependent product along BG*\mathbf{B}G \to \asthomotopy invariants/∞-group cohomology
dependent product of internal hom along BG*\mathbf{B}G \to \astequivariant cohomology
dependent sum along BGBH\mathbf{B}G \to \mathbf{B}Hinduced representation
context extension along BGBH\mathbf{B}G \to \mathbf{B}Hrestricted representation
dependent product along BGBH\mathbf{B}G \to \mathbf{B}Hcoinduced representation
spectrum object in context BG\mathbf{B}Gspectrum with G-action (naive G-spectrum)

(NSS, dcct)

Some B 1B_1 is B 2B_2.

In order to formalize judgements of intersection of concepts of the form

Some B 1B_1 is B 2B_2.

it is necessry to specify a context. Regard both B 1B_1 and B 2B_2 as dependent types witnessed by display maps

f i:B iCf_i \colon B_i \longrightarrow C

to a common context CC. Then the product type in context, hence, in the categorical semantics, the homotopy fiber product

B 1×CB 2 B_1 \underset{C}{\times} B_2

is the type whose terms are the “some” instances of B 1B_1 which are also instances of B 2B_2, and vice versa. Indeed, the fiber product canonically sits in the homotopy pullback diagram

B 1×CB 2 B 2 B 1 C \array{ B_1 \underset{C}{\times} B_2 &\longrightarrow& B_2 \\ \downarrow && \downarrow \\ B_1 &\longrightarrow& C }

and if we read B 1×CB 2B_1 \underset{C}{\times} B_2 as “some B 1B_1” then according to the previous paragraph the top morphism expresses that “all of these particular B 1B_1 (but not necessarily all of B 1B_1 itself) are B 2B_2”.


(principal infinity-bundles as judgements)

Specifically if C=BGC = \mathbf{B}G here is pointed via a map from B 2=E=*B_2 = E = \ast, and connected, hence equivalently the delooping of its infinity-group GG of loops, then (writing now BB for B 1B_1) a map of types

c:BBG c \colon B \longrightarrow \mathbf{B}G

may be thought of as a cocycle on BB with coefficients in GG, representing a class in the nonabelian cohomology of BB. See at cohomology for more on this general concept of cohomology.

In this case the homotopy fiber of ff is the GG-principal infinity-bundle PBP \to B classified by ff, fitting into the homotopy pullback square.

P E B c BG \array{ P &\longrightarrow& E \\ \downarrow && \downarrow \\ B &\stackrel{c}{\longrightarrow} & \mathbf{B}G }

Via the above translation this is an Aristotlean judgement of the form “Some BB are EE” in the context of BG\mathbf{B}G.


In summary we have that basic judgements in Aristotle’s logic, when some implicit assumptions are made explicit and the broad intention is retained, are naturally taken to be formalized in type theory as combinations of a type former and a judgement asserting a term of that type, as follows.

Aristotle's logicformal syntaxtype theory
judgementc:Cc \colon Ctyping judgement
All BB are AA.f:BAf \colon B \longrightarrow A function type
Some B 1B_1 is B 2B_2.s:B 1×AB 2s \colon B_1 \underset{A}{\times} B_2product type
Individual EE is BB.e:EBe \colon E \to B.unit type/global element

The figure EBAE-B-A

Functions may be composed. Given b:EBb \colon E \to B and f:BAf \colon B \to A, then their composite is a function fe:EAf e \colon E \to A. In type theory this is an example of natural deduction (cut elimination), in words this is a syllogism

All BB are AA.

Individual EE is BB.


Individual EE is AA.

f :BA b :EB fb :EA \begin{aligned} f & \colon B \longrightarrow A \\ b & \colon E \longrightarrow B \\ f b & \colon E \longrightarrow A \end{aligned}

The figure BBAB-B-A

Analogously, the categorical semantics for

Some B 1B_1 is B 2B_2.

All B 2B_2 is AA.


Some B 1B_1 is AA.

(all in some context CC) is given by the horizontal composite in diagrams of the form

B 1×CB 2 B 2 A B 1 C. \array{ B_1 \underset{C}{\times} B_2 &\longrightarrow& B_2 &\longrightarrow& A \\ \downarrow && \downarrow & \swarrow \\ B_1 &\longrightarrow& C } \,.

The method (absolute Idea)

What is not present in such bare homotopy type theory is determination of further qualities of types. For instance for synthetically formalizing physics one needs that types have topological and moreover differential geometric qualities to them. Some externalizations of homotopy type theory exhibit these, others do not. We now consider adding axioms to homotopy type theory that narrow it in on those models that do exhibit further quality in addition to the pure being of types.


A general abstract way to express a kind of quality carried by types is to posit a projection operation \bigcirc that projects out the moment of pure such quality.

For instance for formalizing realistic physics one needs to determine bosonic and fermionic moments (we come to this below), and one way of doing so is by considering a projection operation that projects every space of fields to its purely bosonic body (lemma below).

Generally, for XX a type, then X\bigcirc X is to be the result of projecting out some pure quality of XX. This being a projection means that XX\bigcirc X \simeq \bigcirc \bigcirc X. For this to be constructive, we need to specify a specific comparison map that gives this equivalence. Hence we say a moment projection is an operation \bigcirc on the type system together with natural functions XXX \to \bigcirc X such that (XX)\bigcirc(X \to \bigcirc X) is an equivalence X\bigcirc \stackrel{\simeq}{\longrightarrow} \bigcirc \bigcirc X.

In categorical semantics this means essentially that \bigcirc is an idempotent monad on the type system H\mathbf{H}.

Alternatively we may ask for a comparison map the other way around, XX\Box X \longrightarrow X, such that (XX)\Box(\Box X \longrightarrow X) is an equivalence. In categorical semantics this means essentially that \Box is an idempotent comonad.


A moment on (or in) a type system H\mathbf{H} is


Given a moment, we write

H ,H \mathbf{H}_{\bigcirc, \Box} \hookrightarrow \mathbf{H}

for the inclusion of its image, which we think of as the collection of those types that exhibit the moment purely (conversely these define the kind of moment as whatever quality it is that they all exhibit purely).


This is a language construct natural and familiar also from the point of view of computational trinitarianism, see at monad (in computer science).

Further, it makes sense to refer to moments ,\Box,\;\bigcirc also as modal operators or just modalities for short, and speak of type theory equipped with such operators as modal type theory, a type-theoretic refinement of modal logic. In this language the types in H \mathbf{H}_{\Box} are the \Box-_modal types.


A moment \bigcirc or \Box may be thought of as encoding a concept of similarity: as the operator projects out some details of the quality of a type and only retains some pure moment, it coarse-grains the nature of a type to some extent. Hence two types XX and YY may be different but “similar with respect to \bigcirc-quality” if their images under \bigcirc are equivalent:

(Xsimilar Y)((X)=(Y)) (X \,similar_{\bigcirc}\, Y) \coloneqq (\bigcirc(X) \,= \, \bigcirc(Y))

(where on the right we have an identity type of the type universe).

Example of this are made explicit below as example , example .


The category H \mathbf{H}_{\bigcirc} is equivalently the Eilenberg-Moore category of \bigcirc.

This is a standard fact in category theory, see at idempotent monad – Algebras.


Prop. means that we may naturally make sense of “pure qualtity” also for (co-)monads that are not idempotent, the pure types should be taken to be the “algebras” over the monad.

A single moment \Box or \bigcirc may be interpreted as most anything, since it is not further determined yet. One now observes that there is an intrinsic, self-propelling way to further determine such abstract moments, by asking for their opposite and for their negative moments.



(unity of opposites)

The opposite of a moment \bigcirc, def. is, if it exists, another moment \Box in adjunction with it,

  1. either \bigcirc left adjoint to \Box and such that there is an adjoint triple

    H H H \mathbf{H}_{\Box}\simeq H_{\bigcirc} \stackrel{\hookrightarrow}{\stackrel{\longleftarrow}{\hookrightarrow}} \mathbf{H}

    which we denote by

    \Box \dashv \bigcirc
  2. or right adjoint to it with

    H H H \mathbf{H}_{\Box}\simeq \mathbf{H}_{\bigcirc} \stackrel{\longleftarrow}{\stackrel{\hookrightarrow}{\longleftarrow}} \mathbf{H}

    which we denote by

    . \bigcirc \dashv \Box \,.

(We always display adjoint functors with the left adjoint on top and its right adjoint beneath.)

We say that the adjunction itself is the unity of opposites, and we indicate this by labels as in

momentunityofoppositesoppositemoment. \stackrel{moment}{} \Box \stackrel{unity \atop {of\,opposites}}{\dashv} \bigcirc \stackrel{opposite\;moment}{} \,.

In categorical semantics an opposition of moments, def. ,

It is fairly familiar from the practice of category theory that adjunctions express oppositions. The following example is drawn from arithmetic and is meant to illustrate this in a familar context, but the actual examples that we will be concerned with are more fundamental.


Consider the two inclusions even,odd:(,<)(,<)even, odd \colon (\mathbb{Z},\lt ) \hookrightarrow (\mathbb{Z},\lt) of the even and the odd integers, i.e. the maps n2nn \mapsto 2 n and n(2n+1)n \mapsto (2n+1), respectively.

oddeven \mathbb{Z} \stackrel{\overset{even}{\hookrightarrow}}{\stackrel{\longleftarrow}{\underset{odd}{\hookrightarrow}}} \mathbb{Z}

Both are adjoint to the operation of forming the floorfloor of the result of dividing by two, this is right adjoint to the inclusion of even numbers, and left adjoint to the inclusion of odd numbers.

even odd \array{ \stackrel{even}{} & \Box &\dashv& \bigcirc & \stackrel{odd}{} }

This has been considered in (Lawvere 00)


Consider the inclusion ι:(,<)(,<)\iota \colon (\mathbb{Z}, \lt) \hookrightarrow (\mathbb{R}, \lt) of the integers into the real numbers, both regarded linear orders. This inclusion has a left adjoint given by ceilingceiling and a right adjoint given by floorfloor. The composite CeilingιceilingCeiling \coloneqq \iota ceiling is an idempotent monad and the composite FloorιfloorFloor \coloneqq \iota floor is an idempotent comonad on \mathbb{R}. Both express a moment of integrality in an real number, but in opposite ways, each real number xx\in \mathbb{R} sits in between its floor and celling

Floor(x)<x<Ceiling(x). Floor(x) \lt x \lt Ceiling(x) \,.
ceiling floor. \array{ \stackrel{ceiling}{} &\bigcirc &\dashv& \Box & \stackrel{floor}{} } \,.

This example highlights that:


There is an opposition between the two kinds of opposition here:

  1. ()(\Box \dashv \bigcirc) – Here are two different opposite “pure moments” .

  2. ()(\bigcirc \dashv \Box) – Here is only one pure moment, but two opposite ways of projecting onto it.

Determinate negation

If X\Box X is a pure moment found inside XX, then it makes to ask for its complement moment or its negative


The negative of a comonadic moment \Box is what remains after taking away the piece of pure \Box-quality, hence is the cofiber of the counit map:

¯Xcofib(XX). \overline{\Box} X \coloneqq cofib(\Box X \to X) \,.

The intuitive meaning suggests to ask whether this kind of negation of determinations is faithful in that there is no \Box-moment left in the negative ¯\overline{\Box}, hence whether

¯*. \Box \overline{\Box} \simeq \ast \,.

In general there is no reason for this to be the case. But if \Box also has an opposite in the sense of def. , then one of the two opposite moments is left adjoint, hence preserves cofibers, and then a little more may be said.

Consider the case of an opposition of the form \bigcirc \dashv \Box. In view of remark then both \bigcirc and \Box express the same pure moment, just opposite ways of projecting onto it. Therefore in this situation it makes sense to alternatively ask that there is no \bigcirc-moment left in the ¯\overline{\Box}.


Given a unity of opposite moments \bigcirc \dashv \Box, def. , we say this has determinate negation if \Box and \bigcirc both restrict to 0-type and such that there

  1. **\bigcirc \ast \simeq \ast;

  2. \Box \longrightarrow \bigcirc is epi.


For an opposition with determinate negation, def. , then on 0-types there is no \bigcirc-moment left in the negative of \Box-moment:

¯*. \bigcirc \overline{\Box} \simeq \ast \,.

Given that \bigcirc, being a left adjoint, preserves colimits, hence cofibers, the first condition in def. gives that

¯X=cofib(XX)cofib(XX). \bigcirc \overline{\Box} X = \bigcirc cofib(\Box X \to X) \simeq cofib(\Box X \to \bigcirc X) \,.

Now the second condition and the fact that epiness is preserved by pushout say that this result receives an epimorphism from the terminal object. But this forces it to be the terminal obect itself.

The proof of prop. depends crucially on the restriction to 0-types. At the other extreme, on stable types the intuition that \bigcirc-moment is complementary to ¯\overline{\Box}-moment is verified in the following sense:


For opposite moments of the form \bigcirc \dashv \Box, def. , then for stable types XX the hexagons

¯X ¯X ¯X X ¯X X X \array{ && \overline{\bigcirc} X && \longrightarrow && \overline{\Box} X \\ &\nearrow& &\searrow& & \nearrow && \searrow \\ \overline{\bigcirc} \Box X && && X && && \bigcirc \overline{\Box} X \\ &\searrow& &\nearrow & & \searrow && \nearrow \\ && \Box X && \longrightarrow && \bigcirc X }

are homotopy exact in that

  1. both squares are homotopy Cartesian, hence are fracture squares;

  2. the boundary sequences are long homotopy fiber sequences.

In particular every stable type is the fibered direct sum of its pure \bigcirc-moment and its pure ¯\overline{\Box}-moment:

X(X)¯X(¯X). X \simeq (\bigcirc X) \underset{\bigcirc \overline{\Box} X}{\oplus} (\overline{\Box} X) \,.

In this form this has been highlighted in (Bunke-Nikolaus-Völkl 13) in the context of our prop. below. See at differential hexagon for the proof.

Note that in the diagram we have also referred to the negative of a monadic moment, ¯X\overline{\bigcirc} X. We define this as follows:


The negative of a monadic moment \bigcirc is the fiber of the unit map:

¯Xfib(XX). \overline{\bigcirc} X \coloneqq fib(X \to \bigcirc X) \,.



Say that a moment \bigcirc, is exhibited by a type JJ if \bigcirc is equivalently JJ-homotopy localization

loc J. \bigcirc \simeq loc_{J} \,.

This implies in particular that J*\bigcirc J \simeq \ast.


We have seen how to formalize determination of qualities of types together with their opposite and their negative determination. But so far these determinations are abstract in that when interpreting them in models they could come out as all kinds of very different-natured (co-)monads. What is missing is something that bases these determinations on a concrete ground with respect to which they would gain actual meaning.

Indeed, there are natural ways in which determinations of qualities may progress from given ones to further ones: on the one hand a given unity of oppositions may itself have an opposite and hence exhibit a higher order “opposition of oppositions”, on the other hand a given unity of oppositions may be “resolved” inside one new quality, which then in turn may have its own opposite and negative in turn, and so on.

Progression I: Higher order opposition

Given a concrete particular moment (i.e. an interpretation of the moment in categorical semantics), then adjoints to it are a property of the moment, not a choice to made. Abstractly we may specify that moments proceed to further moments this way by positing further adjoints.


(opposition of unities of oppositions)

Given one opposition \Box \dashv \bigcirc, we say that on opposition of oppositions is a further left adjoint \lozenge \dashv \Box, which we may think of as constituting a system of adjoints of this form:

unity2 oppositionofunities unity1 . \array{ \lozenge &\overset{unity\;2}{\dashv}& \Box \\ \bot &\stackrel{opposition \atop {of\;unities}}{}& \bot \\ \Box &\underset{unity\;1}{\dashv}& \bigcirc } \,.

(Indeed, an adjoint triple is equivalently an adjunction of adjunctions, see here).

In principle this may go on, but in models one finds that there are essentially no examples with a fourth adjoint that do not degenerate to the ambidextrous situation where \lozenge \simeq \bigcirc.

This shows further how oppositions serve to further determine moments: while a bare \Box-operator has all kinds of unrelated interpretations in models, asking it to be in opposition with a \bigcirc-moment considerably constrains its possible interpretations, further asking it to participate in an opposition-of-oppositions constraints it much more still, and asking for yet one more opposition tends to overconstrain it such as to degenerate.

Progression II: Resolution of oppositions

There is another way for a system of moments to proceed, not by adding further oppositions, but by resolving them.


(resolution of unity of opposites)

Given an essential subtopos \Box \dashv \bigcirc then one may ask if it sits inside a bigger essential subtopos, we write

2 2 1 1 \array{ \Box_2 &\dashv& \bigcirc_2 \\ \vee && \vee \\ \Box_1 &\dashv& \bigcirc_1 }

to indicate that the image of 1\bigcirc_1 is contained in the image of 2\bigcirc_2, and we say that 2\bigcirc_2 is at a higher level or in a higher sphere than 1\bigcirc_1.

If in addition 1< 2\Box_1 \lt \bigcirc_2 then this means that the opposing moments of 1 1\Box_1 \dashv \bigcirc_1 both are of purely 2\bigcirc_2 nature, and hence we say that 2\bigcirc_2 resolves or lifts or sublates or is Aufhebung of this (unity of) oppostions. We might indicate this by:

2 2 1 1 \array{ \Box_2 &\dashv& \bigcirc_2 \\ \vee && \vee \\ \Box_1 & &\dashv& \bigcirc_1 }

Dually there may be Aufhebung of the form

2 2 1 1 \array{ & \Box_2 &\dashv& \bigcirc_2 \\ & \vee && \vee \\ \Box_1 &\dashv& & \bigcirc_1 }

Notice that for oppositions of the other form, given

2 2 1 1 \array{ \bigcirc_2 &\dashv& \Box_2 \\ \vee && \vee \\ \bigcirc_1 &\dashv& \Box_1 }

then resolution in the sense that 2 1 1\bigcirc_2 \Box _1 \simeq \Box_1 and 2 1 1\Box_2 \bigcirc_1 \simeq \bigcirc_1 is automatic.

These two kinds of progression, higher order opposition, def. , and resolution of oppositions, def. , may alternate to produce processes of oppositions of moments and of their resolutions of the form

b b a a a a \array{ \vdots &\dashv& \vdots \\ \bot && \bot \\ \lozenge_b &\dashv& \Box_b \\ \vee && \vee \\ \lozenge_a &\dashv& \Box_a \\ \bot && \bot \\ \Box_a &\dashv& \bigcirc_a }

Objective Logic

By the above discussion, we are led to add to homotopy type theory the axiom that there are various moments \bigcirc or \Box. But which?

In the existing literature on modal logic it is tradition to consider unspecified idempotent (co-)monads to the formal system and have them acquire the intended meaning only via a specific choice of interpretation in a model. But here we are after developing genuine theory that works across all its possible interpretations, and hence we want an axiomatic determination of moments.

We observe now that there is a canonical starting point of two opposing moments that are secretly present in plain homotopy type theory. This hence constitutes a ground from which naturally a progression, as above, of determinations of further moments emanates.

The ground

The beginning

We observe now that in plain type theory already by itself carries one non-trivial unity of opposites.

There is the unit type *\ast. As a concept, this is the concept with a unique instance (up to equivalence). As such this may be thought of as the concept of “pure being”: an instance of this concept just purely is, without having any further qualities, and hence two instances have no distinctions between them, both just purely are, nothing else, and so they are indistinguishlably the same.

Every type has a unique map X*X\to \ast to that. Hence there is the monad which sends every type to *\ast and this is a moment

=* \bigcirc = \ast

according to def. .


Every type is similar to every other, in the formal sense of def. , with respect to the *\ast-moment. This says that all things are similar at least in that they are at all (§906).

Dually there is the empty type \emptyset. As a concept, this is the concept with no instance. As such this may be thought of as the concept of “not being”: since any instance of that concept would at least be (namely be an instance of the concept), but there is no such instance.

The empty type is such that it has a unique map X\emptyset \to X to any other type XX, hence the comonad which sends every type to the empty type, and this is a moment

=. \Box = \emptyset \,.

It is immediate that:


In plain homotopy type theory there is a unity of opposites, def. ,

*. \emptyset \dashv \ast \,.

We also call this the initial opposition.


It may be suggestive to think of this initial opposition in one of the following ways.

  1. The initial opposition of prop. is (leaving context extension notationally implicit) the adjunction between dependent sum and dependent product over the context given by the empty type

    ()(). \underset{\emptyset}{\sum}(-) \;\vdash\; \underset{\emptyset}{\prod}(-) \,.
  2. The initial opposition of prop. is the Cartesian product \dashv internal hom-adjunction of the empty type

    (()×)(()). \left( (-) \times \emptyset \right) \;\dashv\; \left( \emptyset \to (-) \right) \,.

On the other hand, the Cartesian product\dashvinternal hom-adjunction of the unit type

(()×*)(*()) \left( (-) \times \ast \right) \;\dashv\; \left( \ast \to (-) \right)

is the identity moment, in opposition with itself:

idid. id \dashv \id \,.

This trivially resolves the initial opposition. Moreover, the negative, def. , of idid is *\ast:

id¯=* \overline{id} = \ast

So that we find

id id =*¯ * =id¯. \array{ id &\dashv& id & = \overline{\ast} \\ \vee && \vee \\ \emptyset &\dashv& \ast & = \overline{id} } \,.

From this perspective it seems as if alternatively (idid)(\id \dashv \id) could be referred to as the initial opposition.

Notice for completeness that the negative, def. , of \emptyset is the maybe monad. (This is however not a moment in the sense of def. since it is not idempotent.)

Now we may find a progression of further moments by considering the resolution of this unity and then opposites to this resolution, and so forth.


Every essential subtopos level \Box \dashv \bigcirc contains the initial opposition of prop. as the minimal one:

*. \array{ \Box &\dashv& \bigcirc \\ \vee && \vee \\ \emptyset &\dashv& \ast } \,.

Double negation

We are to demand that this provides a resolution, def. of the initial opposition *\empty \dashv \ast, prop. , in that

. \bigcirc \emptyset \simeq \emptyset \,.

In the categorical semantics this says equivalently that ()(\Box \dashv \bigcirc) is a dense subtopos.


The smallest dense subtopos of a topos is that of local types with respect to double negation loc ¬¬\sharp \coloneqq loc_{\neg \neg}.

(Johnstone 02, corollary A4.5.20).

Therefore we may add the demand that the resolution of (*)(\emptyset \dashv \ast) be by loc ¬¬loc_{\neg \neg} (Lawvere 91, p. 8, Shulman 15). This equivalently means to demand that the double negation subtopos is essential .

Thus we have found the first step in the process by demanding resolution of the initial opposition. We will denote this by

=loc ¬¬ * \array{ \flat &\dashv& \sharp & = loc_{\neg \neg} \\ \vee && \vee \\ \emptyset &&\dashv& \ast }

The double negation subtopos is Boolean topos.

(Johnstone 02, lemma A4.5.21)

This means that ()(\flat \dashv \sharp) is naturally regarded as being the ground topos of the topos formed by the ambient type system, with the corresponding adjoint triple

H ΓH \mathbf{H}_{\sharp} \stackrel{\hookrightarrow}{\stackrel{\stackrel{\Gamma}{\longleftarrow}}{\hookrightarrow}} \mathbf{H}

regarded as the termimal geometric morphism whose direct image Γ\Gamma forms global points (aka global sections).

Therefore we label the resolution of the initial opposition as “ground” for “ground topos”(base topos).

=loc ¬¬ ground *. \array{ \flat &\dashv& \sharp & = loc_{\not\not} \\ \vee &\stackrel{ground}{}& \vee \\ \emptyset &\dashv& \ast } \,.
Cohesive substance

This means then that \flat is the operation of taking global points and regarding the collection of them as equipped with discrete structure. Hence \flat is the moment of pure discreteness.

This in turn means that \sharp is the moment of pure continuity (co-discreteness).

discreteness =loc ¬¬ continuity ground * \array{ \stackrel{discreteness}{} & \flat &\dashv& \sharp &= loc_{\not\not}& \stackrel{continuity}{} \\ & \vee &\stackrel{ground}{}& \vee \\ & \emptyset &\dashv& \ast & }

We may hence also say that X\flat X is the “point content” of XX. If we regard the equivalence class of X\flat X then this is the cardinality of the point content of XX, the Größe of the point content, the discrete quantity of XX.

content discreteness =loc ¬¬ continuity ground * \array{ & && \flat && \stackrel{content}{} \\ & && \bot & \\ \stackrel{discreteness}{} & \flat &\dashv& \sharp & = loc_{\not \not}& \stackrel{continuity}{} \\ & \vee &\stackrel{ground}{}& \vee \\ & \emptyset &\dashv& \ast & }

The types XX that are fully determined by their moment of continuity are those for which XXX \to \sharp X is a monomorphism. In categorical semantics these are the concrete objects or equivalently the separated presheaves for \sharp: they are determined by their global points. These are the codomains of those functions which in thermodynamics one calls intensive quantities, functions whose value is genuinely given by their restriction to all possible points.

Contrary to that, objects which have purely the negative moment of continuity ¯\overline{\sharp} are codomains for “fuctions” which vanish on points and receive their contribution only from regions that extend beyond a single point. In thermodynamics these are called extensive quantities, (e.g. differential forms in positive degree). This concept of extension is precisely that which gave the name to Hermann Grassmann‘s Ausdehnungslehre that introduced the concept of exterior differential form.

In summary, we have found that ()(\flat \dashv \sharp) expresses quantity, discrete quantity and continuous quantity, and that the latter is further subdivided into intensive and extensive quantity.

content discrete ¯/ quantity continuous(intensive/extensive) ground * \array{ & && \flat & && \stackrel{content}{} \\ & && \bot & && \\ \stackrel{discrete}{} & \overline{\flat}/\flat &\stackrel{quantity}{\dashv}& \sharp & & & \stackrel{continuous\; (intensive/extensive)}{} \\ & \vee &\stackrel{ground}{}& \vee \\ & \emptyset &\dashv& \ast & }

Proceeding, we next demand a second order opposition, def. , of the above opposition ()(\flat \dashv \sharp), hence we posit a moment ʃ&#643; such that

ʃ . \array{ &#643; &\dashv& \flat \\ \bot && \bot \\ \flat &\dashv& \sharp } \,.

We ask this to have definite negation, def. . This means that

  1. ʃ**&#643; \ast \simeq \ast — the shape of the point is trivial;

  2. ʃ\flat \to &#643; is epi on 0-types — the points-to-pieces transform is onto.

Together this are the axioms of cohesion as considered in (Lawvere 07). (There it is additionally asked that ʃ&#643; preserves binary Cartesian products.)

The intuition is that positing these qualites on a type system makes it, or rather its types XX, behave like a cohesive substance where points X\flat X are separate but held together by a cohesive attraction which, when the opposing repulsion is removed and only pure ʃ&#643;-moment is retained, makes them collapse to the components ʃX&#643; X.

The second clause here is closely related to ()(\flat \dashv \sharp) providing Aufhebung for (*)(\emptyset \dashv \ast):


If ʃ\flat \to &#643; is epi on 0-types, then \sharp \emptyset \simeq \emptyset. Conversely, if \sharp \emptyset \simeq \emptyset and H \mathbf{H}_{\sharp} is a Boolean topos, then ʃ\flat \to &#643; is epi on 0-types.

(Lawvere-Menni 15, lemmas 4.1, 4.2).

In the more refined categorical semantics of homotopy toposes \flat modulates locally constant infinity-stacks. The above adjunction then expresses the central statement of higher Galois theory (dcct):

XGrpd ʃXGrpd \frac{X \to \flat Grpd_\infty}{&#643; X\to Grpd_\infty}

saying that locally constant \infty-stacks on XX are equivalent to infinity-permutation representations of ʃX&#643; X, and that ʃX&#643; X therefore is the fundamental infinity-groupoid of XX, the shape of XX, both in the intuitive as well as in the technical sense of algebraic topology.

Therefore we further add labels as follows.

shape ʃ content discrete ¯ / quantity =loc ¬¬ continuous(intensive/extensive) ground * \array{ \stackrel{shape}{} && & &#643; &\stackrel{}{\dashv}& \flat & & & \stackrel{content}{} \\ && & \bot &\stackrel{}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }

This means that in the presence of the further opposition ʃ&#643; \dashv \flat the types XX which already had an underlying point content X\flat X now also have a shape determined by these points sticking together via a cohesive attraction. This is a qualitative aspect of the types in addition to their quantitative moments X\flat X and X\sharp X.


By remark the shape modality ʃ&#643; determines a concept of similarity of types. This is a well known one: ʃ encodes that two types have the same shape. XX and YY may look like different differential geometric spaces, but (Xsimilar ʃY)(X \, similar_{&#643;} Y) holds if they have the same shape.

In the standard model given by smooth infinity-groupoids, discussed in some detail around theorem below there is for instance the circle S 1S^1 and the cylinder S 1×(0,1)S^1 \times (0,1) over it, both regarded as smooth manifolds in the standard way. As such they are not equal (not diffeomorphic), but clearly they are similar in some sense. The shape modality makes one such sense precise: ʃ(S 1)ʃ(S 1×(0,1)B&#643; (S^1) \simeq &#643; (S^1 \times (0,1) \simeq B \mathbb{Z} and hence

S 1similar ʃ(S 1×(0,1)). S^1 \, similar_{&#643;} \, (S^1 \times (0,1)) \,.

For instance there are now types for which X=*\flat X = \ast and yet they may be very different from the point *\ast themselves, hence while quantiatively these do not differ from the point, they must have some quality that distinguish them from the point. Hence this unity of opposites is geometric quality. In standard models this geometric quality is for instance topology or smooth structure or formal smooth structure or supergeometric structure.

Therefore we write:

shape ʃ quality content discrete ¯ / quantity =loc ¬¬ continuous(intensive/extensive) ground * \array{ \stackrel{shape}{} && & &#643; &\stackrel{quality}{\dashv}& \flat & & & \stackrel{content}{} \\ && & \bot &\stackrel{}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }

Since with (ʃ)(&#643; \dashv \sharp) we have arrived at an opposition of the form ()(\bigcirc \dashv \Box), we should ask for further determination of these qualities by demanding via def. that ʃ&#643; is exhibited by \mathbb{R} (def. ):

ʃ=loc . &#643; = loc_{\mathbb{R}} \,.

In view of the above interpretation of (ʃ)(&#643;\dashv \flat) via higher Galois theory, this comes with a clear meaning: this produces the A1-homotopy theory for 𝔸 1=\mathbb{A}^1 = \mathbb{R}. We may think of \mathbb{R} as being the continuum, i.e. the real line which is the model for the geometric paths that make ʃX&#643;X be the fundamental infinity-groupoid of XX.

Gauge (Measure)

With the concepts given by ()(\flat \dashv \sharp) and by (ʃ)(&#643; \dashv \flat) thus understood, it remains to find which concept the full unity of unities of opposites

ʃ \array{ &#643; &\dashv& \flat \\ \bot && \bot \\ \flat &\dashv& \sharp }


Recall that the Brown representability theorem from stable homotopy theory:


stable homotopy typesEE are equivalently generalized cohomology theories E E^\bullet via

E (X)=[X,S]. E^\bullet(X) = [X,S] \,.

For the moments (ʃ)(&#643; \dashv \flat) the exact hexagon of prop.

ʃ¯X ¯X ʃ¯X X ʃ¯X X ʃX \array{ && \overline{&#643;} X && \stackrel{}{\longrightarrow} && \overline{\flat} X \\ & \nearrow & & \searrow & & \nearrow_{} && \searrow \\ \overline{&#643;} \flat X && && X && && &#643; \overline{\flat} X \\ & \searrow & & \nearrow & & \searrow && \nearrow_{} \\ && \flat X && \longrightarrow && &#643; X }

exhibits cohesive stable homotopy types XX as differential generalized cohomology theories.

Moreover, the existence of \sharp means that the mapping stacks into these coefficients have differential concretification to moduli stacks of differential cocycles.

The first statement is the key insight in (Bunke-Nikolaus-Völkl 13). For more amplification of this point see at Differential cohomology is Cohesive homotopy theory.

Here the moments appearing in the hexagon have the following interpretation.

connectionformsontrivialbundles deRhamdifferential curvatureforms curvature deRhamtheorem flatdifferentialforms geometricbundleswithconnection rationalizedbundle topol.class Cherncharacter geometricbundleswithflatconnection comparison/regulatormap shapeofbundle \array{ && {{connection\;forms}\atop{on\;trivial\;bundles}} && \stackrel{de\;Rham\;differential}{\longrightarrow} && {{curvature}\atop{forms}} \\ & \nearrow & & \searrow & & \nearrow_{\mathrlap{curvature}} && \searrow^{\mathrlap{de\;Rham\;theorem}} \\ {{flat}\atop{differential\;forms}} && && {{geometric\;bundles}\atop{with\;connection}} && && {{rationalized}\atop{bundle}} \\ & \searrow & & \nearrow & & \searrow^{\mathrlap{topol.\;class}} && \nearrow_{\mathrlap{Chern\;character}} \\ && {{geometric\;bundles}\atop{with\;flat\;connection}} && \underset{comparison/regulator\;map}{\longrightarrow} && {{shape}\atop{of\;bundle}} }

Now, cocycles in differential cohomology are the mathematical incarnation of physical fields in (stable) higher gauge theory (e.g. Freed 00). Hence the existence of the opposing moments ʃ&#643; \dashv \flat \dashv \sharp means that types carry gauge measure.

From the gauge theoretic perpective the \flat-moment is that exhibited by flat infinity-connections, its negative ¯\overline{\flat} moment is that exhibited by infinity-connections given by just differential form data. For ordinary differential cohomology, differential K-theory etc. this is the “rational” aspect.

Hence in summary we have found determinations as follows.

shape loc = ʃ quality / ¯ content(flat/rational) gaugemeasure discrete ¯ / quantity =loc ¬¬ continuous(intensive/extensive) ground * \array{ \stackrel{shape}{} && loc_{\mathbb{R}} = & &#643; &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ && & \bot &\stackrel{gauge\;measure}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }
Elastic substance

Continuing the process, we posit a further opposition of moments lifting the previous ones.

& ʃ \array{ \Im &\dashv& \& \\ \vee && \vee \\ &#643; &\dashv& \flat }

Since these are oppositions of the form \bigcirc \dashv \Box, Aufhebung is automatic here and not a further axiom.

To see what these new moments mean, observe that now

XXʃX X \to \Im X \to &#643; X

is a factorization of the full shape projection through a finer approximation. Hence in addition to an intrinsic concept of path (a 1-morphism in the fundamental infinity-groupoid ʃX&#643; X) there is now an intrinsic concept of small path.

Accordingly, what were locally constant infinity-stacks in the higher Galois theory encoded by \flat now become coverings that are constant on small scales. This is the concept of étale morphism as being a formally étale morphism with a condition of smallness on its fibers.

Hence we find that this further determination is that of the moment of being étalé.

infinitsimalshape infinitesimalquality & étalé shape loc = ʃ quality / ¯ content(flat/rational) gaugemeasure discrete ¯ / quantity =loc ¬¬ continuous(intensive/extensive) ground * \array{ \stackrel{infinitsimal \atop shape}{} && & \Im &\stackrel{infinitesimal \atop quality}{\dashv}& \& & && \text{étalé} \\ && & \vee && \vee \\ \stackrel{shape}{} && loc_{\mathbb{R}} = & &#643; &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ && & \bot &\stackrel{gauge\;measure}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }

Proceed by positing a further opposition \Re \dashv \Im.

To see what this moment means, observe that the “small shape” obtained above is representable by passing to pure \Re-moments

UXUX \frac{U \to \Im X}{\Re U \to X}

This has been understood in the 60s, in the context of crystalline cohomology, to be the characterization of paths that are so small that they are infinitesimal. The negative ReRe-moment is that of infinitesimal objects, the pure \Re-moment is that of “reduced objects” (“real” objects), those without infinitesimal extension.

In summary this gives:

infinitesimal/reduced ¯ / infinitesimalshape infinitesimalquality & étalé shape loc = ʃ quality / ¯ content(flat/rational) gaugemeasure discrete ¯ / quantity =loc ¬¬ continuous(intensive/extensive) ground * \array{ \stackrel{infinitesimal/reduced}{} &\overline{\Re} & / & \Re &\dashv& \Im & & & \\ && & \bot && \bot \\ \stackrel{infinitesimal \atop shape}{} && & \Im &\stackrel{infinitesimal \atop quality}{\dashv}& \& & && \text{étalé} \\ && & \vee && \vee \\ \stackrel{shape}{} && loc_{\mathbb{R}} =& &#643; &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ && & \bot &\stackrel{gauge\;measure}{}& \bot \\ \stackrel{discrete}{} &\overline{\flat}& / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }

More in detail, we may ask just how small these small paths are. Hence we demand more generally an infinite tower

ʃ<= ()<< (3)< (2)< (1)<id &#643; \lt \Im = \Im_{(\infty)} \lt \cdots \lt \Im_{(3)} \lt \Im_{(2)} \lt \Im_{(1)} \lt id

of infinitesimal shape modalities, yielding a further factorization of the shape unit as

X (1)X (2)X (3)XXʃX. X \to \Im_{(1)}X \to \Im_{(2)}X \to \Im_{(3)} X \to \cdots \to \Im X \to &#643; X \,.

In total, so far these are the axioms of differential cohesion (dcct). Using these one may naturally axiomatize local diffeomorphism (def. below), jet bundles and related concepts.

Hence with these moments posited, types now now qualities of synthetic differential geometry. On top of just cohesively sticking to each other, the terms in the types now may feel a tighter differential connectedness, we have now a rigidly elastic substance.

Solid substance

Proceed to a new level of oppositions

R . \array{ \rightsquigarrow &\dashv& \R \\ \vee && \vee \\ \Re &\dashv& \Im } \,.

This gives for each type XX a factorization

XXX \Re X \longrightarrow \stackrel{\rightsquigarrow}{X} \longrightarrow X

of the comparison map of the reduction modality \Re.

This hence means now that the purely \rightsquigarrow-types are in between reduced type and unreduced types, hence they are reduced in some sense, but possibly not properly. Hence there are now two kinds of infinitesimals, and the \rightsquigarrow-types have no extension by infinitesimals of one kind, but possibly infinitesimal extension of the other kind is left.

Hence there is now a kind of grading on the infinitesimals and \rightsquigarrow quotients out everything not in degree 0.

The geometric quality of our formal substance that this encodes so far may hence be thought of as akin to Kapranov's noncommutative geometry, which is about ordinary spaces which however may have exotic noncommutative infinitesimal thickenings. We will find that the next two determinations in the progression of the moments refines this further to something of the quality of supergeometry, where the infinitesimal thickening satisfies some strong constraints.

Cyclic grading

The moments proceed by a further higher-oder opposition

R \array{ \rightrightarrows &\dashv& \rightsquigarrow \\ \bot && \bot \\ \rightsquigarrow &\dashv& \R }

For this to have non-degenerate models one finds that infinitesimals in degree 0 must be allowed to map to products of infinitesimals in non-vanishing degree. This means that the grading is not by a free group, but for instance by a finite cyclic group /n\mathbb{Z}/n\mathbb{Z}-grading. The minimal choice is /2\mathbb{Z}/2\mathbb{Z}-grading.


We are to require that this level provides Aufhebung of the previous oppositions, def. , in that

XX. \stackrel{\rightsquigarrow}{\Im X} \simeq \Im X \,.

for all types XX. By adjunction this means that

UU \Re \stackrel{\rightrightarrows}{U} \simeq \Re U

for a set of generators UU, such as objects of a site.

This says that the reduced part of the even-graded part is the same as the reduced part of the original, hence that odd-grade is removed by reduction, hence that odd-graded moment is nilpotent. In superalgebra this is the key consequence of the super-sign rule (Hermann Grassmann, §37 in Ausdehnungslehre, 1844) which says that for odd coordinate functions θ 1\theta_1, θ 2\theta_2 we have

θ 1θ 2=θ 2θ 1, \theta_1 \theta_2 = -\theta_2 \theta_1 \,,

see prop. below.

Hence we think of the above Aufhebungs-condition as further determining the graded function algebras to actually be superalgebras.

By the Pauli exclusion principle/spin-statistics theorem, this is what characterizes fermions: the purely fermionic part is the negative moment ¯\overline{\rightsquigarrow}.

We indicate this notationally by

e¯ \e \coloneqq \overline{\rightsquigarrow}

We may still further determine this, via def. , be requiring that there exists a type 0|1\mathbb{R}^{0|1} which exhibits R\R, in that Rloc 0|1\R \simeq loc_{\mathbb{R}^{0|1}}.

In summary we now have arrived at the following process of determinations.

/ e bosonic/fermionic R =loc 0|1 super infinitesimal/reduced ¯ / infinitesimalshape infinitesimalquality & étalé shape loc = ʃ quality / ¯ content(flat/rational) gaugemeasure discrete ¯ / quantity =loc ¬¬ continuous(intensive/extensive) ground * \array{ && & \rightrightarrows &\dashv& \rightsquigarrow & / & \e & \stackrel{bosonic/fermionic}{} \\ && & \bot && \bot \\ && & \rightsquigarrow &\dashv& \R & = loc_{\mathbb{R}^{0|1}} \\ && & \vee &\stackrel{super}{}& \vee \\ \stackrel{infinitesimal/reduced}{} &\overline{\Re} & / & \Re &\stackrel{}{\dashv}& \Im & & & \\ && & \bot && \bot \\ \stackrel{infinitesimal \atop shape}{} && & \Im &\stackrel{infinitesimal \atop quality}{\dashv}& \& & && \text{étalé} \\ && & \vee && \vee \\ \stackrel{shape}{} && loc_{\mathbb{R}} =& &#643; &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ && & \bot &\stackrel{gauge\;measure}{}& \bot \\ \stackrel{discrete}{} & \overline{\flat} & / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ && & \vee &\stackrel{ground}{}& \vee \\ && & \emptyset &\dashv& \ast & }

Prop. here gives a decomposition of types into their purely even-graded part and their purely fermionic part

e(X) X e(X) X. \array{ && && && \stackrel{}{\e(X)} \\ & & & & & \nearrow_{} && \searrow \\ && && X && && \stackrel{\rightrightarrows}{\e(X)} \\ & & & & & \searrow && \nearrow_{} \\ && && && \stackrel{\rightrightarrows}{X} } \,.

A substance subject to the Pauli exclusion principle given by the above super-grading is yet more rigid than just by the elasticity we had before: it exhibits solidity.


We conclude the process at this point. One may explore it further by continuing it with further resolutions and further oppositions, but for the applications to physics that we consider below the three stages beyond the ground that we have so far turn out to be sufficient.


It is a familiar tought in our age, in view of the intimate relation between physics and mathematics, that theories of physics have a natural mathematical formulation, that it is compelling to consider them also just from within mathematics itself. Famous examples include the formalization of classical mechanics by symplectic geometry, the formalization of Einstein gravity by pseudo-Riemannian geometry/Cartan geometry, the close relation of quantum mechanics and quantum field theory to representation theory (Wigner classification) and more recently the identification of local topological field theory with the theory of symmetric monoidal (infinity,n)-categories.

Hence while mathematics is part of the subjective logic in that it admits the freedom to consider any mathematical structure whatsoever, this suggests to identify among these the “objective” mathematical structures which are theories of physics and as such express a more objective reality than random mathematical structures do.

Classical mechanics (Mechanism)


Given a logic of concepts as above, with its basic constructs of judgements of the form f:XYf \colon X \to Y, among the most natural structures to consider are correspondences, which go from a type X 1X_1 to a type X 2X_2 via an intermediate type YY by maps

Y i o X 1 X 2. \array{ && Y \\ & {}^{\mathllap{i}}\swarrow && \searrow^{\mathrlap{o}} \\ X_1 && && X_2 } \,.

This is the immediate generalization of a relation as we pass from homotopy 0-types to general homotopy types and thereby allow monomorphisms to be replaced by general maps.

Now one observe that a correspondence is naturally interpreted as a process :

every instance/term y:Yy\colon Y may be thought of as a process under which i(y):X 1i(y) \colon X_1 turns into o(y):X 2o(y) \colon X_2.

In traditional mathematical physics this is familiar from the concept of Lagrangian correspondences which serves to encoce much of classical mechanics.

Physical law

Or rather, classical mechanics is encoded by prequantized Lagrangian correspondences, the prequantization expressing the prequantum bundle, an action functional and hence the laws of motion.

By the discussion there, a prequantized Lagrangian correspondence is itself again just a correspondence, but now in context, hence between dependent types, namely depending on a type of phases.

A detailed discussion of how classical field theory is formalized via correspondences in cohesive homotopy type theory in the context of a type of phases is ar

From the dicussion there one finds a picture of sliced correspondences interpreted as classical mechanics as follows.

spaceoftrajectories initialvalues Hamiltonianevolution phasespaceincoming actionfunctional phasespaceoutgoing prequantumbundle in prequantumbundle out 2groupofphases. \array{ && {{space\,of} \atop {trajectories}} \\ & {}^{\mathllap{{initial}\atop {values}}}\swarrow && \searrow^{\mathrlap{{Hamiltonian} \atop {evolution}}} \\ {{phase\,space} \atop {incoming}} && \swArrow_{{action} \atop {functional}} && {{phase\,space} \atop {outgoing}} \\ & {}_{\mathllap{{prequantum}\atop {bundle}_{in}}}\searrow && \swarrow_{\mathrlap{{prequantum} \atop {bundle}_{out}}} \\ && {{2-group} \atop {of\,phases}} } \,.
Quantum mechanics ((quantum-)Chemism)

Recall from remark that the initial opposition gave rise also to the maybe monad, as the negative of the empty moment: ¯=maybe\overline{\empty} = maybe.

The negative of id\id is *\ast.

The opposite of *\ast is \empty.

The negative of \empty is maybemaybe.

While maybemaybe is not idempotent, by remark we may still ask for the types which are pure with respect to it in that they they are objects in its Eilenberg-Moore category. These are precisely the pointed types.

On pointed types the smash product yields a symmetric monoidal structure which is not Cartesian, and we enter the realm of linear type theory in the generality of dependent linear type theory. As discussed there, dependent sum and dependent product here now naturally yield the concept of secondary integral transforms, across correspondences, which in view of the above interpretation of correspondences as spaces of trajectories are really path integrals. Developing this one finds that correspondences in linear homotopy type theory give rise to formalization of quantization and quantum mechanics.

For details see at Quantization via Linear homotopy types.

Boundary conditions (Teleology)

In this context a boundary condition is given by a (prequantized) correspondence which on one end is just the unit type

Y b o * X. \array{ && Y \\ & {}^{\mathllap{b}}\swarrow && \searrow^{\mathrlap{o}} \\ \ast && && X } \,.

For more on this see at

The idea

Including in homotopy type theory the progression of modal operators that we have found above

id id / e bosonic/fermionic solidity R =loc 0|1 rheonomic super infinitesimal/reduced ¯ / elasticity infinitesimalshape infinitesimalquality & étalé shape loc = ʃ quality / ¯ content(flat/rational) cohesion gaugemeasure discrete ¯ / quantity =loc ¬¬ continuous(intensive/extensive) ground * \array{ &&& && & id &\dashv& id \\ &&& && & \vee && \vee \\ &&& && & \rightrightarrows &\dashv& \rightsquigarrow & / & \e & \stackrel{bosonic/fermionic}{} \\ \stackrel{solidity}{} &&& && & \bot && \bot \\ &&& && & \rightsquigarrow &\dashv& \R & = loc_{\mathbb{R}^{0\vert 1}}& & \stackrel{rheonomic}{} \\ &&& && & \vee &\stackrel{super}{}& \vee \\ &&& \stackrel{infinitesimal/reduced}{} &\overline{\Re} & / & \Re &\dashv& \Im & & & \\ \stackrel{elasticity}{} &&& && & \bot && \bot \\ &&& \stackrel{infinitesimal \atop shape}{} && & \Im &\stackrel{infinitesimal \atop quality}{\dashv}& \& & && \text{étalé} \\ &&& && & \vee && \vee \\ &&& \stackrel{shape}{} && loc_{\mathbb{R}} = &&#643; &\stackrel{quality}{\dashv}& \flat & / & \overline{\flat}& \stackrel{content\;(flat/rational)}{} \\ \stackrel{cohesion}{} &&& && & \bot &\stackrel{gauge\;measure}{}& \bot \\ &&& \stackrel{discrete}{} &\overline{\flat} & / & \flat &\stackrel{quantity}{\dashv}& \sharp & = loc_{\not\not} & & \stackrel{continuous\; (intensive/extensive)}{} \\ &&& && & \vee &\stackrel{ground}{}& \vee \\ &&& && & \emptyset &\dashv& \ast & }

makes its term model richer: there are now true propositions and generally terms that may be constructed which are not constructible in plain homotopy type theory. These terms reflect the idea that is induced by these determinations, in that every interpretation of this modal type theory has to realize (externalize) these terms and make these propositions true.

We now indicate some of these new constructions.

Maurer-Cartan forms

Let GG be a an ∞-group type. This means that there is specified a pointed connected type BG\mathbf{B}G and an equivalence GΩBGG\simeq \Omega \mathbf{B}G with its loop space object. We say that BG\mathbf{B}G is the delooping of GG. Notice that all this happens internal to the ambient cohesive homotopy type theory, which makes BG\mathbf{B}G have the interpretation of the moduli ∞-stack of cohesive GG-principal ∞-bundles, instead of just the bare homotopy type of the classifying space

BGʃBG. B G \simeq &#643; \mathbf{B}G \,.

This richer geometric structure is what the boldface in BG\mathbf{B}G is meant to remind us of.


Denote the first and second homotopy fiber of the comparison map B𝔾B𝔾\flat \mathbf{B}\mathbb{G} \to \mathbf{B}\mathbb{G} of the flat moment of this as follows.

Gθ G dRBGBGBG. G \stackrel{\theta_G}{\longrightarrow} \flat_{dR}\mathbf{B}G \longrightarrow \flat \mathbf{B}G \longrightarrow \mathbf{B}G \,.

This double homotopy fiber θ G\theta_G has the interpretation of being the Maurer-Cartan form on GG.

Differential cohomology

Let 𝔾\mathbb{G} be an abelian ∞-group type. The group of phases.

This being abelian just means that there is specified a delooping type B𝔾\mathbf{B} \mathbb{G} and an equivalence 𝔾ΩB𝔾\mathbb{G}\simeq \Omega \mathbf{B} \mathbb{G} with its loop space object, and that with B 0𝔾𝔾\mathbf{B}^0 \mathbb{G} \coloneqq \mathbb{G} we have inductively that B n𝔾\mathbf{B}^n \mathbb{G} is itself equipped with the structure of an abelian ∞-group.

For the present purpose we will assume in addition that 𝔾\mathbb{G} is 0-truncated, which makes it simply an abelian group.


A Hodge filtration is a compatible system of filtrations of B 2𝔾\flat \mathbf{B}^2\mathbb{G} of the form

Ω cl 2 dRB 2𝔾B 2𝔾. \mathbf{\Omega}^{2}_{cl} \to \cdots \to \flat_{dR} \mathbf{B}^2 \mathbb{G} \to \flat \mathbf{B}^2 \mathbb{G} \,.

with 0-truncated extensive Ω cl 2\mathbf{\Omega}^{2}_{cl}.


Given a Hodge filtration, write B𝔾 conn\mathbf{B}\mathbb{G}_{conn} for the homotopy fiber product

B𝔾 connB𝔾× dRB 2𝔾Ω cl 2 \mathbf{B}\mathbb{G}_{conn} \coloneqq \mathbf{B}\mathbb{G}\underset{\flat_{dR}\mathbf{B}^2\mathbb{G}}{\times} \mathbf{\Omega}^2_{cl}

of the Maurer-Cartan form θ B𝔾\theta_{\mathbf{B}\mathbb{G}} with the last Holdge filtration stage.


The decomposition of B𝔾 conn\mathbf{B}\mathbb{G}_{conn} into its (ʃ,¯)(&#643;, \overline{\flat})-moments according to prop reproduces the defining Cartesian sqare of def. :

Ω cl 2 B𝔾 conn dRB 2𝔾 B𝔾 dRB𝔾 B𝔾 \array{ && \mathbf{\Omega}^2_{cl} \\ & \nearrow && \searrow \\ \mathbf{B}\mathbb{G}_{conn} && && \flat_{dR}\mathbf{B}^2\mathbb{G} \\ & \searrow && \nearrow && \searrow \\ && \mathbf{B}\mathbb{G} && && \flat_{dR}B \mathbb{G} \\ && & \searrow && \nearrow \\ && && B \mathbb{G} }
WZW terms

A map

c:BGB p+2𝔾 \mathbf{c} \colon \mathbf{B}G \longrightarrow \mathbf{B}^{p+2} \mathbb{G}

is equivalently a cocycle of degree p+2p+2 in the group cohomology of GG.


Given a group cocycle c\mathbf{c} and a Hodge filtration, then a refinement of the Hodge filtration along the group cocycle is a chose of 0-trucated extensive Ω flat 1(,𝔤)\mathbf{\Omega}^1_{flat}(-,\mathfrak{g}) fitting into a square

Ω flat 1(,𝔤) μ Ω cl 2 dRBG dRc dRB 2𝔾. \array{ \mathbf{\Omega}^1_{flat}(-,\mathfrak{g}) &\stackrel{\mu}{\longrightarrow}& \mathbf{\Omega}^2_{cl} \\ \downarrow && \downarrow \\ \flat_{dR} \mathbf{B}G &\stackrel{\flat_{dR}\mathbf{c}}{\longrightarrow}& \flat_{dR} \mathbf{B}^2 \mathbb{G} } \,.

Given this, write

G˜G× dRBGΩ flat 1(,𝔤) \tilde G \coloneqq G \underset{\flat_{dR}\mathbf{B}G}{\times} \mathbf{\Omega}^1_{flat}(-,\mathfrak{g})

For GG 0-truncated, then the canonical choice is Ω flat 1(,𝔤)= dRBG\mathbf{\Omega}^1_{flat}(-,\mathfrak{g}) = \flat_{dR}\mathbf{B}G. With this one has G˜G\tilde G \simeq G.

On the other extreme, for G=B p+1𝔾G = \mathbf{B}^{p+1}\mathbb{G} then the canonical choice is Ω flat 1(,𝔤)=Ω cl p+2\mathbf{\Omega}^1_{flat}(-,\mathfrak{g}) = \mathbf{\Omega}^{p+2}_{cl}. With this one has G˜B p+1𝔾 conn\tilde G \simeq \mathbf{B}^{p+1}\mathbb{G}_{conn}.

This means that in general G˜\tilde G is a homotopy fiber product of GG with B p+1𝔾 conn\mathbf{B}^{p+1}\mathbb{G}_{conn}, hence that a map to out of some Σ\Sigma is a pair of a map ΣG\Sigma \to G and of (p+1)(p+1)-form data on Σ\Sigma. This is the kind of field content of higher gauged WZW models.


Given a group cocycle c:BGB p+2\mathbf{c} \colon \mathbf{B}G \to \mathbf{B}^{p+2} and a form refinement μ\mu as in def. , then there exists an essentially unique prequantization

L WZW:G˜B conn p+1 \mathbf{L}_{WZW} \;\colon\; \tilde G \longrightarrow \mathbf{B}^{p+1}_{conn}

of μ(θ G)\mu(\theta_G) whose underlying B p𝔾\mathbf{B}^p\mathbb{G}-principal ∞-bundle is Ωc\Omega \mathbf{c}.

We call this the WZW term whose curvature is μ(θ G)\mu(\theta_G).


See also at geometry of physics – manifolds and orbifolds.


Given X,YHX,Y\in \mathbf{H} then a morphism f:XYf \;\colon\; X\longrightarrow Y is a local diffeomorphism if its naturality square of the infinitesimal shape modality

X X f f Y Y \array{ X &\longrightarrow& \Im X \\ \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{\Im f}} \\ Y &\longrightarrow& \Im Y }

is a pullback square.


The abstract definition comes down to being the appropriate synthetic differential supergeometry-version of the traditional statement that ff is a local diffeomorphism if the diagram of tangent bundles

TX X Tf f TY Y \array{ T X &\longrightarrow& X \\ \downarrow^{\mathrlap{T f}} && \downarrow^{\mathrlap{f}} \\ T Y &\longrightarrow& Y }

To see this, notice by the discussion at synthetic differential geometry that for DD an infinitesimally thickened point, then for any XHX \in \mathbf{H} the mapping space [D,X][D,X] is the jet bundle of XX with jets of order as encoded by the infinitesimal order of DD. In particular if 𝔻 1(1)\mathbb{D}^1(1) is the first order infinitesimal interval defined by the fact that its algebra of functions is the algebra of dual numbers C (𝔻 1(1))=(ϵ)/(ϵ 2)C^\infty(\mathbb{D}^1(1)) = (\mathbb{R} \oplus \epsilon \mathbb{R})/(\epsilon^2), and XX is a smooth manifold, then

[𝔻 1(1),X]TX [\mathbb{D}^1(1), X]\simeq T X

is the ordinary tangent bundle of XX. Now use that the internal hom [D,][D,-] preserves limits in its second argument, and that, by the hom-adjunction, H(U,[D,X])H(U×D,X)\mathbf{H}(U, [D,X]) \simeq \mathbf{H}(U \times D, X) and finally use that H(U×D,X)H((U×D),X)H(U,X)\mathbf{H}(U \times D, \Im X)\simeq \mathbf{H}(\Re(U \times D), X)\simeq \mathbf{H}(U,X).

Let now VHV \in \mathbf{H} be given, equipped with the structure of a group (infinity-group).


A VV-manifold is an XHX \in \mathbf{H} such that there exists a VV-atlas, namely a correspondence of the form

U V X \array{ && U \\ & \swarrow && \searrow \\ V && && X }

with both morphisms being local diffeomorphisms, def. , and the right one in addition being an epimorphism, hence an atlas.


If f:XYf \;\colon\; X \longrightarrow Y is a local diffeomorphism, def. , then so is image f:XY\stackrel{\rightsquigarrow}{f}\colon \stackrel{\rightsquigarrow}{X} \longrightarrow \stackrel{\rightsquigarrow}{Y} under the bosonic modality.


Since the bosonic modality provides Aufhebung for \Re\dashv \Im we have \rightsquigarrow \Im \simeq \Im. Moreover \Im \rightsquigarrow \simeq \Im anyway. Finally \rightsquigarrow preserves pullbacks (being in particular a right adjoint). Hence hitting a pullback diagram

X X f f Y Y \array{ X &\longrightarrow& \Im X \\ \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{\Im f}} \\ Y &\longrightarrow& \Im Y }

with \rightsquigarrow\;\; yields a pullback diagram

X X f f Y Y \array{ \stackrel{\rightsquigarrow}{X} &\longrightarrow& \Im \stackrel{\rightsquigarrow}{X} \\ \downarrow^{\mathrlap{\stackrel{\rightsquigarrow}{f}}} && \downarrow^{\mathrlap{\Im \stackrel{\rightsquigarrow}{f}}} \\ \stackrel{\rightsquigarrow}{Y} &\longrightarrow& \Im \stackrel{\rightsquigarrow}{Y} }

The bosonic space X\stackrel{\rightsquigarrow}{X} underlying a VV-manifold XX, def. , is a V\stackrel{\rightsquigarrow}{V}-manifold

Frame bundles

Given XHX \in \mathbf{H}, its infinitesimal disk bundle T infXXT_{inf} X\to X is the pullback of the unit of the infinitesimal shape modality along itself

T infX X X X. \array{ T_{inf} X &\stackrel{}{\longrightarrow}& X \\ \downarrow && \downarrow \\ X &\longrightarrow& \Im X } \,.

Given a point x:*Xx \;\colon\; \ast \to X, then the infinitesimal neighbourhood *𝔻 xX\ast \to \mathbb{D}_x \to X of that point is the further pullback of the infinitesimal disk bundle to this point:

𝔻 x T infX X * x X X. \array{ \mathbb{D}_x &\longrightarrow & T_{inf} X &\stackrel{}{\longrightarrow}& X \\ \downarrow && \downarrow && \downarrow \\ \ast &\stackrel{x}{\longrightarrow} & X &\longrightarrow& \Im X } \,.

More generally, for kk \in \mathbb{N} then the kkth order infinitesimal disk bundle is

T (k)X (k)X X X \array{ T_{(k)} X &\stackrel{}{\longrightarrow}& \Im_{(k)} X \\ \downarrow && \downarrow \\ X &\longrightarrow& \Im X }

and accordingly the kkth order infinitsimal neighbourhood is

𝔻(k) x T (k)X (k)X * x X X. \array{ \mathbb{D}(k)_x &\longrightarrow & T_{(k)} X &\stackrel{}{\longrightarrow}& \Im_{(k)}X \\ \downarrow && \downarrow && \downarrow \\ \ast &\stackrel{x}{\longrightarrow} & X &\longrightarrow& \Im X } \,.

It is natural not to pick any point, but to collect all infinitesimal disks around all the points of a space:


The relative flat modality is the operation rel\flat^{rel} that sends XHX \in \mathbf{H} to the homotopy pullback

rel X X X. \array{ \flat^{rel} &\longrightarrow& X \\ \downarrow && \downarrow \\ \flat X &\longrightarrow& \Im X } \,.

More generally, for any kk \in \mathbb{N} then the order kk relative flat modality is the pullback in

(k) rel (k)X X X. \array{ \flat^{rel}_{(k)} &\longrightarrow& \Im_{(k)} X \\ \downarrow && \downarrow \\ \flat X &\longrightarrow& \Im X } \,.

The general linear group GL(V)GL(V) is the automorphism infinity-group of the infinitesimal neighbourhood 𝔻 e V\mathbb{D}^V_e, def. , of the neutral element e:*𝔻 e VVe \colon \ast \to \mathbb{D}^V_e \to V:

GL(V)Aut(𝔻 e V). GL(V) \coloneqq \mathbf{Aut}(\mathbb{D}^V_e) \,.

For XX a VV-manifold, def. , then its infinitesimal disk bundle T infXXT_{inf} X \to X, def. , is associated to a GL(V)GL(V)-principal Fr(X)XFr(X) \to X – to be called the frame bundle, modulated by a map to be called τ X\tau_X, producing homotopy pullbacks of the form

T infX V/GL(V) X τ X BGL(V)Fr(X) * X τ X BGL(V). \array{ T_{inf} X &\longrightarrow& V/GL(V) \\ \downarrow && \downarrow \\ X &\stackrel{\tau_X}{\longrightarrow}& \mathbf{B} GL(V) } \;\;\; \array{ Fr(X) &\longrightarrow& \ast \\ \downarrow && \downarrow \\ X &\stackrel{\tau_X}{\longrightarrow}& \mathbf{B} GL(V) } \,.

A framing of a VV-manifold is a trivialization of its frame bundle, prop. , hence a diagram in H\mathbf{H} of the form

X * BGL(V) \array{ X && \longrightarrow && \ast \\ & \searrow &\swArrow& \swarrow \\ && \mathbf{B}GL(V) }

It is useful to express def. in terms of the slice topos H /BGL(V)\mathbf{H}_{/\mathbf{B}GL(V)}. Write VFrameH /BGL(V)V\mathbf{Frame}\in \mathbf{H}_{/\mathbf{B}GL(V)} for the canonical morphism *BGL(V)\ast \to \mathbf{B}GL(V) regarded as an object in the slice. Then a framing as in def. is equivalently a morphism

ϕ:τ XVFrame \phi \colon \tau_X \longrightarrow V\mathbf{Frame}

in H /BGL(V)\mathbf{H}_{/\mathbf{B}GL(V)}.


The group object VV, canonically regarded as a VV-manifold, carries a canonical framing, def. , ϕ li\phi_{li}, induced by left translation.


See also at geometry of physics – G-structure and Cartan geometry.


Given a homomorphism of groups GGL(V)G \longrightarrow GL(V), a G-structure on a VV-manifold XX is a lift c\mathbf{c} of the frame bundle τ X\tau_X of prop. through this map

X G τ X BGL(V). \array{ X && \stackrel{}{\longrightarrow} && G \\ & {}_{\mathllap{\tau_X}}\searrow &\swArrow& \swarrow \\ && \mathbf{B}GL(V) } \,.

As in remark , it is useful to express def. in terms of the slice topos H /BGL(V)\mathbf{H}_{/\mathbf{B}GL(V)}. Write GStrucH /BGL(V)G\mathbf{Struc}\in \mathbf{H}_{/\mathbf{B}GL(V)} for the given map BGBGL(V)\mathbf{B}G\to \mathbf{B}GL(V) regarded as an object in the slice. Then a GG-structure according to def. is equivalently a choice of morphism in H /BGL(V)\mathbf{H}_{/\mathbf{B}GL(V)} of the form

c:τ XGStruc. \mathbf{c} \;\colon\; \tau_X \longrightarrow G\mathbf{Struc} \,.

In other words, GStrucH /BGL(v)G\mathbf{Struc} \in \mathbf{H}_{/\mathbf{B}GL(v)} is the moduli stack for GG-structures.


A choice of framing ϕ\phi, def. , on a VV-manifold XX induces a G-structure for any GG, given by the pasting diagram in H\mathbf{H}

X * BGL(V) \array{ X &\longrightarrow& \ast &\longrightarrow& \\ & \searrow & \downarrow & \swarrow \\ && \mathbf{B}GL(V) }

or equivalently, via remark and remark , given as the composition

c li:τ XϕVFrameGStruc. \mathbf{c}_{li} \;\colon\; \tau_X \stackrel{\phi}{\longrightarrow} V\mathbf{Frame} \longrightarrow G\mathbf{Struc}\,.

We call this the left invariant GG-structure.


For XX a VV-manifold, then a G-structure on XX, def. , is integrable if for any VV-atlas VUXV \leftarrow U \rightarrow X the pullback of the GG-structure on XX to VV is equivalent there to the left-inavariant GG-structure on VV of example , i.e. if we have an correspondence in the double slice topos (H /BGL(V)) /GStruc(\mathbf{H}_{/\mathbf{B}GL(V)})_{/G\mathbf{Struc}} of the form

τ U τ V τ X c li c GStruc. \array{ && \tau_U \\ & \swarrow && \searrow \\ \tau_V && \swArrow && \tau_X \\ & {}_{\mathllap{\mathbf{c}_{li}}}\searrow && \swarrow_{\mathrlap{\mathbf{c}}} \\ && G \mathbf{Struc} } \,.

The GG-structure is infintesimally integrable if this holds true after restriction along the relative shape modality relUU\flat^{rel} U \to U, def. , to all the infinitesimal disks in UU:

τ relU τ V τ X c li c GStruc. \array{ && \tau_{\flat^{rel}U} \\ & \swarrow && \searrow \\ \tau_V && \swArrow && \tau_X \\ & {}_{\mathllap{\mathbf{c}_{li}}}\searrow && \swarrow_{\mathrlap{\mathbf{c}}} \\ && G \mathbf{Struc} } \,.

Finally, the GG-structure is order kk infinitesimally integrable if this holds for the order-kk relative shape modality (k) rel\flat^{rel}_{(k)}.


Consider an infinity-action of GL(V)GL(V) on VV which linearizes to the canonical GL(V)GL(V)-action on 𝔻 e V\mathbb{D}^V_e by def. . Form the semidirect product GL(V)VGL(V) \rtimes V. Consider any group homomorphism GGL(V)G\to GL(V).

A (GGV)(G\to G\rtimes V)-Cartan geometry is a VV-manifold XX equipped with a GG-structure, def. . The Cartan geometry is called (infinitesimally) integrable if the GG-structure is so, according to def. .


For VV an abelian group, then in traditional contexts the infinitesimal integrability of def. comes down to the torsion of a G-structure vanishing. But for VV a nonabelian group, this definition instead enforces that the torsion is on each infinitesimal disk the intrinsic left-invariant torsion of VV itself.

Traditionally this is rarely considered, matching the fact that ordinary vector spaces, regarded as translation groups VV, are abelian groups. But super vector spaces regarded (in suitable dimension) as super translation groups are nonabelian groups. Therefore super-vector spaces VV may carry intrinsic torsion, and therefore first-order integrable GG-structures on VV-manifolds are torsion-ful.

Indeed, this is a phenomenon known as the torsion constraints in supergravity. Curiously, as discussed there, for the case of 11-dimensional supergravity the equations of motion of the gravity theory are equivalent to the super-Cartan geometry satisfying this torsion constraint. This way super-Cartan geometry gives a direct general abstract route right into the heart of M-theory.

Definite forms

Given a group cocycle c:BGB p+2𝔾\mathbf{c} \colon \mathbf{B}G\to\mathbf{B}^{p+2}\mathbb{G} with WZW term, prop. , of the form

L WZW V:VB p+1𝔾 \mathbf{L}_{WZW}^V \colon V \longrightarrow \mathbf{B}^{p+1}\mathbb{G}

and given a VV-manifold XX we say that an integrable globalization of L WZW V\mathbf{L}_{WZW}^V over XX is a WZW on on XX

L WZW X:XB p+1𝔾 conn \mathbf{L}_{WZW}^X \;\colon\;X \longrightarrow \mathbf{B}^{p+1}\mathbb{G}_{conn}

such that there is a VV-atlas for XX

U V X \array{ && U \\ & \swarrow && \searrow \\ V && && X }

which extends to a correspondence between L WZW\mathbf{L}_{WZW} and L WZW X\mathbf{L}_{WZW}^X

U V X L WZW V L WZW X B p+1𝔾 conn. \array{ && U \\ & \swarrow && \searrow \\ V && \swArrow && X \\ & {}_{\mathllap{\mathbf{L}_{WZW}^V}}\searrow && \swarrow_{\mathrlap{\mathbf{L}_{WZW}^X}} \\ && \mathbf{B}^{p+1}\mathbb{G}_{conn} } \,.

Accordingly, as in def. we say that L WZW X\mathbf{L}_{WZW}^X is an infinitesimally integrable globalization if this correspondence exists after restriction along the inclusion relUU\flat^{rel} U \to U of the infinitesimal disks in XX and such that

  1. the induced section of the associated [𝔻(1) V,B p+1𝔾 conn][\mathbb{D}(1)^V,\mathbf{B}^{p+1}\mathbb{G}_{conn}]-fiber infinity-bundle is definite on the restriction L WZW 𝔻\mathbf{L}_{WZW}^{\mathbb{D}} of L WZW V\mathbf{L}_{WZW}^V to the infinitesimal disk;

  2. also the underlying cocycle is definite, in that the infinitesimal disk bundle lifts to an 𝔻 V(1)\mathbb{D}^V(1)-gerbe (for the induced group structure on 𝔻 V(1)\mathbb{D}^V(1)).

If B p+1𝔾 conn\mathbf{B}^{p+1}\mathbb{G}_{conn} had no higher gauge transformations, then this would already ensure that such a globalization globalizes L WZW V\mathbf{L}_{WZW}^V locally cohesively, but here in higher differential geometry this property becomes genuine structure and hence we need to demand it. There is an axiomatic way to say this (see dcct for details) and if this is imposed then we say that L WZW X\mathbf{L}_{WZW}^X is a definite globalization of L WZW V\mathbf{L}_{WZW}^V.


There is a canonical (∞,1)-functor from (infinitesimally integrable) definite globalizations of L WZW X\mathbf{L}_{WZW}^X over a VV-manifold XX to (infinitesimally integrable) GG-structures on XX, def. , for

G=intens(Stab GL(V)(L WZW 𝔻 V)) G = intens(\mathbf{Stab}_{GL(V)}(\mathbf{L}_{WZW}^{\mathbb{D}^V}))

the intensification (in the sense above) of the stabilizer ∞-group of the restriction of L WZW V\mathbf{L}_{WZW}^V along the inclusion of the typical infinitesimal disk 𝔻 VV\mathbb{D}^V \to V.


Given a theory of physics, made sufficiently precise in formal logic, then an interpretation of the theory by a model “is” nature as predicted by this theory.

For instance if we considered Einstein gravity to be the theory of pseudo-Riemannian manifolds subject to some energy condition, then a model for this theory is one concrete particular spacetime.

Above we saw that cohesive (elastic) homotopy type theory contains Cartan geometry, hence in particular pseudo-Riemannian geometry in its idea, as well as gauge theory and hence we accordingly find models of nature here.

Recall specifically that

  1. From prop. we have that group cocycles c:BVB p+2𝔾\mathbf{c}\colon \mathbf{B}V \longrightarrow \mathbf{B}^{p+2}\mathbb{G} of degree p+2p+2 induce WZW terms in that degree and hence the WZW sigma model prequantum field theory on the worldvolume of a p-brane propagating on the “model spacetimeVV.

  2. A second cocycle on the infinity-group extension classified by c\mathbf{c} yields a type of p˜\tilde p-brane on which these pp-branes may end;

  3. This structure is naturally generalized to VV-manifolds XX equipped with definite globalizations of these WZW terms, defining pp-branes propagating on XX.

  4. The definite globalization of the WZW term L WZW\mathbf{L}_{\mathrm{WZW}} induces a Stab(L WZW)Stab(\mathbf{L}_{WZW}) structure on XX and the requirement that this be infinitesimally integrable is a torsion constraint on XX.

We now find an externalization of the idea such that

  1. There is a canonical bouquet of higher group cocycles and their ∞-group extensions emanating from the unique 0-truncated purely fermionic type – the superpoint.

  2. The resulting branes and their intersection laws are those seen in string theory;

  3. The resulting spacetimes are superspacetimes as in the relevant supergravity theories;

  4. The resulting torsion constraints, namely the supergravity torsion constraints, imply, in the maximally extended situation, the Einstein equations of motion of 11-dimensional supergravity, specifically of d=4 N=1 supergravity arising in the guise of M-theory on G2-manifolds.

This is a “theory of everything” in the sense of modern fundamental physics, which is beeing argued to have viable phenomenology, see at G2-MSSM for more on this. Even if it turns out that there are no models in this theory which match quantitative measurements in experiment, it is noteworthy that the qualitative structure of this theory is that of Einstein-Yang-Mills-Dirac-Higgs theory and hence matches faithfully the qualitative features of nature that is in experiment. Given our starting point above this is maybe not to be lightly dismissed.


The cohesive+elastic+solid homotopy type theory above has a faithful (i.e. non-degenerate) categorical semantics in the homotopy topos SuperFormalSmoothGrpdSuperFormalSmooth\infty Grpd of super formal smooth infinity-groupoids.

We now spell out the construction of this model and indicate the proof of this statement.



There are then “semidirect product” sites CartSpInfinPointCartSp \rtimes InfinPoint and CartSpSuperPointCartSp \rtimes SuperPoint (whose objects are Cartesian products of the given form inside synthetic differential supergeometry and whose morphisms are all morphisms in that context (not just the product morphisms)).

Set then

SmoothGrpdSh (CartSp) Smooth \infty Grpd \coloneqq Sh_\infty(CartSp)

for the collection of smooth ∞-groupoids;

FormalSmoothGrpdSh (CartSpInfPoint) FormalSmooth\infty Grpd \coloneqq Sh_\infty(CartSp \rtimes InfPoint)

for the collection of formal smooth ∞-groupoids (see there) and finally

SuperFormalSmoothGrpdSh (CartSpSuperPoint) SuperFormalSmooth\infty Grpd \coloneqq Sh_\infty(CartSp \rtimes SuperPoint)

for that of super formal smooth ∞-groupoids.


The sites in question are alternatingly (co-)reflective subcategories of each other (we always display left adjoints above their right adjoints)

*CartSpCartSpInfPointCartSpSuperPoint. \ast \stackrel{\longleftarrow}{\hookrightarrow} CartSp \stackrel{\hookrightarrow}{\longleftarrow} CartSp\rtimes InfPoint \stackrel{\longleftarrow}{\stackrel{\hookrightarrow}{\longleftarrow}} CartSp \rtimes SuperPoint \,.


Passing to (∞,1)-categories of (∞,1)-sheaves, this yields, via (∞,1)-Kan extension, a sequence of adjoint quadruples as follows:

Δ: Grpd SmoothGrpd FormalSmoothGrpd SuperFormalSmoothGrpd \array{ & && && &\longleftarrow& \\ & && &\hookrightarrow& &\hookrightarrow& \\ & &\longleftarrow& &\longleftarrow& &\longleftarrow& \\ \Delta \colon & \infty Grpd &\hookrightarrow& Smooth \infty Grpd &\hookrightarrow& FormalSmooth \infty Grpd &\hookrightarrow& SuperFormalSmooth \infty Grpd \\ & &\longleftarrow& &\longleftarrow& \\ & &\hookrightarrow& }

the total composite labeled Δ\Delta is indeed the locally constant infinity-stack-functor.

Forming adjoint triples from these adjoint quadruples gives idempotent (co-)monads

ʃ* &#643; \dashv \flat \dashv \ast
& \Re \dashv \Im \dashv \&
\rightrightarrows \dashv \rightsquigarrow \dashv \Re

satisfying the required inclusions of their images.


All the sites are ∞-cohesive sites, which gives that we have an cohesive (infinity,1)-topos. The composite inclusion on the right is an ∞-cohesive neighbourhood site, whence the inclusion SmoothGpdSuperFormalSmoothGrpdSmooth\infty Gpd\hookrightarrow SuperFormalSmooth\infty Grpd exhibits differential cohesion.

With this the rightmost adjoint quadruple gives the Aufhebung of \Re \dashv \Im by R\rightsquigarrow \dashv \R and the further opposition \rightrightarrows \dashv \rightsquigarrow.


The model in def. admits also the refinement of the infinitesimal shape modality to an infinite tower

ʃ<= ()<< (3)< (2)< (1)<id &#643; \lt \Im = \Im_{(\infty)} \lt \cdots \lt \Im_{(3)} \lt \Im_{(2)} \lt \Im_{(1)} \lt id

characterizing kkth order infinitesimals. Let

*=InfPoint (0)InfPoint (1)InfPoint (2)InfPoint (3)InfPoint \ast = InfPoint_{(0)} \hookrightarrow InfPoint_{(1)} \hookrightarrow InfPoint_{(2)} \hookrightarrow InfPoint_{(3)} \hookrightarrow \cdots InfPoint

be the stratification of InfPointInfPoint by its full subcategories on those objects whose coresponding Weil algebras/local Artin algebras are of the form V\mathbb{R} \oplus V with V k=0V^k = 0. Each of these inclusions has coreflection, given by projection onto the quotient by the ideal V kV^k, as kk ranges


The model in def. verifies the required determinate negations

  1. determinate negations I:

    • ʃ**&#643; \ast \simeq \ast;

    • ʃ\flat \to &#643; is epi restricted to 0-types;

  2. determinate negations II:

    • ʃloc &#643; \simeq loc_{\mathbb{R}} for SmoothMfdSuperFormalSmoothGrpd\mathbb{R} \in SmoothMfd \hookrightarrow SuperFormalSmooth\infty Grpd the ordinary real line;

    • Rloc 0|1\R \simeq loc_{\mathbb{R}^{0|1}} for 0|1SuperMfdSuperFormalSmoothGrpd\mathbb{R}^{0|1} \in SuperMfd \hookrightarrow SuperFormalSmooth\infty Grpd the odd line.


The first two items follow with the discussion at ∞-cohesive site. The second two by dcct, prop. 5.2.51.


The model in def. verfies the required Aufhebungen

  1. \sharp \emptyset \simeq \emptyset;

  2. \rightsquigarrow \Im \simeq \Im.


For the statement \sharp \emptyset \simeq \emptyset consider the following:

Since the site SS of HSuperFormalSmoothGrpds\mathbf{H} \coloneqq SuperFormalSmooth\infty Grpds has a terminal object *\ast, it follows that for XHX\in \mathbf{H} any sheaf X:𝒮 opSetX \colon \mathcal{S}^{op}\to Set then

XX(*) \flat X \simeq X(\ast)

(where we may leave the constant re-embedding implicit, due to it being fully faithful).

Moreover, for every object U𝒮U\in \mathcal{S} there exists a morphism i:*Ui \colon \ast \to U hence for every XHX\in \mathbf{H} and every UU there exists a morphism i *:X(U)Xi^\ast \colon X(U)\to \flat X. This means that if X\flat X \simeq \emptyset then X(U)X(U) \simeq \emptyset for all U𝒮U \in \mathcal{S} and hence XX\simeq \emptyset.

We now show that this condition is equivalent to the required Aufhebung:

Generally, given a topos equipped with a level of a topos given by an adjoint modality ()()(\Box\dashv \bigcirc) \coloneqq (\flat \dashv \sharp), then the condition \sharp \emptyset \simeq \emptyset is equivalent to (X)(X)(\flat X \simeq \emptyset) \Leftrightarrow (X \simeq \emptyset).

Because: in a topos the initial object \emptyset is a strict initial object, and hence (X)(X)(X \simeq \emptyset) \simeq (X \to \emptyset). Therefore in one direction, assuming \sharp \emptyset \simeq \emptyset then

(X) (X) (X) (X) (X). \begin{aligned} (X \simeq \emptyset) & \simeq (X \to \emptyset) \\ & \simeq (X \to \sharp \emptyset) \\ & \simeq (\flat X \to \emptyset) \\ & \simeq (\flat X \simeq \emptyset) \end{aligned} \,.

Conversely, assuming that (X)(X)(\flat X \simeq \emptyset) \Leftrightarrow (X \simeq \emptyset), then for all XX

(X) (X) (X) (X) (X) \begin{aligned} (X\to \emptyset) & \simeq (X\simeq \emptyset) \\ & \simeq (\flat X \simeq \emptyset) \\ & \simeq (\flat X \to \emptyset) \\ & \simeq (X\to \sharp \emptyset) \end{aligned}

and hence by the Yoneda lemma \emptyset \simeq \sharp \emptyset.


Second, for the statement \rightsquigarrow \Im \simeq \Im consider the following:

For any XHX \in \mathbf{H} and any U×D sCartSpSuperInfPointHU \times D_s\in CartSp \rtimes SuperInfPoint \hookrightarrow \mathbf{H} we have by adjunction natural equivalences

H(U×D s,X) H(U×D s,X) H((U×D s),X) H(U,X) H((U×D s),X) H(U×D s,X). \begin{aligned} \mathbf{H}(U \times D_s , \stackrel{\rightsquigarrow}{\Im X}) & \simeq \mathbf{H}(\stackrel{\rightrightarrows}{U \times D_s} , \Im X) \\ &\simeq \mathbf{H}(\Re(\stackrel{\rightrightarrows}{U \times D_s}) , X) \\ & \simeq \mathbf{H}(U, X) \\ & \simeq \mathbf{H}(\Re(U \times D_s), X) \\ & \simeq \mathbf{H}(U \times D_s, \Im X) \end{aligned} \,.

Here the crucial step is the observation that on representables, by construction, the reduced part of the even part is the reduced part of the original object.

But observe that


While, due to prop. , in the model of def.

  • the opposition ʃ&#643; \dashv \sharp has determinate negation in the sense of def. ;

on the other hand

  • the opposition \rightrightarrows \dashv \rightsquigarrow does not have definite negation in the sense of def. .

The definition would require that

0|2 0|2 \stackrel{\rightsquigarrow}{\mathbb{R}^{0|2}} \longrightarrow \stackrel{\rightrightarrows}{\mathbb{R}^{0|2}}

is an epimorphism. But this is equivalent to the point inclusion

*𝔻(1) \ast \longrightarrow \mathbb{D}(1)

into the formal dual of the algebra of dual numbers.


We discuss now how in the externalization of the theory given by theorem there naturally appears spacetime from the idea.

The progressive system of moments above, yields, by prop. , two god-given objects:

real linesuperpoint
= 1|0\mathbb{R} = \mathbb{R}^{1\vert 0} 0|1\mathbb{R}^{0\vert 1}
ʃloc &#643; \simeq loc_{\mathbb{R}}Rloc 0|1\R \simeq loc_{\mathbb{R}^{0\vert 1}}

Both have familiar structure of an abelian group object, \mathbb{R} being the additive group, hence there are arbitrary deloopings B n 0|1\mathbf{B}^n \mathbb{R}^{0|1} and B n\mathbf{B}^{n}\mathbb{R}.

Given two types, there are the judgements in which these appear as subject and as predicate, in the sense discussed above.

There are no non-trivial judgements with (a delooping of) \mathbb{R} as the subject and (a delooping of) 0|1\mathbb{R}^{0|1} as the predicate. But there turn out to be some exceptional judgements with subject 0|q\mathbb{R}^{0|q} and predicate B d\mathbf{B}^d \mathbb{R}.

By example this leads to the deduction of the object which is the homotopy fibers of the corresponding maps. From these one obtains further judgements, then further objects, and so forth. This way a “bouquet” of objects is induced from the initial ones.

We now discuss how this bouquet first of all yields super Minkowski spacetime (Huerta-Schreiber 17) and then further the extended super Minkowski spacetimes arising from super p-brane condensates (FSS).

Minkowski spacetime

Consider first the superpoint 0|1\mathbb{R}^{0|1}.


This is the unique 0-truncated object which is

  1. purely negative to bosonic moment;

  2. purely opposite to bosonic moment;

in that

e( 0|1) 0|1 \e(\mathbb{R}^{0|1})\simeq \mathbb{R}^{0|1}
0|1*. \stackrel{\rightrightarrows}{\mathbb{R}^{0|1}} \simeq \ast \,.

Since 0|1\mathbb{R}^{0|1} (and the other objects obtained in a moment) are contractible as super Lie groups, we may use the van Est isomorphism to conveniently discuss them as super Lie algebras. Regarding 0|1\mathbb{R}^{0\vert 1} as a super Lie algebra, then its Chevalley-Eilenberg algebra is freely generated from a (1,odd)(1,odd)-bigraded element dθd\theta

CE( 0|1)=( dθ,d CE=0). CE(\mathbb{R}^{0\vert 1}) = \left( \wedge^\bullet \langle d\theta \rangle, d_{CE} = 0 \right) \,.

It is evident that


The second super Lie algebra cohomology of 0|1\mathbb{R}^{0\vert 1} is

H 2( 0|1,)= H^{2}(\mathbb{R}^{0\vert 1}, \mathbb{R}) = \mathbb{R}

represented by the 2-cocycles of the form

dθdθCE( 0|1). d\theta\wedge d\theta \in CE(\mathbb{R}^{0\vert 1}) \,.

The Lie algebra extension

1|1 0|1 B 1 \array{ \mathbb{R}^{1|\mathbf{1}} \\ \downarrow \\ \mathbb{R}^{0|1} &\stackrel{}{\longrightarrow}& \mathbf{B}^1 \mathbb{R} }

classified by this is the super translation group in 1-dimension.

This is the worldline of the superparticle.

There are no further non-trivial cocycles here giving further extensions.

Hence next consider the Cartesian product of the initial superpoint with itself.

0|2= 0|1× 0|1. \mathbb{R}^{0|2} = \mathbb{R}^{0|1}\times \mathbb{R}^{0|1} \,.

This is still purely of negative bosonic moment in that e( 0|2) 0|2e(\mathbb{R}^{0|2}) \simeq \mathbb{R}^{0|2}, but it no longer has purely no moment opposed to bosonic moment (witnessing that the fermionic opposition is not complete, lemma ), instead

0|2𝔻(1) \stackrel{\rightrightarrows}{\mathbb{R}^{0|2}} \simeq \mathbb{D}(1)

is the first-order infinitesimal interval (the formal dual of the “algebra of dual numbers”).


The second super Lie algebra cohomology of 0|2\mathbb{R}^{0\vert 2} is

H 2( 0|2,) 3 H^2(\mathbb{R}^{0\vert 2}, \mathbb{R}) \simeq \mathbb{R}^3

represented by the cocycles of the form

a 11dθ 1dθ 1+a 22dθ 2dθ 2+a 12dθ 1dθ 2. a_{11} \, d\theta_1 \wedge d\theta_1 + a_{22} \, d\theta_2 \wedge d\theta_2 + a_{12} \, d\theta_1 \wedge d\theta_2 \,.

The extension classified by this

2,1|2 0|2 B 3 \array{ \mathbb{R}^{2,1|\mathbf{2}} \\ \downarrow \\ \mathbb{R}^{0|2} &\stackrel{}{\longrightarrow}& \mathbf{B} \mathbb{R}^3 }

is 3-dimensional super Minkowski spacetime.


This follows by inspection of the real spin representations in dimension 3, see the details spelled out at spin representation – via division algebras – Example d=3).

For more on this see at geometry of physics – supersymmetry the section Supersymmetry from the Superpoint.

Now the old brane scan gives:


The Spin(2,1)Spin(2,1)-invariant third Lie algebra cohomology of 3d Minkowski super-spacetime is

H 3( 2,1|2) Spin(2,1)= H^3(\mathbb{R}^{2,1\vert \mathbf{2}})^{Spin(2,1)} = \mathbb{R}

represented by the 3-cocycle which, as a left invariant super differential form on 2,1|2\mathbb{R}^{2,1\vert \mathbf{2}} is the WZW term in the Green-Schwarz action functional for the super 1-brane in 3d.

𝔰𝔱𝔯𝔦𝔫𝔤 hetonG 2 2,1|2 B 2 \array{ \mathfrak{string}_{het \, on \, G_2} \\ \downarrow \\ \mathbb{R}^{2,1\vert \mathbf{2}} &\stackrel{}{\longrightarrow}& \mathbf{B}^2 \mathbb{R} }

A definite globalization, of this 3-cocycle over a 3|2\mathbb{R}^{3\vert \mathbf{2}}-manifold requires, by def. , that the tangent bundle is a bundle of super Lie algebras and that the cocycle extends to a definite form. This imposes G-structure for GG the Lorentz group (or rather its spin group double cover).


The joint stabilizer of GL( 2,1|2)GL(\mathbb{R}^{2,1\vert 2}) of the Lie bracket and the 3-cocycle is the pin group Pin(2,1)Pin(2,1), the unoriented generalization of the spin group Spin(2,1)Spin(2,1), the double cover of the Lorentz group SO(2,1)SO(2,1).

This is one special case of a more general statement which we come to as prop. below.

Consider then 2,1|4\mathbb{R}^{2,1\vert 4}

2,1|4 0|2 0|2 B 3. \array{ && \mathbb{R}^{2,1\vert 4} \\ & \swarrow && \searrow \\ \mathbb{R}^{0 \vert 2} && && \mathbb{R}^{0\vert 2} \\ & \searrow && \swarrow \\ && \mathbf{B} \mathbb{R}^3 } \,.

There is a 1-dimensional space of Spin(2,1)Spin(2,1)-invariant 2-cocycles on 2,1|2+2\mathbb{R}^{2,1\vert \mathbf{2} + \mathbf{2}}. The Lie algebra extension classified by that is 4d super Minkowski spacetime

3,1|4 2,1|2+2 B \array{ \mathbb{R}^{3,1\vert 4} \\ \downarrow \\ \mathbb{R}^{2,1\vert \mathbf{2}+{\mathbf{2}}} &\longrightarrow& \mathbf{B}\mathbb{R} }

By inspection of the real spin representations in dimension 4.

Now the old brane scan gives:

H 4( 3,1|4)= H^4(\mathbb{R}^{3,1\vert \mathbf{4}}) = \mathbb{R}

represented by the 4-cocycle which, as a left invariant super differential form on 3,1|2\mathbb{R}^{3,1\vert \mathbf{2}} is the WZW term in the Green-Schwarz action functional for the super 2-brane in 4d.

𝔪2𝔟𝔯𝔞𝔫𝔢 onG 2 3,1|4 B 3. \array{ \mathfrak{m}2\mathfrak{brane}_{on\,G_2} \\ \downarrow \\ \mathbb{R}^{3,1\vert \mathbf{4} } &\stackrel{}{\longrightarrow}& \mathbf{B}^3 \mathbb{R} } \,.
Lorentz symmetry

Notice that so far we have obtained 3-dimensional and 4-dimensional Minkowski spacetime and the WZW-term for the superstring and the membrane propagating on it without assuming knowledge of the Lorentz group. In fact we assumed nothing but the presence of the real line \mathbb{R} and the odd line 0|1\mathbb{R}^{0|1} and we have simply investigated their cohomology.

The following proposition shows that the Lorentz group, in fact its universal cover by the pseudo-Riemannian spin group is deduced from this.


Let d1,1,N\mathbb{R}^{d-1,1,N} be super Minkowski spacetime in dimension d{3,4,6,10}d \in \{3,4,6,10\} and let ϕΩ 3( d1,1|N)\phi \in \Omega^{3}(\mathbb{R}^{d-1,1|N}) the corresponding 3-form characterizing the super-1-brane (superstring) in this dimension, according to the brane scan . Then the stabilizer subgroup of both the super Lie bracket and the cocycle is the Spin group Spin(d1,1)Spin(d-1,1):

Stab GL( d1,1|N)([,],ϕ)Spin(d1,1)GL( d1,1|N). Stab_{GL(\mathbb{R}^{d-1,1|N})}([-,-], \phi) \simeq Spin(d-1,1) \hookrightarrow GL(\mathbb{R}^{d-1,1|N}) \,.

It is clear that the spin group fixes the cocycle, and by the discussion at spin representation it preserves the bracket. Therefore it remains to be seen that the Spin group already exhausts the stabiizer group of bracket and cocycle. For that observe that the 3-cocycle is

(ψ,ϕ,v)η([ψ,ϕ],v), (\psi,\phi, v) \mapsto \eta( [\psi,\phi], v ) \,,

where η(,)\eta(-,-) is the given Minkowski metric, and that the bilinear map

[,]:SSV [-,-]\colon S \otimes S\to V

is surjective. This imples that if gGL( d1,1|N)g \in GL(\mathbb{R}^{d-1,1|N}) preserves both the bracket and the cocycle for all ψ,ϕS\psi, \phi \in S and vVv \in V to

η([g(ψ),g(ϕ)],g(v))=η(g([ψ,ϕ]),g(v))=η([ψ,ϕ],v) \eta( [g(\psi),g(\phi)], g(v) ) = \eta( g([\psi,\phi]), g(v) ) = \eta( [\psi,\phi], v )

then it preserves the Minkowski metric for all w,vw,v

η(g(w),g(v))=η(w,v). \eta(g(w), g(v)) = \eta(w,v) \,.

This means that 2,1|2\mathbb{R}^{2,1|2}-manifolds XX equipped with the 3-cocycle as a definite form such that the resulting G-structure according to prop. also preserves the the group structure on 2,1|2\mathbb{R}^{2,1|2}, then this is equivalent to equipping XX with Lorentzian orthogonal structure, hence with super-pseudo-Riemannian metric, hence with a field-configuration for 3d supergravity.

Fundamental branes

The brane bouquet that we find…

𝔪2𝔟𝔯𝔞𝔫𝔢 onG 2 3,1|4 2,1|2¯ 𝔰𝔱𝔯𝔦𝔫𝔤 IIAonG 2 2,1|2+2¯ 3 0|2+2¯ 2,1|2 0|2 0|1 0|1 \array{ && \mathfrak{m}2\mathfrak{brane}_{on\,G_2} \\ && \downarrow \\ && \mathbb{R}^{3,1|\mathbf{4}} && \mathbb{R}^{2,1|\overline{\mathbf{2}}} \\ && \downarrow & \nearrow& & \searrow \\ \mathfrak{string}_{IIA\,on\,G_2} &\longrightarrow& \mathbb{R}^{2,1|\mathbf{2}+\overline{\mathbf{2}}} && && \mathbb{R}^{3} \\ && \downarrow &\searrow& & \nearrow \\ && \mathbb{R}^{0|\mathbf{2}+\overline{\mathbf{2}}} && \mathbb{R}^{2,1|\mathbf{2}} \\ && && \downarrow \\ && && \mathbb{R}^{0|\mathbf{2}} \\ && & \swarrow && \searrow \\ && \mathbb{R}^{0|1} && && \mathbb{R}^{0|1} }

this is equivalently the physics coming from M-theory on G2-manifolds, given by the extensions that emanate from 32 copies of the smallest superpoint:

𝔪5𝔟𝔯𝔞𝔫𝔢 𝔪2𝔟𝔯𝔞𝔫𝔢 p𝔡2p𝔟𝔯𝔞𝔫𝔢 10,1|32 𝔰𝔱𝔯𝔦𝔫𝔤 IIA 9,1|16+16¯ 0|16+16¯ 0|1 0|1 \array{ && && \mathfrak{m}5\mathfrak{brane} \\ && && \downarrow \\ && && \mathfrak{m}2\mathfrak{brane} \\ && && \downarrow \\ && \underset{p}{\coprod} \mathfrak{d}{2p}\mathfrak{brane} && \mathbb{R}^{10,1|\mathbf{32}} \\ && \downarrow && \downarrow \\ && \mathfrak{string}_{IIA} &\longrightarrow & \mathbb{R}^{9,1|\mathbf{16}+\overline{\mathbf{16}}} \\ && && \downarrow \\ && && \mathbb{R}^{0|\mathbf{16}+\overline{\mathbf{16}}} \\ && & \swarrow && \searrow \\ && \mathbb{R}^{0|1} && \cdots && \mathbb{R}^{0|1} }

These are branches of The brane bouquet of string theory, see there for more. By prop. each branch here gives the WZW form for the corresponing Green-Schwarz super p-brane sigma model.


Above we have found two interlocking ingredients arising from the axiomatics:

  1. abstract generals – Given any group object VV, then there is an abstract general concept of VV-manifolds XX, def. . Given furthermore a WZW term L WZW V\mathbf{L}_{WZW}^V on VV, then there is an abstract general concept of definite globalizations of this term over these manifolds XX, inducing G-structures on XX, prop. .

  2. concrete individuals – We have found concrete individual VVs: extended super Minkowski spacetimes, prop. , prop. emanating from the objects which represent the moments ʃ&#643; and \rightrightarrows, and we have further found individual L WZW V\mathbf{L}_{WZW}^V: the super p-brane WZW terms, prop. etc., forming The brane bouquet.

Plugging the concrete individuals into the general abstract theory, we hence obtain particular phenomena.

(1) relU d1,1|N X L WZW brane L WZW X B p+2𝔾 conn \array{ && \flat^{rel}_{(1)} U \\ & \swarrow && \searrow \\ \mathbb{R}^{d-1,1|\mathbf{N}} && \swArrow && X \\ & {}_{\mathllap{\mathbf{L}_{WZW}^{brane}}}\searrow && \swarrow_{\mathrlap{\mathbf{L}_{WZW}^X}} \\ && \mathbf{B}^{p+2}\mathbb{G}_{conn} }

Specifically there is 11-dimensional super Minkowski spacetime V= 10,1|32V = \mathbb{R}^{10,1\vert \mathbf{32}} carrying the WZW term L WZW M2\mathbf{L}_{WZW}^{M2} for the M2-brane, in some sense the endpoint of the bouquet of super-spacetimes. The KK-compactification of this on a 7-dimensional G2-manifold yields the 4-dimensional super-Minkowski spacetime discussed above, with the WZW term for the super 2-brane in 4d.

The 11-dimensional super-Minkowski spacetime is special in many ways, one of which is that in this dimension the equations of motion of 11-dimensional supergravity on a (Spin(10,1)Iso( 10,1|32))(Spin(10,1)\hookrightarrow Iso(\mathbb{R}^{10,1\vert \mathbf{32}}))-super Cartan geometry XX modeled on 10,1|32\mathbb{R}^{10,1\vert \mathbf{32}} are already captured by just a constraint on the torsion tensor. But by remark this means that in dimension 11 the equations of motion of supergravity have an immediate axiomatization in our objective logic.

equivalent to just the condition that the of XX is at each point and to first infinitesimal order the intrinsic torsion of 10,1|32\mathbb{R}^{10,1\vert \mathbf{32}}


First-order integrable (Spin(10,1)Iso( 10,1|32))(Spin(10,1)\hookrightarrow Iso(\mathbb{R}^{10,1\vert \mathbf{32}}))-super-Cartan geometries, def. , on 10,1|32\mathbb{R}^{10,1\vert\mathbf{32}}-manifolds XX, def. , which are first-order integrable with respect to the intrinsic left-invariant torsion of 10,1|32\mathbb{R}^{10,1\vert \mathbf{32}}, remark , are equivalent to vacuum solutions to the equations of motion of 11-dimensional supergravity, i.e. to solutions for which the field strength of the gravitino and of the supergravity C-field vanishes identically, hence to solutions to the ordinary vacuum Einstein equations in 11d.


(Howe 97) shows that imposing (on some chart) dE a+ω a bE bψ¯Γ aψ=0\mathbf{d} E^a + \omega^{a}{}_b \wedge E^b - \bar \psi \Gamma^a \psi = 0 implies (and hence is equivalent to) the equations of motion of 11d supergravity. These equations (see e.g. D’Auria-Fré 82, p. 31) then show that furthermore requiring dψ+12ω abΓ abψ=0\mathbf{d} \psi + \tfrac{1}{2}\omega_{a b} \Gamma^{a b}\psi = 0 (and hence requiring the full supertorsion tensor to be that of super-Minkowski spacetime) puts the field strength of the gravitino and of the supergravity C-field to 0.


Vacuum Einstein solutions as in prop. , are considered notably in the context of M-theory on G2-manifolds (e.g. Acharya 02, p. 9). See also at M-theory on G2-manifolds – Details – Vacuum solution and torsion constraints.


Given a definite globalization L WZW X\mathbf{L}_{WZW}^X of a super pp-brane WZW term L WZW V\mathbf{L}_{WZW}^V, then the stabilizer infinity-group of L WZW\mathbf{L}_{WZW} is the integrated BPS charge algebra of this solution of supergravity.

See at BPS charge – Formalization in higher differential geometry.


These notes benefited from discussion with Dave Carchedi, David Corfield, Thomas Holder, John Huerta and Mike Shulman.



Related talks include

  1. Quantum gauge field theory in Cohesive homotopy type theory,

  2. Synthetic Quantum Field Theory,

  3. Classical field theory via Cohesive homotopy types,

  4. Quantization via Linear homotopy types

  5. Duality of Monads in Geometric Homotopy Theory

Last revised on January 7, 2019 at 16:13:07. See the history of this page for a list of all contributions to it.