text:
\section{Introduction}
\label{sec:introduction}

The observable world of physical phenomena is fundamentally governed by
\emph{quantum gauge field theory} (QFT) \cite{Deligne},
as was recently once more confirmed by the
detection \cite{CERNPressRelease} of the Higgs boson \cite{Bernstein}.
On the other hand, the world of mathematical concepts
is fundamentally governed by \emph{formal logic}, as elaborated in a foundational system such as axiomatic set theory or type theory.

Quantum gauge field theory is traditionally valued for the elegance and beauty
of its mathematical description (as far as this has been understood).
Formal logic is likewise valued for elegance and simplicity; aspects which have become especially important recently because they enable formalized mathematics to be verified by computers.
This is generally most convenient using type-theoretic foundations~\cite{MartinLoef}; see e.g.~\cite{Coquand}.

However, the mathematical machinery of quantum gauge field theory ---
such as differential geometry
(for the description of spacetime \cite{GS}),
differential cohomology
(for the description of gauge force fields \cite{HopkinsSinger, Freed})
and symplectic geometry
(for the description of geometric quantization \cite{Brylinski})
--- has always seemed to be many levels of complexity above the mathematical foundations.
Thus, while automated proof-checkers
can deal with fields like linear algebra \cite{Coquand},
even formalizing a basic differential-geometric \emph{definition} (such as a principal connection on a smooth manifold) seems intractable,
not to speak of proving its basic properties.

\medskip

We claim that this situation improves drastically by combining two insights from type theory.
The first is that type theory can be interpreted ``internally''
in
locally Cartesian closed categories
(see e.g.~\cite{CD}),
including categories of smooth spaces (which contain the classical category of smooth manifolds).
In this way, type-theoretic arguments which appear to speak about discrete sets may be interpreted to speak about smooth spaces, with the smooth structure automatically ``carried along for the ride''.
Thus, differential notions can be developed in a simple and elegant axiomatic framework --- avoiding the complexity of the classical definitions by working in a formal system whose \emph{basic objects} are already ``smooth''.
This is known as \emph{synthetic differential geometry} (SDG)~\cite{kock:sdg,lavendhomme:sdg,SIA}.
In this paper, we
will axiomatize it in a way which does not require that our basic objects are ``smooth'',
only that they are ``cohesive'' as in~\cite{Lawvere}.
This includes topological objects as well as smooth ones,
and also variants of differential geometry such as \emph{supergeometry},
which is necessary for a full treatment of quantum field theory (for the description of fermions).

The second
insight is that types in
intensional
type theory can also behave like \emph{homotopy types},
a.k.a.\ \emph{$\infty$-groupoids}, which are not just sets of points but contain higher homotopy information.
Just as SDG imports differential geometry directly into type theory, this one imports \emph{homotopy theory}, and as such is called \emph{homotopy type theory}~\cite{Voevodsky,AwodeyHoTT,ShulmanCourse,hottbook}.

Combining these insights, we obtain \emph{cohesive homotopy type theory}~\cite{ShulmanCohesion,SchreiberCohesion}.
Its basic objects (the ``types'') have both \emph{cohesive structure} and \emph{higher homotopy structure}.
These two kinds of structure are independent, in contrast to how classical algebraic topology identifies homotopy types with the topological spaces that present them.
For instance, the geometric circle $S^1$ is categorically \emph{0-truncated}
(it has a mere set of points with no isotropy),
but carries an interesting topological or smooth structure ---
whereas the homotopy type it presents, denoted $\Pi(S^1)$ or $\mathbf{B}\mathbb{Z}$
(see below), has (up to equivalence) only \emph{one} point (with trivial topology), but that point has a countably infinite isotropy group.
More general cohesive homotopy types can be nontrivial in both ways,
such as orbifolds~\cite{MoerdijkPronk,Lerman} and moduli stacks~\cite{Wang}.
In particular the standard model of SDG known as the {\it Cahiers topos} lifts to a model of
cohesive homotopy type theory that contains orbifolds and generally moduli stacks equipped with
synthetic differential structure (section 4.5 of \cite{SchreiberCohesion}).

\medskip

Today it is clear that homotopy theory is at the heart of quantum field theory.
One way to define an
$n$-dimensional QFT is as a rule that assigns to each
closed $(n-1)$-dimensional manifold, a vector space --- its space of \emph{quantum states} --- and
to each $n$-dimensional \emph{cobordism},
a linear map between the corresponding vector spaces --- a \emph{correlator} ---
in a way which respects gluing of cobordisms.
An \emph{extended} or \emph{local} QFT also assigns data
to all $(0 \leq k \leq n)$-dimensional manifolds,
such that the data assigned to any manifold can be reconstructed by gluing along lower dimensional boundaries.
By~\cite{BD,LurieTQFT},
the case of \emph{extended topological QFT}
(where the manifolds are equipped only with smooth structure) is entirely defined and classified by
a universal construction in \emph{directed homotopy theory}, i.e.\ $(\infty,n)$-category theory~\cite{BarwickSchommer-Pries,ShulmanDirected}.
For non-topological QFTs, where the cobordisms have conformal or metric
structure, the situation is more complicated, but directed
homtopy type theory still governs the construction;
see~\cite{SatiSchreiber} for recent developments.
We will see in section \ref{GeometricQuantization}
how in cohesive homotopy type theory one naturally obtains such higher
spaces of (pre-)quantum states assigned to manifolds of higher codimension.

Notice, as discussed in the introduction of \cite{SatiSchreiber},
that many of the developments that led to these insights
about the role of homotopy theory in quantum field theory originate in \emph{string theory},
but they are now statements in pure QFT. String theory is the investigation
of the \emph{second quantization} of 1-dimensional quanta (``strings'') instead of 0-dimensional
quanta (``particles'') and this increase in geometric dimension induces a corresponding
increase of homotopical dimension of many aspects. At least some of these are also usefully captured
by cohesive homotopy type theory \cite{SchreiberLectures}.
But while the phenomenological relevance of string theory for fundamental physics remains speculative,
its proposal alone led to further investigation into the nature of pure quantum field theories
which showed how this alone already involves homotopy theory, as used here.

The value of \emph{cohesive} homotopy theory for physics lies in the observation that
the QFTs observed to
govern our world at the fundamental level --- namely,
Yang-Mills theory (for electromagnetism and the weak and strong nuclear forces)
and Einstein general relativity (for gravity) --- are not random
instances of such QFTs.
Instead
(1) their construction follows a geometric principle,
traditionally called the \emph{gauge symmetry principle}~\cite{RS},
and (2) they are obtained by \emph{quantization} from
(``classical'') data that lives in \emph{differential cohomology}.
Both of these aspects are actually native to cohesive homotopy type theory, as follows:
\begin{enumerate}[leftmargin=*]
\item The very concept of a collection of quantum field configurations
with \emph{gauge transformations} between them
is really that of a configuration \emph{groupoid}, hence of a homotopy 1-type.
More generally, in higher gauge theories such as those that appear in string theory, the
\emph{higher gauge symmetries} make the configurations form higher groupoids, hence general
homotopy types.
Furthermore,  these configuration groupoids of gauge fields have
\emph{smooth structure}: they are \emph{smooth homotopy types}.

To physicists, these smooth configuration groupoids
are most familiar in their infinitesimal Lie-theoretic
approximation: the (higher) \emph{Lie algebroids} whose function algebras
constitute the \emph{BRST complex}, in terms of which modern quantum gauge theory is
formulated \cite{HT}. The degree-$n$
\emph{BRST cohomology} of these complexes
corresponds to the $n^{\mathrm{th}}$ \emph{homotopy group} of the cohesive homotopy types.
\item Gauge fields are \emph{cocycles} in a cohomology theory
(sheaf hyper-cohomology), and the
gauge transformations
between them are its
coboundaries.
A classical result~\cite{Brown} says, in modern language,
that all such cohomology theories are realized in some interpretation of
homotopy type theory (in some $(\infty,1)$-category of $(\infty,1)$-sheaves):
the cocycles on $X$ with coefficients in $A$ are just functions $X \to A$.
Moreover, if $A$ is the coefficients of some \emph{differential} cohomology theory, then the \emph{type} of all such functions is exactly the configuration gauge groupoid of quantum fields on $A$ from above.
This cannot be expressed in plain homotopy theory, but it can be in \emph{cohesive} homotopy theory.

Finally, differential cohomology is also the natural context for
\emph{geometric quantization}, so that central aspects of this process can also be formalized in
cohesive homotopy type theory.
\end{enumerate}

\vspace{.2cm}

In \S\ref{sec:cohott}, we briefly review homotopy type theory and then describe the axiomatic formulation of cohesion.
The axiomatization is chosen so that if we \emph{do} build things from the ground up out of sets, then we can construct categories (technically, \io-categories of \io-sheaves) in which cohesive homotopy type theory is valid internally.
This shows that the results we obtain can always be referred back to a classical context.
However, we emphasize that the axiomatization stands on its own as a formal system.

Then in \S\ref{sec:quantum}, we show how cohesive homotopy type theory directly expresses
fundamental concepts in differential geometry, such as differential forms,
Maurer-Cartan forms, and connections on principal bundles.
Moreover, by the homotopy-theoretic ambient logic, these concepts are thereby automatically generalized to
\emph{higher differential geometry} \cite{NSS}. In particular,
we show how to naturally formulate
\emph{higher moduli stacks} for \emph{cocycles in differential cohomology}.
Their 0-truncation shadow has been known to
formalize gauge fields and higher gauge fields \cite{Freed}.
We observe that their full homotopy formalization yields a refinement of
the Chern-Weil homomorphism from secondary characteristic classes to
cocycles, and also the action functional of generalized
Chern-Simons-type gauge theories with an \emph{extended} geometric prequantization.
At present, however, completing the process of quantization requires special properties of the usual models; work is in progress isolating exactly how much quantization can be done formally in cohesive homotopy type theory.

The constructions of \S\ref{sec:cohott} have been fully implemented in {\tt Coq
\footnote{Currently, this requires a patch to Coq that collapses universe levels (making it technically inconsistent).  However, true ``universe polymorphism'' is slated for future inclusion in Coq, which should should make this no longer necessary.} \cite{Coq};
the source code can be found at~\cite{CohesiveCoq}.  With this as foundation, the implementation
of much of \S\ref{sec:quantum} is straightforward.

\section{Cohesive homotopy type theory}
\label{sec:cohott}

\subsection{Categorical type theory}
\label{sec:type-theory}

A type theory is a formal system
whose basic objects are \emph{types} and \emph{terms},
and whose basic assertions are that a term $a$ belongs to a type $A$, written ``$a:A$''.
More generally, $\jd{x:A, y:B |- c:C}$ means that given variables $x$ and $y$ of types $A$ and $B$, the term $c$ has type $C$.
For us,
types themselves are terms of type \type.
(One avoids paradoxes arising from $\type:\type$ with a hierarchy of universes.)
Types involving variables are called \emph{dependent types}.

Operations on types include cartesian product $A\times B$, disjoint union $A+B$, and function space $A\to B$, each with corresponding rules for terms.
Thus $A\times B$ contains pairs $(a,b)$ with $a:A$ and $b:B$, while $A\to B$ contains functions $\lambda x^A.b$ where $b:B$ may involve the variable $x:A$, i.e.\ $\jd{x:A |- b:B}$.
Similarly, if $\jd{x:A |- B(x):\type}$ is a dependent type, its \emph{dependent sum} $\sum_{x:A} B(x)$ contains pairs $(a,b)$ with $a:A$ and $b:B(a)$, while its \emph{dependent product} $\prod_{x:A} B(x)$ contains functions $\lambda x^A .b$ where $\jd{x:A |- b : B(x)}$.

In many ways, types and terms behave like sets and elements as a foundation for mathematics.
One fundamental difference is that
in type theory, rather than proving theorems \emph{about} types and terms, one \emph{identifies}
``propositions'' with
types containing at most one term
(also called ``mere propositions'', for emphasis),
and ``proofs'' with terms belonging to such types.
Constructions such as $\times,\to,\prod$ restrict to logical operations such as $\wedge,\Rightarrow,\forall
, embedding logic into type theory.
By default, this logic is \emph{constructive}, but one can force it to be classical.

Type theory also admits \emph{categorical models}, where types are interpreted by objects of a category $\H$, while a term $\jd{x:A, y:B |- c:C}$ is interpreted by a morphism $A\times B\to C$.
A dependent type $\jd{x:A |- B(x):\type}$ is interpreted by $B\in\H/A$, while $\jd{x:A|- b:B(x)}$ is interpreted  by a \emph{section} of $B$, and substitution of a term for $x$ in $B(x)$ is interpreted by pullback.
Thus, we can ``do mathematics'' internal to \H, with any additional structure on its objects
carried along automatically.
In this case, the logic is usually unavoidably constructive.

In the context of quantum physics, such ``internalization'' has been used in the ``Bohrification'' program~\cite{Bohrification} to make noncommutative von Neumann algebras into internal commutative ones.
There are also ``linear'' type theories which describe mathematics internal to monoidal categories (such as Hilbert spaces); see~\cite{Rosetta}.

\subsection{Homotopy type theory}
\label{sec:hott}

Since propositions are types, we expect \emph{equality types}
\[\jd{x:A,y:A|- (x=y):\type}.\]
But surprisingly, $(x=y)$ is naturally \emph{not} a mere proposition.
We can add axioms forcing it to be so, but if we don't, we obtain \emph{homotopy type theory}~\cite{hottbook}, where types behave less like sets and more like \emph{homotopy types} or \emph{$\infty$-groupoids}.\footnote{The associativity of terminology ``homotopy (type theory) = (homotopy type) theory'' is coincidental, though fortunate!}
Space does not permit an introduction to homotopy theory and higher category theory here; see e.g.~\cite[\S1.1]{LurieHTT}.
We re-emphasize that in \emph{cohesive} homotopy type theory, simplicial or algebraic models for homotopy types are usually less confusing than topological ones.

Homotopy type theory admits models in \emph{\io-categories}, where the equality type of $A$ indicates its diagonal $A\to A\times A$.
Voevodsky's \emph{univalence axiom}~\cite{KLVunivalence} implies that the type \type is an
\emph{object classifier}: there is a morphism $p:{\type}_\bullet\to \type$ such that
pullback of $p$ induces an equivalence of $\infty$-groupoids
\begin{equation}
  \H(A,\type) \simeq \mathrm{Core}_\kappa(\H/A).\label{eq:objclassif}
\end{equation}
(The \emph{core} of an \io-category contains all objects, the morphisms that are equivalences, and all higher cells; $\mathrm{Core}_\kappa$ denotes the
small full subcategory of ``$\kappa$-small'' objects.)
A well-behaved \io-category with object classifiers is called an \emph{\io-topos}; these are the natural places to internalize homotopy type theory.\footnote{There are, however, coherence issues in making this precise, which are a subject of current research; see e.g.~\cite{ShulmanUnivalence,ShulmanUnivalence2}.}

An object $X\in\H$ is \emph{$n$-truncated} if it has no homotopy above level $n$.
The $0$-truncated objects are like sets, with no higher homotopy, while the $(-1)$-truncated objects are the propositions.
The $n$-truncated objects in an \io-topos are reflective, with reflector $\pi_n$; in type theory, this is
an example of
a \emph{higher inductive type}~\cite{ShulmanLumsdaine,hottbook}
which is the homotopy-theoretic refinement of a type defined by induction, such as the natural numbers.
The $(-1)$-truncation of a morphism $X\to Y$, regarded as an object of $\H/Y$, is its \emph{image factorization}.

\subsection{Cohesive \io-toposes}
\label{sec:cohesion}

A \emph{cohesive \io-topos} is an \io-category whose objects can be thought of as $\infty$-groupoids
endowed with ``cohesive structure'', such as a topology or a smooth structure.
As observed in~\cite{Lawvere} for 1-categories, this gives rise to a string of adjoint functors relating $\H$ to \ig (which replaces $\mathbf{Set}$ in~\cite{Lawvere}).
First, the \emph{underlying} functor $\Gamma:\H\to\ig$ forgets the cohesion.
This can be identified with the hom-functor $\H(*,-)$, where the terminal object $*$ is a single point with its trivial cohesion.

Secondly, any $\infty$-groupoid admits both a \emph{discrete} cohesion, where no distinct points ``cohere'' nontrivially, and a \emph{codiscrete} cohesion, where all points ``cohere'' in every possible way.
This gives two fully faithful functors $\Delta: \ig\to\H$ and $\nabla:\ig\to\H$, left and right adjoint to $\Gamma$ respectively.

Finally, $\Delta$ also has a left adjoint $\Pi$, which preserves finite products.
In~\cite{Lawvere}, $\Pi$ computes \emph{sets of connected components}, but for \io-categories, $\Pi$ computes entire \emph{fundamental $\infty$-groupoids}.
There are two origins of higher morphisms in $\Pi(X)$: the higher morphisms of $X$, and the cohesion of $X$.
If $X=\Delta Y$ is an ordinary $\infty$-groupoid with discrete cohesion, then $\Pi(X) \simeq Y$.
But if $X$ is a plain set with some cohesion (such as an ordinary smooth manifold), then $\Pi(X)$ is its ordinary fundamental $\infty$-groupoid, whose higher cells are paths and homotopies in $X$.
If $X$ has both higher morphisms and cohesion, then $\Pi(X)$ automatically combines these two sorts of higher morphisms sensibly, like the Borel construction of an orbifold.

Thus, we define an \io-topos \H to be \emph{cohesive} if it has an adjoint string
\begin{equation}
\vcenter{\xymatrix{
  \H \ar@<2mm>[d]|{\Gamma} \ar@<-6mm>[d]|{\Pi}\\
  \ig \ar@<2mm>[u]|{\Delta} \ar@<-6mm>[u]|{\nabla}
}}\label{eq:cohesion}
\end{equation}
where $\Delta$ and $\nabla$ are fully faithful and $\Pi$ preserves finite products.
Using $\infty$-sheaves on sites~\cite{CohesiveSites}, we can obtain such \H's which contain smooth manifolds as a full subcategory; we call these \emph{smooth models}.

Now we plan to work in the internal type theory of such an \H, so we must reformulate cohesiveness internally to \H.
But since $\Delta$ and $\nabla$ are fully faithful, from inside \H we see two subcategories, of which the codiscrete objects are reflective, and the discrete objects are both reflective (with reflector preserving finite products) and coreflective.
We write $\sharp \coloneqq \nabla\Gamma$ for the codiscrete reflector, $\flat \coloneqq \Delta\Gamma$ for the discrete coreflector, and $\Pi \coloneqq \Delta\Pi$ for the discrete reflector.
Assuming only this, if $A$ is discrete and $B$ is codiscrete, we have
\[ \H(\sharp A,B) \simeq \H(A,B) \simeq \H(A,\flat B) \]
so that $\sharp\dashv\flat$ is an adjunction between the discrete and codiscrete objects.
If we assume that for \emph{any} $A\in\H$, the maps $\flat A\to \flat\sharp A$ and $\sharp \flat A\to\sharp A$ induced by $\flat A\to A\to \sharp A$ are equivalences, this adjunction becomes an equivalence, modulo which $\flat$ is identified with $\sharp$ (i.e.\ $\Gamma$).
From this we can reconstruct~\eqref{eq:cohesion}, except that the lower \io-topos need not be \ig.
This is expected: just as homotopy type theory admits models in all \io-toposes, cohesive homotopy type theory admits models that are ``cohesive over any base''.

We think of $\sharp$, $\flat$, and $\Pi$ as \emph{modalities}, like those of~\cite{AB}, but which apply to all types, not just propositions.
Note also that as functors $\H\to \H$, we have $\Pi\dashv\flat$, since for any $A$ and $B$
\[ \H(\Pi A,B)\simeq \H(\Pi A,\flat B) \simeq \H(A,\flat B) \]
as both $\Pi A$ and $\flat B$ are discrete.

\subsection{Axiomatic cohesion I: Reflective subfibrations}
\label{sec:axiomatic-cohesion-i}

We begin our internal axiomatization with the reflective subcategory of codiscrete objects.
An obvious
way to describe a reflective subcategory in type theory is to use \type.
(This idea is also somewhat na\"ive; in a moment we will discuss an important subtlety.)
First we need, for any type $A$, a proposition expressing the assertion ``$A$ is codiscrete''.
Since propositions are particular types, this can simply be a function term
\begin{equation}
  \mathsf{isCodisc} : \type \to \type
\end{equation}
together with an axiom asserting that for any type $A$, the type $\mathsf{isCodisc}(A)$ is a proposition:
\begin{equation}
  \jd{A:\type |- \mathsf{isCodiscIsProp}_A : \mathsf{isProp} (\mathsf{isCodisc}(A))}
\end{equation}
Next we need the reflector $\sharp$ and its unit:
\begin{gather}
\sharp : \type\to\type.\\
\jd{A:\type |- \mathsf{sharpIsCodisc}_A : \mathsf{isCodisc}(\sharp A)}\\
  \jd{A:\type |- \eta_A : A \to \sharp A}.  \label{SharpUnit}
\end{gather}
Finally, we assert the universal property of the reflection: if $B$ is codiscrete, then the space of morphisms $\sharp A \to B$ is equivalent, by precomposition with $\eta_A$, to the space of morphisms $A\to B$.
\begin{equation}
  \jd{A:\type, B:\type, \mathsf{bc} : \mathsf{isCodisc}(B) |-
    \mathsf{tsr} : \mathsf{isEquiv} (\lambda f^{\sharp A\to B}. f\circ \eta_A)
  }\label{eq:tsr}
\end{equation}
This looks like a complete axiomatization of a reflective subcategory, but in fact it describes more data than we want, because \type is an object classifer for \emph{all} slice categories.
If \H satisfies these axioms, then each $\H/X$ is equipped with a reflective subcategory, and moreover these subcategories and their reflectors are stable under pullback.
For instance, if $A\in\H/X$ is represented by $\jd{x:X |- A(x):\type}$, then the dependent type $\jd{x:X |- \sharp(A(x)):\type}$ represents a ``fiberwise reflection'' $\sharpsub{X}(A) \in \H/X$.

We call such data a \emph{reflective subfibration}~\cite{CJKP}.
If a reflective subcategory underlies some reflective subfibration, then its reflector preserves finite products, and the converse holds in good situations~\cite{ShulmanSubfibrations}.
If the reflector even preserves all finite \emph{limits}, as $\sharp$ does, then there is a \emph{canonical} extension to a reflective subfibration.
Namely, we define $A\in\H/X$ to be \emph{relatively codiscrete} if the naturality square for $\eta$:
\[\vcenter{\xymatrix@-.5pc{
    A\ar[r]^{\eta_A}\ar[d] &
    \sharp A\ar[d]\\
    X\ar[r]^{\eta_X} &
    \sharp X
  }}\]
is a pullback.
(This says that $A$ has the ``initial cohesive structure'' induced from $X$: elements of $A$ cohere in precisely the ways that their images in $X$ cohere.)
For general $A\in\H/X$, we define $\sharpsub{X}A$ to be the pullback of $\sharp A \to \sharp X$ along $X\to \sharp X$.
When $\sharp$ preserves finite limits, this defines a reflective subfibration.

Reflective subfibrations constructed in this way are characterized by two special properties.
The first is that the relatively codiscrete morphisms are closed under composition.
A reflective subfibration with this property is equivalent to a \emph{stable factorization system}: a pair of classes of morphisms $(\E,\M)$ such that every morphism factors essentially uniquely as an \E-morphism followed by an \M-morphism, stably under pullback.
(The corresponding reflective subcategory of $\H/X$
is the category of \M-morphisms into $X$.)
If a reflective subcategory underlies a stable factorization system, its reflector preserve all pullbacks over objects in the subcategory --- and again, the converse holds in good situations~\cite{ShulmanSubfibrations}; such a reflector has \emph{stable units}~\cite{CHK}.

We can axiomatize this property as follows.
Axiom~\eqref{eq:tsr} implies, in particular, a factorization operation:
\begin{gather}
  \jd{\mathsf{bc}:\mathsf{isCodisc}(B), f:A\to B |- \factsharp(f):\sharp A \to B} \label{eq:sharpfact1} \\
  \jd{\mathsf{bc}:\mathsf{isCodisc}(B), f:A\to B |- \mathsf{ff}_f:(\factsharp(f) \circ \eta_A = f)}\label{eq:sharpfact2}
\end{gather}
It turns out that relatively codiscrete morphisms are closed under composition if and only if we have a more general factorization operation, where $B$ may depend on $\sharp A$:
\begin{gather}
  \jd{ \mathsf{bc}:\textstyle\prod_{x:\sharp A}\mathsf{isCodisc}(B(x)),
    f:\textstyle\prod_{x:A} B(\eta_A(x))
    |- \factsharp(f):\textstyle\prod_{x:\sharp A} B(x)} \\
  \jd{ \mathsf{bc}:\textstyle\prod_{x:\sharp A}\mathsf{isCodisc}(B(x)),
    f:\textstyle\prod_{x:A} B(\eta_A(x))
    |- \mathsf{ff}_f: (\factsharp(f) \circ \eta_A = f)}
\end{gather}
This sort of ``dependent factorization'' is familiar in type theory;
it is related to~\eqref{eq:sharpfact1}--\eqref{eq:sharpfact2} in the same way that proof by induction is related to definition by recursion.

The second property is that if $g\in\E$ and $g f \in\E$, then $f\in \E$.
If a stable factorization system has this property, then it is determined by its underlying reflective subcategory, whose reflector must preserve finite limits.
(\E is the class of morphisms inverted by the reflector, and \M is defined by pullback as above.)
We can state this in type theory as the preservation of $\sharp$-contractibility by homotopy fibers:
\begin{multline}\label{eq:lexrefl}
  \jd{\mathsf{acs}:\mathsf{isContr}(\sharp A), \mathsf{bcs}:\mathsf{isContr}(\sharp B),
    f:A\to B, b:B |- \mathsf{fcs} : \mathsf{isContr}\left(\sharp \textstyle\sum_{x:A}(f(x)=b)\right)}
\end{multline}
This completes our axiomatization of the reflective subcategory of codiscrete objects.
We can apply the same reasoning to the reflective subcategory of \emph{discrete} objects.
Now $\Pi$ does not preserve all finite limits, only finite products, so we cannot push the characterization all the way as we did for $\sharp$.
But because the target of $\Pi$ is \ig, it automatically has stable units; thus the discrete objects underlie \emph{some} stable factorization system $(\E,\M)$, which can be axiomatized as above with~\eqref{eq:lexrefl} omitted.
(For cohesion over a general base, we ought to demand stable units explicitly.)
We do not know whether there is a particular choice of such an $(\E,\M)$ to be preferred.
In \S\ref{sec:axiomatic-cohesion-ii}, we will mention a different way to axiomatize $\Pi$ which is less convenient, but does not require choosing $(\E,\M)$.

\subsection{Axiomatic cohesion II: $\sharp\type$}
\label{sec:axiomatic-cohesion-ii}

We consider now an axiomatization of the external hom $\H(A,B)$ in addition
to the internal hom $A \to B$. The latter we will equivalently write also as
$[A,B]$, which better matches the convention in algebraic topology and in geometry.
More precisely, we consider the external $\infty$-groupoid $\H(A,B)$, re-internalized as a codiscrete object.
(Since $\sharp$ preserves more limits than $\Pi$, the codiscrete objects are a better choice for this sort of thing.)

To construct such an external function-type, consider $\sharp\type$.
This is a codiscrete object, which as an $\infty$-groupoid is interpreted by the core of (some small full subcategory of) \H.
Any type $A:\type$ has an ``externalized'' version $\eta_\type(A):\sharp \type$, which we denote $\llbracket A\rrbracket$.
And since $\sharp$ preserves products, the operation
\begin{gather*}
[-,-]:\type\times\type\to\type \mathrlap{\qquad\qquad\text{induces an operation}}\\
[-,-]^\sharp:\sharp\type\times\sharp\type\to\sharp\type
\end{gather*}
which is interpreted by the internal-hom $[-,-]$ as an operation $\mathrm{Core}(\H) \times \mathrm{Core}(\H) \to \mathrm{Core}(\H)$.
We now define the \emph{escaping} morphism $\esc:\sharp\type\to\type$ as follows
\footnote{Technically, $\esc A$ lives in a higher universe than $A$, but we ignore this as it causes no problems.}
\[ \esc A \coloneqq \sum_{B:\sharp \sum_{X:\type} X} (\sharp(\mathsf{pr}_1)(B) = A) \]
Here $\sum_{X:\type} X$ is the type-theoretic version of the domain ${\type}_\bullet$ of the morphism
$p:{\type}_\bullet\to\type$ from \S\ref{sec:hott}, with $p$ being the first projection $\mathsf{pr}_1: \sum_{X:\type} X \to \type$.
Thus functoriality of $\sharp$ gives $\sharp(\mathsf{pr}_1):\sharp \sum_{X:\type} X \to \sharp \type$, and so $\sharp(\mathsf{pr}_1)(B) : \sharp \type$ can be compared with $A$.
Now it turns out that $\esc A$ is codiscrete (i.e.\ $\mathsf{isCodisc}(\esc A)$ is inhabited), and the composite
\[\type \xrightarrow{\eta_\type} \sharp\type \xrightarrow{\esc} \type\]
is equivalent to $\sharp$.
Thus, since
in the intended categorical semantics
$\H(A,B) = \Gamma[A,B]$,
we can define the external function-type as
\[\H(A,B) \coloneqq \esc\left([A, B]^\sharp\right)\]
Note that this makes sense for any $A,B:\sharp\type$.
If instead $A,B:\type$, then $\H(\llbracket A\rrbracket, \llbracket B\rrbracket) \simeq \sharp[A,B]$.
Thus, if $f:[A,B]$, then applying this equivalence to $\eta_{[A,B]}(f): \sharp[A,B]$, we obtain an ``externalized'' version of $f$, which we denote $\llbracket f \rrbracket : \llbracket A\rrbracket \to \llbracket B\rrbracket$.
Now using dependent factorization for the modality $\sharp$, we can define all sorts of categorical operations externally.
We have composition:
\begin{equation*}
  \jd{A\cm B \cm C:\sharp\type, f:{\H(A, B)}, g:{\H(B, C)} |- g \circ f : \H(A,C)}
\end{equation*}
and the property of being an equivalence:
\[ \jd{A\cm B:\sharp \type, f:{\H(A,B)} |- \mathsf{eisEquiv}(f) : \type}. \]

Using these external tools, we can now complete our internal axiomatization of cohesion.
One may be tempted to define the coreflection $\flat$ as we did the reflections $\sharp$ and $\Pi$, but
this would amount to asking for a pullback-stable system of \emph{coreflective} subcategories of each $\H/X$, and at present we do not know any way to obtain this in models.
Instead, we work externally:
\begin{gather}
  \mathsf{eisDisc} : [\sharp\type,\type]\\
  \jd{A:\sharp\type |- \mathsf{eisDiscIsProp}_A : \mathsf{isProp}(\mathsf{eisDisc}(A))}\\
  \flat:[\sharp\type,\sharp\type]\\
  \jd{A:\sharp\type |- \mathsf{flatIsDisc}_A : \mathsf{eisDisc}(\flat A)}\\
  \jd{A:\sharp \type |- \epsilon_A : \H(\flat A, A)}\label{flatCounit}\\
  \jd{A\cm B:\sharp \type, \mathsf{ad} : \mathsf{eisDisc}(A) |-
    \mathsf{flr} : \mathsf{isEquiv}(\lambda f^{{\H(A,\flat B)}} . \, \epsilon_B \circ f)}.\label{eq:flatUniv}
\end{gather}
If we axiomatize discrete objects
as in \S\ref{sec:axiomatic-cohesion-i}, we can define
$\mathsf{eisDisc}(A) \coloneqq \esc(\sharp(\mathsf{isDisc})(A))$.
But we can also treat discrete objects externally only, with $\mathsf{eisDisc}$ axiomatic and $\Pi$ defined analogously to $\flat$.
This would allow us
to avoid choosing an $(\E,\M)$ for the categorical interpretation.
In any case,~\eqref{eq:flatUniv} implies factorizations:
\begin{gather*}
  \jd{\mathsf{ad}:\mathsf{eisDisc}(A), f:{\H(A,B)} |- \factflat(f):{\H(A,\flat B)}} \\
  \jd{\mathsf{ad}:\mathsf{eisDisc}(A), f:{\H(A,B)} |- \mathsf{ff}_f:(\epsilon_B \circ \factflat(f) = f)}.
\end{gather*}
Thus, we can state the final axioms internally as
\begin{gather}
  \jd{A:\sharp\type |- \mathsf{sfe}:\mathsf{eisEquiv} (\factsharp (\llbracket\eta_A\rrbracket \circ \epsilon_A))} \\
  \jd{A:\sharp\type |- \mathsf{fse}:\mathsf{eisEquiv} (\factflat (\llbracket\eta_A\rrbracket \circ \epsilon_A))}
\end{gather}
This completes the axiomatization of the internal homotopy type theory of a cohesive \io-topos, yielding the formal system that we call \emph{cohesive homotopy type theory}.

\section{Quantum gauge field theory}
\label{sec:quantum}

We now
give a list of constructions in this axiomatics
whose interpretation in cohesive
$(\infty,1)$-toposes \H reproduces various notions in differential geometry,
differential cohomology, geometric quantization and quantum gauge field theory.
Because of the homotopy theory built into the type theory, this also automatically generalizes
all these notions to homotopy theory.  For instance, a
\emph{gauge group} in the following may be interpreted as an ordinary gauge group such
as the Spin-group, but may also be interpreted as a \emph{higher} gauge
group, such as the String-2-group or the Fivebrane-6-group \cite{SSS}.
Similarly, all fiber products are automatically homotopy fiber products, and so on.
(The fiber product of $f:[A,C]$ and $g:[B,C]$ is $A\times_C B \coloneqq \sum_{x:A}\sum_{y:B}(f(x)=g(y))$, and this can be externalized easily.)

In this section we will mostly speak ``externally'' about a cohesive \io-topos \H.
This can all be expressed in type theory using the technology of \S\ref{sec:axiomatic-cohesion-ii}, but due to space constraints we will not do so.

\subsection{Gauge fields}

The concept of a \emph{gauge field} is usefully decomposed into two stages, the \emph{kinematical}
aspect and the \emph{dynamical} aspect bulding on that:

\hspace{-.6cm}
\begin{tabular}{|r||c|c|}
  \hline
  {\bf gauge field:} & {\bf kinematics} & {\bf dynamics}
  \\
  \hline
  \hline
  physics  term: &
  instanton sector / charge sector
  & gauge potential
  \\
  \hline
  formalized as: & cocycle in (twisted) cohomology & cocycle in (twisted) differential cohomology
  \\
  \hline
     diff.\ geo.\
     term:
  &
  fiber bundle
  &
  connection
  \\
  \hline
  ambient logic:
  & homotopy type theory & cohesive homotopy type theory
  \\
  \hline
\end{tabular}

\subsubsection{Kinematics}

Suppose $A$ is a pointed connected type, i.e.\ we have $a_0:A$ and $\pi_0(A)$ is contractible.
Then its loop type $\Omega A \coloneqq * \times_A * \simeq (a_0 = a_0)$ is
a group. This establishes an equivalence between pointed connected homotopy types and
group homotopy types; its inverse is called
\emph{delooping} and denoted $G \mapsto \mathbf{B}G$.\footnote{Currently, we cannot fully formalize completely general $\infty$-groups and their deloopings, because they involve infinitely many higher homotopies.  This is a mere technical obstruction that will hopefully soon be overcome.
It is not really a problem for us, since we generally care more about deloopings than groups themselves, and pointed connected types are easy to formalize.}
For instance, the
\emph{automorphism group} $\mathbf{Aut}(V)$ of a homotopy type $V$ is the looping of the image factorization
\[\xymatrix{
    {*} \ar@{->>}[r] \ar@/_1pc/[rr]|{\;\vdash V\;} & \mathbf{B}\mathrm{Aut}(V) \ar@{^{(}->}[r] & \type
  }.\]
It can also be defined as the space of self-equivalences, $\mathbf{Aut}(V) = \sum_{f:[V,V]}\mathsf{isEquiv}(f)$; this is roughly the content of the univalence axiom.

Given a group $G$ and a homotopy type $X$, we write
$
H^1(X,G) \coloneqq
\pi_0 {\H(X,\mathbf{B}G)}
$
for the \emph{degree-1 cohomology} of $X$ with coefficients in $G$. If $G$ has higher
deloopings $\mathbf{B}^n G$, we write
$
H^n(X, G) \coloneqq
\pi_0 {\H(X,\mathbf{B}^n G)}
$
and speak of the \emph{degree-$n$ cohomology} of $X$ with coefficients in $G$.
The interpretation of this simple definition in homotopy type theory is very general,
and (if we allow disconnected choices of deloopings) much more general than what is traditionally called \emph{generalized cohomology}:
in traditional terms, it would be called \emph{non-abelian equivariant twisted sheaf hyper-cohomology}.

A  \emph{$G$-principal bundle} over $X$ is a function $p : P \to X$ where $P$ is
equipped with a $G$-action over $X$ and such that $p$ is the quotient $P \to P\ssl G$
(as always, this is a \emph{homotopy quotient}, constructible as a higher inductive type
~\cite{ShulmanLumsdaine,hottbook}
, see above.
One finds that the delooping $\mathbf{B}G$
is the \emph{moduli stack} of $G$-principal bundles: for any $g : X \to \mathbf{B}G$, its
(homotopy) fiber is canonically a $G$-principal bundle over $X$, and this establishes
an equivalence
$G \mathrm{Bund}(X) \simeq {\H(X,\mathbf{B}G)} $
between $G$-principal bundles and cocycles in \emph{$G$-cohomology}.
In particular, equivalence classes of $G$-principal bundles on $X$ are classified by $H^1(X,G)$.

Conversely, any $G$-action $\rho : G \times V \to V$ is equivalently encoded in
a fiber sequence
$
  \xymatrix@-1pc{
    V \ar[r] & V\ssl G \ar[r]^{\bar \rho}
  & \mathbf{B}G
  }
$,
hence in a $V$-fiber bundle $V\ssl G$ over $\mathbf{B}G$.
This is the \emph{universal $\rho$-associated} $V$-fiber bundle
in that, for $g$ and $P$ as above, the $V$-bundle $E \coloneqq P \times_G V \to X$
is equivalent to the pullback $g^* \bar \rho$.

Syntactically, this means that homotopy type theory in the context of a pointed connected type
$\mathbf{B}G$ is the \emph{representation theory} of $G$: the fiber sequence above
is the interpretation of a dependent type
$
  \jd{x : \mathbf{B}G |- V : \type}
$
which hence encodes a $G$-$\infty$-representation on a type $V$.
One finds that the dependent product
$
 \vdash( \prod_{x : \mathbf{B}G} V : \type)
$
is the type of \emph{invariants} of the $G$-action, while the dependent sum
$
  \vdash(\sum_{x : \mathbf{B}G} V : \type)
$
is the syntax for the quotient $V\sslash G$ mentioned above. Moreover, for $V_1, V_2$ two
such $G$-representations, the dependent product of their function type
$
  \vdash (\prod_{x : \mathbf{B}G} [V_1, V_2] : \type)
$
is interpreted as the type of $G$-action homomorphisms, while the dependent sum
$
  \vdash (\sum_{x : \mathbf{B}G} [V_1, V_2] : \type)
$
is interpreted
as
the quotient $[V_1, V_2]\sslash G$ of the space of all morphisms modulo
the \emph{conjugation action} by $G$. It follows that the homotopy type of sections
$\Gamma_X(E)$ above is the interpretation of the syntax
$\vdash (\prod_{x : \mathbf{B}G}  [P, V] : \type)$. Notice that this
expression reproduces almost verbatim the traditional statement that a section of a $\rho$-associated
$V$-bundle is a $G$-equivariant map from the total space $P$ to $V$, only that the
interpretation of this statement in homotopy type theory here generalizes it to higher bundles.

In particular, the
homotopy type of sections $\Gamma_X(E)$
of the associated bundle $E$ above is equivalent to the dependent product of the mapping
space $[g, \bar \rho]$ formed in the slice, the
homotopy type theory syntax for it being $\vdash( \prod_{x : \mathbf{B}G} [P, V] : \type)$.

Since all the bundles involved are locally trivial with respect to the intrinsic notion of
covers (epimorphic maps) it follows that
elements of $\Gamma_X(E)$ are locally maps to $V$. If $V$ here is pointed connected,
and hence $V \simeq \mathbf{B}H$, then $E$ is called an \emph{$H$-gerbe} over $X$.
In this case a section of $E \to X$ is therefore locally a cocycle in $H$-cohomology,
and hence globally a cocycle in \emph{$g$-twisted $H$-cohomology} with respect to the
\emph{local coefficient bundle} $E \to X$. Hence twisted cohomology in $\mathbf{H}$
is ordinary cohomology in a slice $\mathbf{H}_{/\mathbf{B}G}$. All this is discussed in
detail in \cite{NSS}.

In gauge field theory a group $H$ as above serves as the \emph{gauge group} and then
an $H$-principal bundle on $X$ is the charge/kinematic part of an \emph{$H$-gauge field} on $X$.
(In the special case that $H$ is a discrete homotopy type, this is already the full
gauge field, as in this case the dynamical part is trivial).
The mapping type $[X, \mathbf{B}H]$ interprets as the moduli stack of kinematic
$H$-gauge fields on $X$, and a term of identity type $\lambda :  (\phi_1 = \phi_2)$
is a \emph{gauge transformation} between two gauge field configurations $\phi_1, \phi_2: [X, \mathbf{B}H]$.

It frequently happens that the charge of one $G$-gauge field $\Phi$ \emph{shifts} another $H$-gauge field
$\phi$, in generalization of the way that magnetic charge shifts the electromagnetic field.
Such shifts are controlled by an action $\rho$ of $G$ on $\mathbf{B}H$ and in this case
$\Phi$ is a cocycle in $G$-cohomology and $\phi$ is a cocycle in $\Phi$-twisted $H$-cohomology
with respect to the local coefficient bundle $\bar \rho$.

An example of this phenomenon is given by the field configurations in Einstein-gravity
(general relativity). For this we assume that the \emph{general linear group} $\mathrm{GL}(n)$
in dimension $n$ exists as a group type, which is the case in the standard models for
smooth cohesion. Notably if we pass to a context of synthetic differential cohesion then
the first order infintesimal neighbourhood of the origin of $\mathbb{R}^n$ exists as a
type $D^n$ and we have $\mathrm{GL}(n) = \mathbf{Aut}(D^n)$. By the above, for an $n$-dimensional
smooth manifold $\Sigma$ (to be thought of as \emph{spacetime}) the frame bundle
$T \Sigma \to \Sigma$
is characterized as the type sitting
in a fiber sequence
$$
  \raisebox{20pt}{
  \xymatrix{
    T \Sigma \ar[r] & \Sigma \ar[d]
  \\
  & \mathbf{B}GL(n)
  }}
  \,,
$$
which syntactically is therefore the dependent type $\jd{x : \mathbf{B}GL(n) |- T \Sigma : \type}$.
Let then $\mathbf{B}O(n) \to \mathbf{B}\mathrm{GL}(n)$ be the delooping of the inclusion of the
maximal compact subgroup
\footnote{Assuming that we can talk about general colimits, which is
work in progress in fully formal HoTT, then geometric compactness can be axiomatized
as smallness with respect to filtered colimits whose structure maps are monomorphisms.}
, the
orthogonal group, into the general linear group. This sits in a homotopy fiber sequence
$$
  \raisebox{20pt}{
  \xymatrix{
    \mathrm{GL}(n)/O(n) \ar[r] & \mathbf{B}O(n) \ar[d]
  \\
  & \mathbf{B}\mathrm{GL}(n)
  }
  }
  \,,
$$
with the smooth coset space, exhibiting the canonical $\mathrm{GL}(n)$-action on that space.
Syntactically this is therefore the dependent type
$\jd{x : \mathbf{B}\mathrm{GL}(n) |- \mathrm{GL}(n)/O(n) : \type}$.
With the above one finds then that the homotopy type theory syntax
$$
  \vdash\; \left(\prod_{x : \mathbf{B}\mathrm{GL}(n)} [T \Sigma, \mathrm{GL}(n)/O(n)] : \type\right)
$$
is interpreted as the space of diagrams
$$
  \Gamma_{\Sigma}(T \Sigma \times_{GL(n)} \mathrm{GL}(n)/O(n))
  =
  \left\{
   \raisebox{20pt}{
  \xymatrix{
    \Sigma \ar[rr]_{\ }="s" \ar[dr]^{\ }="t" && \mathbf{B}O(n) \ar[dl]
  \\
  & \mathbf{B}\mathrm{GL}(n)

  \ar@{=>} "s"; "t"
  }}
  \right\}
  \,.
$$
Here $T \Sigma \times_{\mathrm{GL}(n)} \mathrm{GL}(n)/O(n)$ denotes the $(\mathrm{GL}(n)/O(n))$-bundle associated to the frame bundle (so $\times_{\mathrm{GL}(n)}$ denotes not a pullback but a tensor product over $\mathrm{GL}(n)$-actions).
The homotopy type theory syntax here is manifestly the expression for $\mathrm{GL}(n)$-equivariant maps from the
frame bundle to the coset, while the diagram manifestly expresses a reduction of the
structure group of the frame bundle to an $O(n)$-bundle. Both of these equivalent
constructions encode a choice of \emph{vielbein}, hence of a \emph{Riemannian metric}
on $\Sigma$, hence of a field of gravity. (We could just as well discuss
genuine pseudo-Riemannian metrics.) Moreover, by the homotopy-theoretic construction
this space of fields automatically contains the $O(n)$-gauge transformations on the vielbein
fields corresponding to choices of \emph{reference frames}.
But since gravity is a \emph{generally covariant} field theory,  the correct
configuration space of gravity is furthermore the \emph{quotient} of this space of
vielbein fields by the diffeomorphism action on $T \Sigma$. One finds from the above that
in homotopy type theory syntax this is simply expressed by interpreting the
space of fields in the context of the delooped automorphism group of $\Sigma$
and then forming the dependent sum:
the interpretation of
$$
  \vdash\;\left( \prod_{x : \mathbf{B}\mathrm{GL}(n)} \;\sum_{y : \mathbf{B}\mathbf{Aut}(T \Sigma)}
    [T \Sigma, \mathrm{GL}(n)/O(n)] : \type\right)
$$
is the moduli stack of the generally covariant field of gravity. In the
smooth context it is the Lie integration of the gravitational (off-shell) BRST complex with diffeomorphism
ghosts in degree 1.

Further discussion of examples and further
pointers are in \cite{SchreiberLectures, SchreiberErlangen}.

\subsubsection{Dynamics}
\label{Dynamics}

Given a $G$-principal bundle in the presence of cohesion, we may ask if its cocycle $g : X \to \mathbf{B}G$
lifts through the counit $\epsilon_{\mathbf{B}G} : \flat \mathbf{B}G \to \mathbf{B}G$
from (\ref{flatCounit}) to a cocycle
$\nabla : X \to \flat \mathbf{B}G$. By the $(\Pi \dashv \flat)$-adjunction this is equivalently
a map $\Pi(X) \to \mathbf{B}G$. Since $\Pi(X)$ is interpreted as the \emph{path $\infty$-groupoid}
of $X$, such a $\nabla$ is a \emph{flat parallel transport} on $X$ with values in $G$, equivalently
a \emph{flat $G$-principal connection} on $X$.

Consider then the homotopy fiber
$
  \flat_{\mathrm{dR}} \mathbf{B}G \coloneqq \flat \mathbf{B}G \times_{\mathbf{B}G} {*}
$.
By definition,
a map $\omega : X \to \flat_{\mathrm{dR}} \mathbf{B}G$ is a
flat $G$-connection on $X$ together with a trivialization of the underlying
$G$-principal bundle. This is interpreted
as a \emph{flat $\mathfrak{g}$-valued differential form}, where $\mathfrak{g}$ is the \emph{Lie algebra}
of $G$. By using this definition in the statement of the above classification of $G$-principal bundles,
one finds that every flat connection
$\nabla : X \to \flat \mathbf{B}G$ is \emph{locally} given by a flat $\mathfrak{g}$-valued form:
$\nabla$ is equivalently a form $A : P \to \flat_{\mathrm{dR}} \mathbf{B}G$ on the total space
of the underlying $G$-principal bundle, such that this is $G$-equivariant in a natural sense.
Such an $A$ is interpreted as the incarnation of the connection $\nabla$
in the form of an \emph{Ehresmann connection} on $P \to X$.

Moreover, the coefficient $\flat_{\mathrm{dR}}\mathbf{B}G$ sits in
a long fiber sequence of the form
\[
  \xymatrix{
    G
   \ar[r]^-{\theta_G}
    &
    \flat_{\mathrm{dR}}\mathbf{B}G
   \ar[r]
  &
    \flat \mathbf{B}G
   \ar[r]^-{\epsilon_{\mathbf{B}G}}
  &
  \mathbf{B}G
  }
  \,.
\]
with the further homotopy fiber $\theta_{G}$
giving a canonical flat $\mathfrak{g}$-valued differential form on $G$. This is
the \emph{Maurer-Cartan form} of $G$, in that when interpreted in smooth homotopy types
and for $G$ an ordinary Lie group, it is canonically identified with the classical
differential-geometric object of this name. Here in cohesive homotopy type theory it
exists in much greater generality.

Specifically, assume that $G$ itself is once more
deloopable, hence assume that $\mathbf{B}^2 G$ exists. Then
the above long fiber sequence extends further to the right as
$
  \xymatrix{
    \flat \mathbf{B}G
   \ar[r]^-{\epsilon_{\mathbf{B}G}}
  &
  \mathbf{B}G
   \ar[r]^-{\theta_{\mathbf{B}G}}
  &
  \flat_{\mathrm{dR}} \mathbf{B}^2 G
  }
$, since $\flat$ is right adjoint.
This means, by the universal property of homotopy fibers, that if $g : X \to \mathbf{B}G$ is the
cocycle for a $G$-principal bundle on $X$, then the class of the differential form $\theta_{\mathbf{B}G}(g)$ is the \emph{obstruction} to the existence of a flat
connection $\nabla$ on this bundle. Hence
this class is interpreted as the \emph{curvature} of the bundle, and we interpret
the Maurer-Cartan form
$\theta_{\mathbf{B}G}$ of the delooped group $\mathbf{B}G$
as the \emph{universal curvature characteristic} for $G$-principal bundles.

This universal curvature characteristic is the key to the notion of non-flat connections,
for it allows us to define these in the sense of twisted cohomology as
\emph{curvature-twisted flat cohomology}.
There is, however, a choice involved in defining the universal curvature-twist, which depends
on the intended application. But in standard interpretations there is a collection
of types singled out, called the \emph{manifolds}, and the standard universal
curvature twist can then be characterized as a map
$i : \Omega^{2}_{\mathrm{cl}}(-,\mathfrak{g}) \to \flat_{\mathrm{dR}}\mathbf{B}^2 G$ out of a 0-truncated
homotopy type such that for all
manifolds $\Sigma$ its image under $[\Sigma,-]$ is epi, meaning that
$\Omega^2_{\mathrm{cl}}(\Sigma,\mathfrak{g}) \to [\Sigma, \flat_{\mathrm{dR}}\mathbf{B}^2 G]$
is an \emph{atlas} in the sense of geometric stack theory.

Assuming such a choice of universal curvature twists has been made, we may then define
the moduli
of general (non-flat) $G$-principal connections to be the homotopy fiber product
\[
  \mathbf{B}G_{\mathrm{conn}}
  \coloneqq
  i^* \theta_{\mathbf{B}G}
  =
  \mathbf{B}G \times_{\flat_{\mathrm{dR}} \mathbf{B}^2 G} \Omega^2(-,\mathfrak{g})
  \,.
\]
In practice one is usually interested in a canonical abelian (meaning arbitrarily deloopable, i.e.\ $E_\infty$)
group $A$ and the tower of delooping groups $\mathbf{B}^n A$ that it induces.
In this case we write
$
  \mathbf{B}^n A_{\mathrm{conn}}
  \coloneqq
  \mathbf{B}^n A \times_{\flat_{\mathrm{dR}} \mathbf{B}^{n+1} A} \Omega^{n+1}(-,A)
$.
When interpreted in smooth homotopy types and choosing the Lie group
$A = \mathbb{C}^\times$ or $= U(1)$ one finds that $\mathbf{B}^n A_{\mathrm{conn}}$
is the coefficient for \emph{ordinary differential cohomology}, specifically that it is presented
by the $\infty$-stack given by the \emph{Deligne complex}.

Notice that the pasting law for homotopy pullbacks implies generally that the restriction of
$\mathbf{B} G_{\mathrm{conn}}$ to
vanishing curvature indeed coincides with the universal flat coefficients:
$\flat \mathbf{B}G \simeq \mathbf{B}G_{\mathrm{conn}} \times_{\Omega^2(-,\mathfrak{g})} \{*\}$.
This means that we obtain a factorization
of $\epsilon_{\mathbf{B} G}$ as $\flat \mathbf{B}G \to \mathbf{B}G_{\mathrm{conn}} \to \mathbf{B}G$.

Let then $G$ be a group which is not twice deloopable, hence to which the above universal definition
of $\mathbf{B}G_{\mathrm{conn}}$ does not apply. If we have in addition a map
$\mathbf{c} : \mathbf{B}G \to \mathbf{B}^n A$ given (representing a
universal characteristic class in
$H^n(\mathbf{B}G, A)$), then we may still ask for \emph{some} homotopy type
$\mathbf{B}G_{\mathrm{conn}}$ that supports a \emph{differential refinement}
$
 \mathbf{c}_{\mathrm{conn}} : \mathbf{B}G_{\mathrm{conn}} \to \mathbf{B}^n A_{\mathrm{conn}}
$
of
$\mathbf{c}$
in that it lifts the factorization of $\epsilon_{\mathbf{B}^n A}$ by
$\mathbf{B}^n A_{\mathrm{conn}}$.
Such a $\mathbf{c}_{\mathrm{conn}}$ interprets, down on cohomology, as a
\emph{secondary universal characteristic class} in the sense of refined Chern-Weil theory.
Details on all this are in \cite{FSSt, SchreiberCohesion}.

With these choices and
for $G$ regarded as a gauge group, a genuine \emph{$G$-gauge field} on $\Sigma$ is a map
$\phi : \Sigma \to \mathbf{B}G_{\mathrm{conn}}$. For $G$ twice deloopable, the \emph{field strength}
of $\phi$ is the
composite
$F_{\phi} : \Sigma \to \mathbf{B}G_{\mathrm{conn}} \xrightarrow{F_{(-)}} \Omega^2_{\mathrm{cl}}(-,\mathfrak{g})$.

Moreover, the choice of $\mathbf{c}_{\mathrm{conn}}$ specifies an exended \emph{action functional}
on the moduli type $[\Sigma, \mathbf{B}G_{\mathrm{conn}}]$ of $G$-gauge field configurations, and hence
specifies an actual quantum gauge field theory. This we turn to now.

\subsection{$\sigma$-Model QFTs}

An $n$-dimensional (``nonlinear'')
\emph{$\sigma$-model} quantum field theory describes the dynamics of an $(n-1)$-dimensional
quantum ``particle'' (for instance an electron for $n = 1$, a string  for $n = 2$, and generally
an ``$(n-1)$-brane'') that propagates in a \emph{target space} $X$
(for instance our spacetime) while acted on by forces (for instance the \emph{Lorentz force})
exerted by a fixed background $A$-gauge field on $X$
(for instance the electromagnetic field for $n = 1$ or the \emph{Kalb-Ramond $B$-field} for $n = 2$
or the \emph{supergravity $C$-field} for $n = 3$).
By the above, this background gauge field is the interpretation of a map
$
  \mathbf{c}_{\mathrm{conn}}
    : X \to  \mathbf{B}^n A_{\mathrm{conn}}
$.

Let then $\Sigma$ be a cohesive homotopy type of \emph{cohomological dimension} $n$,
to be thought of as the abstract \emph{worldvolume} of the $(n-1)$-brane.
The homotopy type $[\Sigma,X]$ of cohesive
maps from $\Sigma$ to $X$ is interpreted as the moduli space of field configurations of the
$\sigma$-model for this choice of shape of worldvolume.
The (gauge-coupling part of) the \emph{action functional} of the $\sigma$-model is
then to be the \emph{$n$-volume holonomy} of the background gauge field over a given
field configuration $\Sigma \to X$.

To formalize this, we need the notion of \emph{concreteness}.
If $X$ is a cohesive homotopy type, its \emph{concretization} is the image factorization
$X \twoheadrightarrow \mathrm{conc} X \hookrightarrow \sharp X$
of $\eta_X:X\to \sharp X$ (\ref{SharpUnit}).
We call $X$ \emph{concrete} if $X \to \mathrm{conc}\,X$ is an equivalence.
In the standard smooth model, the 0-truncated concrete
cohesive homotopy types are precisely the \emph{diffeological spaces} (see~\cite{SmoothSpaces}).
Generally, for models over \emph{concrete sites}, they are the \emph{concrete sheaves}.

Now we can define the \emph{action functional} of the $\sigma$-model associated
to the background gauge field $\mathbf{c}_{\mathrm{conn}}$ to be the composite
$$
  \exp(i S(-))
    :
  \xymatrix{
    [\Sigma, X]
  \ar[rr]^-{[\Sigma, \mathbf{c}_{\mathrm{conn}}]}
  &&
  [\Sigma, \mathbf{B}^n A_{\mathrm{conn}}]
  \ar[r]
  &
  \mathrm{conc}\,\pi_0 [\Sigma, \mathbf{B}^n A_{\mathrm{conn}}]
  }
  \,.
$$
In the standard smooth model, with $A = \mathbb{C}^\times$ or
$U(1)$, the second morphism is \emph{fiber integration in differential cohomology}
$\exp(2 \pi i \int_{\Sigma}(-))$.
For $n = 1$ this computes the line holonomy of a circle bundle with connection,
hence the correct gauge coupling action functional of the 1-dimensional $\sigma$-model; for
$n = 2$ it computes the surface holonomy of a circle 2-bundle, hence the
correct ``WZW-term'' of the string; and so on.

Traditionally, $\sigma$-models are thought of as having as target space $X$ a manifold
or at most an orbifold. However, since these are smooth homotopy $n$-types for $n \leq 1$, it is natural to
allow $X$ to be a general cohesive homotopy type.
If we do so, then a variety of
quantum field theories that are not traditionally considered as $\sigma$-models become
special cases of the above general setup.
Notably, if $X = \mathbf{B}G_{\mathrm{conn}}$ is
the moduli for $G$-principal connections, then a $\sigma$-model with target space $X$ is
a $G$-gauge theory on $\Sigma$. Moreover, as we have seen above, in this case the background
gauge field is a secondary universal characteristic invariant. One finds that the corresponding
action functional
$
 \exp(2 \pi i \int_\Sigma [\Sigma, \mathbf{c}_{\mathrm{conn}}])
 : [\Sigma, \mathbf{B}G_{\mathrm{conn}}] \to A
$
is that of \emph{Chern-Simons}-type gauge field theories \cite{FSS, CS},
including the standard 3-dimensional Chern-Simons theories as well a
various higher generalizations.

More generally, at least in the smooth model, there is a \emph{transgression} map for
differential cocycles: for
$\Sigma_d$ a manifold of dimension $d$ there is a canonical map
$$
  \exp(2 \pi i \int_{\Sigma}[\Sigma,\mathbf{c}_{\mathrm{conn}}])
  :
  \xymatrix{
    [\Sigma_d, X]
  \ar[rr]^-{[\Sigma_d, \mathbf{c}_{\mathrm{conn}}]}
  &&
  [\Sigma_d, \mathbf{B}^n A_{\mathrm{conn}}]
  \ar[rr]^{\exp(2 \pi i \int_\Sigma)}
  &&
  \mathbf{B}^{n-d} A_{\mathrm{conn}}
  }
$$
modulating an $n$-bundle on the $\Sigma_d$-mapping space. For $d = n-1$ and
quadratic Chern-Simons-type theories this turns out to be the (off-shell)
prequantum bundle of the QFT. See \cite{FSS} for details on these matters.
Thus the differential characteristic
cocycle $\mathbf{c}_{\mathrm{conn}}$ should itself be regarded as a
\emph{higher prequantum bundle}, in the sense we now discuss.

\subsection{Geometric quantization}
\label{GeometricQuantization}

Action functionals as above are supposed to induce $n$-dimensional \emph{quantum} field theories
by a process called \emph{quantization}. One formalization of what this means is
\emph{geometric quantization}, which is well-suited to formalization in
cohesive homotopy type theory. We indicate here how to formalize the spaces of
higher (pre)quatum states that an extended QFT assigns in codimension $n$.

The \emph{critical locus} of a
local action functional -- its \emph{phase space} or
\emph{Euler-Lagrange solution space} -- carries a canonical closed 2-form $\omega$,
and standard geometric quantization gives a method for constructing the
\emph{space of quantum states} assigned by the QFT in dimension $n-1$
as a space of certain sections of a
\emph{prequantum bundle} whose curvature is $\omega$.
This works well for non-extended topological quantum field theories and generally for
$n = 1$ (quantum mechanics). The generalization to $n \geq 2$ is
called \emph{multisymplectic} or \emph{higher symplectic geometry} \cite{CR},
for here $\omega$ is promoted to an $(n+1)$-form which reproduces the former 2-form
upon transgression to a mapping space. Exposition of the string $\sigma$-model
($n = 2$) in the context of higher symplectic geometry is in \cite{BHR},
and discussion of quantum Yang-Mills theory ($n = 4$)
and further pointers are in \cite{Kan}.
A homotopy-theoretic formulation is given in \cite{SchreiberErlangen}: here the prequantum
bundle is promoted to a prequantum $n$-bundle, a $(\mathbf{B}^{n-1}A)$-principal connection
as formalized above.

Based on this we can give a formalization of central ingredients of geometric quantization in
cohesive homotopy type theory. When interpreted in the standard smooth model with $A = \mathbb{C}^\times$ or $= U(1)$ the following reproduces the traditional notions for $n = 1$, and for $n \geq 2$ consistently generalizes them to higher
geometric quantization.

Let $X$ be any cohesive homotopy type. A closed $(n+1)$-form on $X$ is a map
$\omega : X \to \Omega^{n+1}_{\mathrm{cl}}(-,A)$, as discussed in section \ref{Dynamics}.
We may call the pair $(X, \omega)$ a \emph{pre-$n$-plectic} cohesive homotopy type.
The group of \emph{symplectomorphisms} or \emph{canonical transformations} of $(X, \omega)$
is the automorphism group of $\omega$:
\[
    \mathbf{Aut}_{/\Omega^{n+1}_{\mathrm{\mathrm{cl}}}(-, A)}(\omega)
  =
  \left\{
    \raisebox{20pt}{
    \xymatrix{
       X \ar[rr]^{\simeq} \ar[dr]_{\omega} && X \ar[dl]^{\omega}
     \\
     & \Omega^{n+1}_{\mathrm{cl}}(-,A)
    }
    }
  \right\}
  \,,
\]
regarded as an object in the slice
$\mathbf{H}_{/\Omega^{n+1}_{\mathrm{cl}}(-,A)}$.
A \emph{prequantization} of $(X,\omega)$ is a lift
\[
 \raisebox{18pt}{
  \xymatrix{
      & \mathbf{B}^n A_{\mathrm{conn}}
    \ar[d]^{F_{(-)}}
     \\
     X \ar[ur]^-{\mathbf{c}_{\mathrm{conn}}} \ar[r]^-\omega & \Omega^{n+1}_{\mathrm{cl}}(-,A)
  }
  }
\]
through
the defining projection from the moduli of $(\mathbf{B}^{n-1}A)$-principal connections.
This $\mathbf{c}_{\mathrm{conn}}$ modulates the \emph{prequantum $n$-bundle}.
Since $A$ is assumed abelian, there is abelian
group structure on $\pi_0(X \to \mathbf{B}^n A_{\mathrm{conn}})$ and hence we may rescale
$\mathbf{c}_{\mathrm{conn}}$ by a natural number $k$.
This corresponds to rescaling \emph{Planck's constant} $\hbar$ by $1/k$. The limit $k \to \infty$
in which $\hbar \to 0$ is the \emph{classical limit}.

The automorphism group of the prequantum bundle
\[
   \mathbf{Aut}_{/\mathbf{B}^n A_{\mathrm{conn}}}(\mathbf{c}_{\mathrm{conn}})
  :=
  \left\{
    \raisebox{20pt}{
    \xymatrix{
      X \ar[rr]^{\sigma}_{\ }="s" \ar[dr]_{\mathbf{c}_{\mathrm{conn}}}^{\ }="t" & & X \ar[dl]^{\mathbf{c}_{\mathrm{conn}}}
    \\
    & \mathbf{B}^n A_{\mathrm{conn}}

    \ar@{=>}^\simeq "s"; "t"
    }
    }
  \right\},
\]
in the slice $\mathbf{H}_{/\mathbf{B}^n A_{\mathrm{conn}}}$,
is the \emph{quantomorphism group} of the system.
Syntactically this is
$$
  \vdash\; \left(\prod_{\nabla : \mathbf{B}^n A_{\mathrm{conn}}}
    \mathbf{Aut}(X(\nabla))
  :
  \type
  \right).
$$
See \cite{SchreiberErlangen} for more on this.

There is an evident projection from the
quantomorphism group to the symplectomorphism group, and its image is the group of
\emph{Hamiltonian symplectomorphisms}.
The Lie algebra of the quantomorphism group is that of
\emph{Hamiltonian observables} equipped with the \emph{Poisson bracket}.
If $X$ itself has abelian group structure,
then the subgroup of the quantomorphism group covering the action on $X$ on itself is the
\emph{Heisenberg group} of the system.
An action of any group $G$ on $X$ by quantomorphisms, i.e.\ a map
$\mu : \mathbf{B}G \to \mathbf{B}\mathbf{Aut}_{/\mathbf{B}^n A_{\mathrm{conn}}}(\mathbf{c}_{\mathrm{conn}})$,
is a \emph{Hamiltonian $G$-action} on $(X,\omega)$. The (homotopy) quotient
$\mathbf{c}_{\mathrm{conn}}\ssl G : X \ssl G \to \mathbf{B}^n A_{\mathrm{conn}}$ is the
corresponding \emph{gauge reduction} of the system.

After a choice of representation $\rho$ of $\mathbf{B}^{n-1}A$ on some $V$, the
space of \emph{prequantum states} is
\[
 \Gamma_X(E)
   \coloneqq
  [\mathbf{c}, \mathbf{p}]_{/\mathbf{B}^n A}
  =
  \left\{
    \raisebox{20pt}{
    \xymatrix{
      X \ar[rr]^{\sigma}_{\ }="s" \ar[dr]_{\mathbf{c}}^{\ }="t" & & V \ssl {\mathbf{B}^{n-1}A}
    \ar[dl]^{\bar \rho}
    \\
    & \mathbf{B}^n A

    \ar@{=>}^\simeq "s"; "t"
    }
    }
  \right\},
\]
the space of $\mathbf{c}$-twisted cocycles with respect to the local coefficient bundle
$\bar \rho$.
There is an evident action of the quantomorphism group on $\Gamma_X(E)$
and this is the action of \emph{prequantum operators} on the space of states.

It remains to formalize in cohesive homotopy type theory
the quantization step from this \emph{pre}quantum data to actual quantized
field theory. This is discussed, in terms of standard homotopy theory and
$\infty$-topos theory,  in \cite{NuitenThesis},
to which we refer the reader for further details.
This quantization step involves, naturally, linear algebra, which
internal to homotopy theory
is \emph{stable homotopy theory}, the theory of spectra and
ring spectra. This has not been fully formalized in
homotopy type theory at the moment, but it seems clear that this can be done.
In any case, a discussion of the quantization step
in the language of homotopy type theory is possible, but
beyond the scope of this article.

\medskip

In conclusion then, the amount of gauge QFT notions naturally
formalized here in cohesive homotopy type theory seems to be remarkable,
emphasizing the value of a formal, logical, approach to concepts like
smoothness and cohomology.

\bibliographystyle{eptcs}

redpajama_set_name: RedPajamaArXiv


text:
Posts Tagged 'potions'
The Witchy Moon, Magic, and News
Wednesday, June 22nd, 2016
Wednesday, June 22, 2016: The moon phase is Waning Gibbous in the zodiac sign Capricorn until entering Aquarius at 4:08 PM EST.
Color: Topaz
Incense: Bay Laurel (see below for magical uses)
Garden Activities:
Plow, Cultivate, and weed.
Plant onions, potatoes, rhubarb, grapes, winter wheat, and berries.
Herbal Magic – Bay Laurel
(Laurus nobilis) G
Folk Names: Baie, Bay Tree, Daphne, Grecian Laurel, Sweet Bay, Laurel, Laurier d'Apollon, Laurier Sauce Lorbeer, Noble Laurel, Roman Laurel
Deities: Aesculapius, Apollo, Ceres, Faunus, Eros
Planet: Sun (Healing, Legal Matters, Protection)
Element: Fire (Courage, Exorcism, Health, Lust, Strength, Protection)
Powers: Healing, Protection, Psychic Powers, Purification, Strength
Lore: Hermes invented fire by striking a pomegranate against a bay laurel. It is also sacred to Apollo and Zeus.
Magical and Ritual Uses:
For Psychic Powers: Burn with Frankincense on charcoal. It can also be placed beneath your pillow for prophetic dreams.
For Protection: Carry a Bay leaf in a mojo bag to ward off evil, negativity, and unwanted people. Place around windows and in the attic to prevent lightening. A potted bay is also used to protect against storms and invoking the protection of Apollo. Wearing a wreath of bay is used to conquer one's fear of thunderstorms.
To Remove a Curse or Evil Spirits: Mix with Sandalwood and burn over charcoal.
To Attract Love or Romance: Use in a fire sacrifice to the gods. The oil can also be extracted and used to dress a candle which is then burned.
For Victory: Take three fresh Bay leaves and write the names of Archangels Michael, Gabriel, and Raphael on each leaf, then wrap the leaves in white cloth and carry them.
Dabble In Magic Using This Handbook Of Witchcraft
There was a time when choosing to invoke an incantation as a means to an end would get one burnt at the stake. In today's world, taboos seem to be falling like leaves in autumn. So one need not be fearful any longer when choosing to resort to witchcraft in a time of need.
If the thought of dabbling in witchcraft has piqued your curiosity, you are in luck. There is a new handbook you should find very useful. It is titled Witchcraft: A Handbook of Magic, Spells and Potions. This beautifully bound book includes wonderful illustrations. Read full story – huffingtonpost.com
Llewellyn's Magical Almanac
Llewellyn's 2016 Moon Sign Book: Conseious Living by the cycles of the moon
Catherine Yronwode: Hoodoo Herb and Root Magic
Paul Beyerl: A Compendium of Herbal Magick
Scott Cunningham: Cunningham's Encyclopedia of magical herbs
Tags: Bay Laurel, Healing, Herbs, Incantation, Magic, Moon, Moon phase, potions, Protection, Psychic powers, Purification, Ritual, rituals, Spells, Strength, withcraft
Posted in Opinions, Pagan News, Site Updates | Comments Off
News & Submissions 12/30/2010
Dark future for wrong psychics
There are many things to dislike about end-of-year celebrations — the pressure to make New Year's Eve memorable, the shameful amounts of money wasted on fireworks, drunken renditions of Auld Lang Syne. But perhaps the most annoying tradition is the value placed on predictions made by psychics.
According to a 2009 Neilsen poll, 49 per cent of Australians believe in psychic powers, despite — it must be pointed out — a distinct lack of supporting evidence.
However, as 2010 draws to a close, we have a unique chance to put some of these beliefs to the test by reflecting on the accuracy of psychic predictions made at the start of the year. After all, the rest of us face performance reviews at this time of the year, so why not critically appraise clairvoyants as well? Read full story from haroldsun.com
January, New Year and the Compitalia
For many people, after the December festivities January comes as a quite a gloomy anti-climax. However, Classical Pagans (i.e. those following a Roman/Greek pantheon) perceive the world with somewhat different eyes.
Subsequent to the festivities of Yuletide and the Midwinter Solstice, or Christmas – if one subscribes to the more recent Christian ethos, we swiftly arrive at the start of another contemporary year. I accentuate the word 'contemporary' because calendars have so frequently changed over the centuries.
The bucolic, pre-Christian, Celtic land dwellers regarded the period we now call Halloween (originally Samhain) as the end of summer and commencement of winter. It marked the start of the New Year.
When we disregard the 'man-made' calendar and take a long look at nature's moods, this old agricultural method of time calculation begins to make a great deal of sense. Read full story from ufodigest
Secular Coalition Calls for Email Campaign to Mayor-Elect Gray
December 29, 2010 (Washington, D.C.) – The Secular Coalition for America (SCA) is calling for an email campaign by all D.C. residents to let Mayor-Elect Vincent Gray know that discrimination in any form, for any reason is unacceptable.
CLICK HERE TO SEND A MESSAGE TO MAYOR-ELECT VINCENT GRAY.
The efforts come one day after SCA went public with the decision from the mayor-elect's transition team to exclude a secular representative for atheists, agnostics, humanists, and other nontheistic Washington, D.C. residents at his first official inaugural event—an ecumenical service entitled "One City … Praying Together" at 8 a.m. Sunday, January 2, 2011. Read full story from richarddawkins.com
Seven arrested for killing man over witchcraft
Seven people were arrested at Thabine village outside Tzaneen on Thursday after a man accused of practising witchcraft was stoned to death, Limpopo police said. Read full story from thenewaga.co.za
Man banished from Busia village over witchcraft
RESIDENTS of Buwhera village in Buyanga sub-county in Busia district have banished a man from their village for allegedly practicing witchcraft.
Robert Barasa, 24, was banished from the village after a meeting held at Buwhera on Tuesday. Karim Sityabude, who is field operations chief of the Uganda traditional healers Busia Chapter, was present at the meeting. Read full story from newvision.co.ug
Yes, Virginia, Hellenes Have Christmas Traditions
Two decades ago, Ann Landers did a column about how various cultures celebrate Christmas. Halfway down her list was this gem: "If you are Greek Orthodox, your sect celebrates Christmas on January 7." Several people wrote back that 1) the Orthodox church is not a sect — it is the original church from which the Catholic one split after the Schism of 1054 and 2) only the so-called Old Believers track Christmas by the Julian calendar.
I was reminded of this when I was leaving work a week ago, and a colleague asked, "Should I wish you Merry Christmas? I heard you Greeks don't celebrate it like we do." As those who read my posts know, I'm an atheist who misses many of my culture's old customs, particularly those that thrum with pagan echoes. So I'm going to put my tour guide's hat briefly on, and tell you what we Hellenes do around the time of the winter solstice. Read full story from huffingtonpost.com
Need a Job? Losing Your House? Who Says Hoodoo Can't Help?
Jennifer Forness, a 39-year-old in Groton, Conn., felt her life falling apart earlier this year. Her husband announced he wanted a divorce. She lost her job as a store clerk. She developed health problems from the stress.
Then one night she discovered a website selling products for hoodoo—an ancient belief system based on spells, potions, balms and curses that slaves developed long ago in the Deep South. Ms. Forness ordered several items and instructions for performing certain rituals. She also had a telephone session with a hoodoo "doctor" who specializes in employment matters. Read full story from wsj.com
Forecasters keep eye on looming 'Solar Max'
PARIS, France — The coming year will be an important one for space weather as the Sun pulls out of a trough of low activity and heads into a long-awaited and possibly destructive period of turbulence.
Many people may be surprised to learn that the Sun, rather than burn with faultless consistency, goes through moments of calm and tempest.
But two centuries of observing sunspots — dark, relatively cool marks on the solar face linked to mighty magnetic forces — have revealed that our star follows a roughly 11-year cycle of behaviour.
The latest cycle began in 1996 and for reasons which are unclear has taken longer than expected to end.
Now, though, there are more and more signs that the Sun is shaking off its torpor and building towards "Solar Max," or the cycle's climax, say experts. Read full story from google.com
Christ In Woman's Chest X-ray (source abc news)
Tags: Agnostic, Atheist, Christ, Compitalia, curses, Hellenes, Hoodoo, humanist, New Year, Pagan, potions, Psychics, Secular Coalition, Solar Max, Spells, witchcraft, Yuletide
All Christians 'targets,' Iraqi militant group says
Baghdad, Iraq (CNN) — All Christians in the Middle East are now "legitimate targets," al Qaeda in Iraq announced Wednesday, as the group's deadline for Egypt's Coptic church to release alleged Muslim female prisoners expired.
An audio message released Monday gave the church 48 hours to disclose the status of Muslim women it said are imprisoned in Coptic churches in Egypt. Read full story from cnn.com
Christian holiday celebrations are out of date
John Philips (Write Back, November 1) states that Christianity "cleverly sanitised" pagan festivals in spring and mid-winter into Easter and Christmas.
While these festivals may have been "sanitised", it was not that "clever". Many of the pagan rituals remain in these festivals, including the use of evergreen decorations, such as holly, ivy, mistletoe and pine trees. Read full story from belfasttelegraph.co.uk
5,000-year-old practice comes around again
Unlike a maze, which includes dead ends and tall walls that are meant to confuse, a labyrinth traces a single path that leads inexorably to the center. It has ancient roots in pagan pre-Christian beliefs, Celtic traditions, and even Wicca, and many consider it a spiritual journey to walk one. Read full story from philly.com
Chief Oshkosh controversy brings back painful memories
OSHKOSH, Wis. – The decision by the mayor of Oshkosh, Wis., to use the name and image of Chief Oshkosh to promote beer drinking in his tavern highlights long-standing cultural dissonances between Natives and non-Natives. Though less than one percent of the population of Oshkosh is Native American, its proximity to the Menominee Nation of Wisconsin has made the mayor's promotion a focus of the ongoing controversy over how and by whom names and images of Native American leaders may be used. Read full story from indiancountrytoday.com
Mexicans Seek Charms, Potions To Ward Off Bad Luck
The Sonora Market near the center of Mexico City is a labyrinth of narrow alleyways that wind between overstuffed stalls where the air is thick with sage smoke. One entire section is known as the mercado de brujeria, or the "witchcraft market."
In a country facing tough times, Mexicans come to the market to buy potions, herbs and charms that supposedly will bring good luck and protection. Read full story from minesotapublicradio.org
Journey Through the Afterlife: Ancient Egyptian Book of the Dead – review
Statues are speaking at the British Museum. The dead are coming to life. The statue in front of me is a small painted wooden figure of the god Osiris, just over half a metre high, in a glass case in one of the first rooms of this engrossing exhibition. It is instantly striking, because of the bright green of its face and hands, but its verbal eloquence lies hidden inside. Read full story from guardian.co.uk
Carving a contemporary tribute to history
NIWOT, Colo. – Annual Nostalgia Days festivities in this community north of metro Denver recall the past for the area's original descendants as well as for those whose 19th century ancestors settled here.
An eagle capture was depicted in a massive carving dedicated at the high point of a celebration for area residents and Northern Arapaho tribal members from the Wind River Reservation, in Wyoming. Noted Arapaho leader, Niwot (Left Hand), gave the town its name and brokered a temporary peace with white settlers in the gold rush era. Read full story from indiancountrytoday.com
Sacred Spaces: inside a Buddhist fire rite ceremony (source cnn.com)
Tags: afterlife, Book of the dead, Buddhism, charms, Chief Oshkosh, Christian, Egyptian, labyrinth, Mexicans, Native American, Pagan, potions, Wicca, Witch, witchcraft

redpajama_set_name: RedPajamaCommonCrawl


A lot of bling and bang for your buck.
Cooler Master is known for its PC cases, power supplies, and as its name implies, CPU coolers, but it also makes peripherals as well. The CM310 (See it at Amazon) is Cooler Master's first-ever gaming mouse, and it features RGB backlighting, an "ambidextrous" ergonomic design, and a Pixart A3325 "gaming grade" optical sensor. Despite these ritzy features it's only $30, so it's surprisingly affordable.
Before I dive into this review, I'd like to acknowledge a passage from the CM310 webpage, which both sets the stage for this product's market positioning and provides my all-time favorite sentence ever published in mouse marketing: "The choice for gamers of all levels, providing unassuming dependability and reliability without asking for much - like that one nice guy who's been friend-zoned but sticks around 'just in case.'" Thanks for the chuckle, Cooler Master.
Like most gaming peripherals, the CM310 is matte black. An RGB strip lines the perimeter of the mouse just under its top panel. Below the backlit scroll wheel are three buttons: the top and bottom buttons scroll through seven preset DPI settings, and the middle button changes the lighting preset. The rear of the mouse features a Cooler Master logo, backlit in the same color as the scroll wheel. The sides of the mouse have rubber grips, and if you flip it over and you'll find two plastic feet and the Pixart A3325 sensor.
In Cooler Master's reviewer's guide, the company states that the CM310 has an "ambidextrous grip." This spurred a semantics battle in my brain. While the mouse does have a symmetrical shape, it only has thumb buttons on its left side. A true ambidextrous mouse features matching buttons on both sides, or no buttons on either side. Therefore, the CM310 is definitely a right-handed mouse, albeit one with a symmetrical shape.
In order to cater to both palm-grip and claw-grip gamers, the CM310 has a slight indent where the tips of your fingers should touch the left/right buttons. Playing with both styles, I found the indents did make it easier to use either grip. Typically I use a half-palm, half-claw style when playing normally and standard claw when sniping.
The CM310 does not use any software. For the DPI switching, there are seven pre-installed DPI settings: 500, 1000, 2000, 3000, 4000, 5000, and 10,000. You can also switch between five lighting presets by pressing the middle button. Here's how the lighting presets work: lighting 1 is the "rainbow mode" present on almost every gaming peripheral, lighting 2 makes the backlight match the scroll wheel (which indicates your DPI setting), lighting 3 is a "breathing" version of setting 2, lighting 4 cycles through colors with a breathing effect, and lighting 5 has different colors shoot along the sides of the mouse. Personally, I thought 1 and 5 looked the best.
Is the absence of a driver utility good or bad? Well, if you're fond of programming macros and having complete functional control, it's bad. If you don't like to hassle with confusing software, which mice and keyboard software can be, it's probably good. The CM310 offers a reasonable range of rainbow-tinted foofaraw without relying on software. This appeals to my minimalist tendencies, especially since I can still plug macros into our gaming keyboard. It does limit your options for customization, but at this price it's not shocking there's not a full-blown software suite available.
To test the CM310, I booted up Overwatch, Team Fortress 2, and Fortnite. Across all three games, the CM310 performed well. Clicks felt precise, and the mouse's plastic feet let it slide smoothly across both desk and mousepad alike. Switching DPI profiles on the fly was a bit tricky due to the rather large hump on the mouse's top where the buttons are located. I could reach the DPI up-and-down buttons with my first two fingers, but it was an awkward stretch. Still, while I only used two settings (500 and 1000 DPI), having the option to change modes on the fly was much appreciated.
I found the scroll wheel's notches to be quite useful, ensuring I never missed a weapon switch. I did find the textured rubber side grips to be a bit slippery – more slippery, in fact, than the rest of the mouse. For a $30 mouse, I got no jitter or any similar issues that seem to crop up in low-end mice when moving slowly. While I was somewhat skeptical of the "gaming grade sensor," (with the casual target audience, the line sounded like it was meant to lure the uninformed) it performed smoothly and consistently.
I think the only thing holding back this mouse is its shape, as I found using the CM310 for prolonged periods to be somewhat uncomfortable. While the symmetrical shape is advertised to be a benefit, I'm used to the ergonomic grooves found on right-handed gaming mice. Thus, the CM310's design felt unnatural and awkward. Another couple weeks of use might soften my stance on this, but after a week behind the (scroll) wheel, using the CM310 still felt a bit weird.
The Cooler Master CM310 is a great first attempt from Cooler Master. It features slick RGB lighting, seven adjustable DPI settings, and a notched scroll wheel. At this price, you can't ask for much more. While this mouse might not ever think of you as "more than just a friend", it's still a great budget pick.
Plenty of welcome features and a low price makes the Cooler Master CM310 a great budget-friendly gaming mouse.


Nathaniel Comfort finds heroism but little nuance in Jennifer Doudna's account of her co-discovery.
The prospect of a memoir from Jennifer Doudna, a key player in the CRISPR story, quickens the pulse. And A Crack in Creation does indeed deliver a welcome perspective on the revolutionary genome-editing technique that puts the power of evolution into human hands, with many anecdotes and details that only those close to her may have known. Yet it does not provide the probing introspection, the nuanced ethical analysis, the moral counterpoint that we CRISPR junkies crave.
After the race for discovery comes the battle for control of the discovery narrative. The stakes for the CRISPR–Cas system are extraordinarily high. In February, the US Patent and Trademark Office ruled against Doudna and the University of California, Berkeley. It found that a patent on the application of CRISPR to eukaryotic cells — filed by Feng Zhang of the Broad Institute of MIT and Harvard in Cambridge, Massachusetts — did not interfere with Berkeley's more sweeping patent on genetic engineering with CRISPR.
Although that battle is over, the war rages on. Berkeley has already appealed against the decision; meanwhile, the European Patent Office has ruled in favour of Doudna and Berkeley. Doubtless there are many more patents to milk out of this versatile system. And then there's the fistful of 66-millimetre gold medals they give out in Stockholm each year.
So far, the Broad Institute has controlled the CRISPR narrative. Rich in funds and talent, the Broad melds sleek, high-tech sexiness with a sense of East Coast, old-money privilege. Last year, institute director Eric Lander published a now-infamous piece entitled 'The heroes of CRISPR' (E. Lander Cell 164, 18–28; 2016). It adopted a tone of magnanimity, crediting Lithuanian biochemist Virginijus Siksnys with observing early on that his findings "pave the way for engineering of universal programmable RNA-guided DNA endonucleases", and Doudna and her CRISPR co-discoverer Emmanuelle Charpentier with noting "the potential to exploit the system for RNA-programmable genome editing".
Lander's clear implication was that they were laying the groundwork; Zhang's group got CRISPR over the finish line. To many of us, such tactics made Team Broad look like the villains of CRISPR.
Doudna's book was a chance to deliver a righteous knockout blow. Instead, we get a counter-narrative just as constructed as Lander's article. It is written entirely in the first person; co-author Samuel Sternberg, a former student in the Doudna lab, barely surfaces.
In that counter-narrative, Doudna had always been interested in gene editing. Her early work was on RNA enzymes, or ribozymes. She developed an impeccable pedigree, doing her PhD with Jack Szostak at Harvard and a postdoc with Tom Cech at the University of Colorado Boulder, before joining the faculty at Yale University in New Haven, Connecticut. From the mid-1990s, she writes, she was exploring the basic molecular mechanisms that "would be able to unlock the full potential of gene editing".
Her work on CRISPR dates to 2006 — six years before the key papers were published — and a call from Berkeley geomicrobiologist Jillian Banfield. Over coffee, Banfield described the clustered, regularly interspaced, short palindromic repeats that kept popping up in her DNA databases of bacteria and archaea. The sequences were ubiquitous among these prokaryotes, but unique to each species. This realization "sent a little shiver of intrigue down my spine", Doudna writes. If CRISPR was so widespread, "there was a good chance that nature was using it to do something important". By 2012, she and her co-workers had characterized the natural CRISPR system, harnessed it as a laboratory tool and developed a modified system that was programmable, cheap and easy to use.
The middle of the book reels off the obligatory breathless list of potential uses, generating everything from malaria-free mosquitoes and police dogs with muscles like Vin Diesel to the canonical cure for cancer. Thankfully, Doudna counterweights sensationalism with a sober accounting of the risks and responsibilities of applications such as altering the genomes of entire populations of organisms with 'gene drives'. In 2015, she sustained doubts about CRISPR ever being safe enough for clinical trials, but she has come to embrace editing of the human germ line — inheritable DNA modification — once it is proved safe.
But the discussion is ultimately unsatisfying. When it is time to "grapple with tricky ethical issues", such as human experimentation, she baulks, unspooling instead a series of rhetorical questions. Rather than guiding us through the ethical thickets of precision genetic engineering, or providing a candid, warts-and-all look at one of the great scientists of our time, the book mainly polishes her 'good scientist' image and rationalizes the unfettered self-direction of human evolution, within liberal bounds of safety, efficacy and individual choice.
Rather than dispel the cartoon-character feel of this epic battle, Doudna elaborates on it. She presents us with a persona so flawless that it seems more concealing than revealing. She waves away the bloody patent fight as a "disheartening twist" in the story, but the entire biomedical world knows that it was much more. As I read A Crack in Creation, I was reminded of Benjamin Franklin's "benevolent man", who, he wrote, "should allow a few faults in himself, to keep his friends in countenance" — and, I would add, to give him- or herself more depth.
The narrative often substitutes melodrama for dramatic tension. A conference in Puerto Rico sees Charpentier and Doudna strolling the cobbles of Old San Juan, with Charpentier saying earnestly, "I'm sure that by working together we can figure out the activity" of what became the Cas enzyme. "I felt a shiver of excitement as I contemplated the possibilities of this project," Doudna writes. When first wrestling with the ethical dilemmas of gene editing, she dreams of meeting Adolf Hitler, who demands to know the secrets of her technique. She wakes, of course, freshly determined to ensure that CRISPR is not put to nefarious use.
The larger purpose of A Crack in Creation, clearly, is to show that Doudna is the true hero of CRISPR. And ultimately, despite the book's flaws, I'm convinced. Nominators and the Nobel Committee will need to read this book. But CRISPR binge-watchers like me still await a truly satisfying account — one that is insightful, candid and contextualized.
Nathaniel Comfort is professor of the history of medicine at Johns Hopkins University in Baltimore, Maryland. He is working on a biography of DNA.


text:
Sixt Car Rental Partners with Singapore Airlines
March 25, 2013 • by Staff
Sixt Rent A Car announced a partnership with Singapore Airlines' frequent flyer program, KrisFlyer, on March 19.
Under the mileage crediting agreement, KrisFlyer members can earn a minimum of 500 miles with every Sixt car rental worldwide. Members can also earn 100 miles when they use Sixt's chauffeur service.
"Singapore Airlines is a worldwide well-known top brand and an ideal partner for the international Sixt family," said Regine Sixt, Senior Executive VP of Marketing. "We are very excited to be able to offer Singapore Airlines passengers our matching top-of-the-line products and services and making their travels even more comfortable and flexible on the ground."
Related news: Sixt Reports Rental Revenue Increase in 2012
Read more about Partnership Travel Industry Sixt air travel Singapore Loyalty Program


I think the lotus 24 in the listing is a typo. The backend of this car looks like a lotus 25 not a 24.
The Lotus 25 was a racing car designed by Colin Chapman for the 1962 Formula One season. It was a revolutionary design, the first fully stressed monocoque chassis to appear in F1. In the hands of Jim Clark it took 14 World Championship Grand Prix wins and propelled him to his 1963 World Championship title. Its last World Championship win was at the 1965 French Grand Prix.
Peter Revson was born into the Revlon Family, he was the nephew of Revlon Cosmetics industry magnate Charles Revson, he was an heir to his father Martin's fortune (reportedly worth over $1 billion).
Revson began racing in 1960 while at the University of Hawaii. He previously attended both Columbia University and Cornell University. Revson finished second in a local club event, driving a Plus Four Morgan. He proceeded in his racing career, becoming experienced in Formula cars, Trans-Am sedans, Can-Am Group 7 racers, GTs, and Indianapolis racers.
Peter Revson is also famous for Co-driving with Steve McQueen in the 1970 12 Hours of Sebring race, Revson and McQueen (driving with a cast on his left foot from a motorcycle accident two weeks earlier) won with a Porsche 908/02 in the 3 litre class and missed winning overall by 23 seconds to Mario Andretti/Ignazio Giunti/Nino Vaccarella in a 5-litre Ferrari 512S.


text:
Q: Parsing malformed json string which doesn't have double quotes around it (Java Script) { ValidationError: { device_uuid: [ [Object] ] } }

I like to convert this string to JSON format which will be like
{ "ValidationError": { "device_uuid": [ [Object] ] } }

Is there anyway that I can possibly get this result from malformed JSON string?

A: Assuming you're sure that the improperly formatted string is safe and is just malformed JSON (ie not going to execute any other javascript), you could just eval and then JSON.stringify it.
JSON.stringify(eval('(' + myString + ')'));

A: I've found really cool javascript library.
https://github.com/freethenation/durable-json-lint
It helped my malformed json string to wellformed json string!
durableJsonLint = require('durable-json-lint');
console.log(durableJsonLint('{name:"value", \'array\':[call(), 0x11]}'))
// The above code would print the following to the console
{
   "json":'{"name":"value", "array":[null, 17]}',
   "errors":[{
         "column":1,
         "description":"Keys must be double quoted in Json. Did you mean \"name\"?",
         "lineNumber":1,
         "status":"correctable"
      },{
         "column":15,
         "description":"Json strings must use double quotes",
         "lineNumber":1,
         "status":"correctable"
      },{
         "column":24,
         "description":"You can not make function calls in Json. Do you think I am a fool?",
         "lineNumber":1,
         "status":"fail"
      },{
         "column":32,
         "description":"Invalid Json number",
         "lineNumber":1,
         "status":"correctable"
      }
   ]
}

redpajama_set_name: RedPajamaStackExchange


text:
Hardback cover blurb
Paleontologist Richard Leyster has achieved professional nirvana: a position with the Smithsonian Museum plus a groundbreaking dinosaur fossil site he can research, publish on, and learn from for years to come. There is nothing that could lure him away – until a disturbingly secretive stranger named Griffin enters Leyster's office with an ice cooler and a job offer. In the cooler is the head of a freshly killed Stegosaurus.
Griffin has been entrusted with an extraordinary gift, an impossible technology on loan to humanity from unknown beings for an undisclosed purpose. Time travel has become a reality millions of years before it rationally could be. With it, Richard Leyster and his colleagues can make their most cherished fantasy come true. They can study the dinosaurs up close, in their own time and milieu.
Now, suddenly, individual lives can turn back on themselves. People can meet, shake hands, and converse with their younger versions at various crossroads in time. One wrong word, a single misguided act, could be disastrous to the project and to the world. But Griffin must make sure everything that is supposed to happen does happen – no matter who is destined to be hurt... or die.
And then there's Dr. Gertrude Salley – passionate, fearless, and brutally ambitious – a genius rebel in the tight community of "bone men" and women. Alternately both Leyster's and Griffin's chief rival, trusted colleague, despised nemesis, and inscrutable lover at various junctures throughout time, Salley is relentlessly driven to screw with the working mechanisms of natural law, audaciously trespassing in forbidden areas, pushing paradox to the edge no matter what the consequences may be. And, when they concern the largest, most savage creatures that ever lived, the consequences may be terrifying indeed.
Few dinosaur novels came out with as much promotion as Bones of the Earth received when it was released in 2002 (the Jurassic Park novels being an obvious exception). Michael Swanwick already had won the Hugo award in 2000 for his short story, "Scherzo with Tyrannosaur," which was something of early incarnation of "Bones of the Earth." The publisher, Eos (a division of HarperCollins), heavily advertised the book though its web site, even allowing web users to e-mail a series of dinosaur-themed short stories to friends and family.
Bones of the Earth lived up to the hype. It's easily one of the best dinosaur novels ever written. The story focuses on three protagonists: paleontologist Richard Leyster; his occasional lover Gertrude Salley, a woman who doesn't like playing by the rules; and Griffin, Gertrude's occasional lover and the man in charge of enforcing the rules. A mysterious race of beings has given humanity the gift of time travel, but there are complications. It turns out changing the past isn't so hard. Griffin's job is to ensure that history stays history or the gift will be taken away. That's not so easy, especially when creationist terrorists are determined to prove themselves right at all costs, and when Gertrude has plans of her own.
To give away more would be spoiling the fun of the novel. Bones of the Earth takes a little time to get going. It's not until about halfway through the book that a story starts to materialize. But it's a wonderful story, filled with believable characters and intriguing speculation about dinosaur ecology. The prose is a little lazy – sometimes the book reads more like a movie script than a novel. Yet that's the only shortcoming I can come up with about this excellent work.
The cover art for "Scherzo with Tyrannosaur" (Asimov's Science Fiction, 1999) features the author with his wife.
A novel excerpt is available at the author's web site: http://www.michaelswanwick.com.


text:
Broadway's 'Diana, The Musical' To Close This Month
By Greg Evans
Associate Editor/Broadway Critic
@GregEvans5
More Stories By Greg
New York's Ensemble Studio Theatre Names Estefanía Fadul And Graeme Gillis As Co-Artistic Directors
Kevin O'Neal Dies: 'No Time For Sergeants' Actor, Brother Of Ryan O'Neal Was 77
Oscar-Winning 'Black Panther' Production Designer & Emmy-Winning 'Watchmen' Costume Designer Join 'The Wiz' On Road To Broadway
Jeanna de Waal in 'Diana, The Musical' Matthew Murphy
The Broadway production of Diana, The Musical will play its final performance on Sunday, Dec. 19, producers have announced.
The musical began previews at the Longacre Theatre on Nov. 2 and opened to withering reviews on Nov. 17. At time of closing, it will have played 33 performances and 16 previews.
"We are extraordinarily proud of the Diana company and of the show onstage at the Longacre," said producers Grove Entertainment (Beth Williams), Frank Marshall and The Araca Group in a joint statement. "Our heartfelt thanks go out to the cast, crew and everyone involved in creating the show. And to the audiences who have shown their love and support at every performance."
Both the Broadway production and a Netflix film version taped at the theater (which, in an experimental move, debuted on the streamer a month prior to the stage opening) received harsh reviews from critics. In recent weeks, the social media campaign for the Broadway musical took on a cheeky tone, playing on the campier elements of the musical favored by some audience members.
The new marketing tack apparently couldn't prevent the inevitable, however. Tickets purchased for cancelled performances will be refunded at the point of purchase.
The cast stars Jeanna de Waal as Diana, Roe Hartrampf as Prince Charles, Erin Davie as Camilla Parker Bowles and Judy Kaye as Queen Elizabeth.
Diana, The Musical features a book and lyrics by Joe DiPietro and music and lyrics by David Bryan. Christopher Ashley directs, with choreography by Kelly Devine and musical supervision and arrangements by Ian Eisendrath.
Diana The Musical
Jeanna de Waal
10 Michael Jackson Nephew Jaafar Jackson To Play King Of Pop In Antoine Fuqua-Directed Biopic
'The Phantom Of The Opera' Tops Broadway Box Office; 'The Piano Lesson' Closes On High Note
'Batman II', James Gunn's 'Superman: Legacy' Get Release Dates As DC Plan Revealed
AMC Entertainment Sells Stake In Saudi Arabia Theater Venture To Local Partner For $30 Million