\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{geometry of physics}

\begin{quote}%
This page is growing incrementally as a series of lecture series proceeds.


\end{quote}

\vspace{.5em} \hrule \vspace{.5em}
\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{physics}{}\paragraph*{{Physics}}\label{physics}

[[!include physicscontents]]

\hypertarget{differential_geometry}{}\paragraph*{{Differential geometry}}\label{differential_geometry}

[[!include synthetic differential geometry - contents]]

A set of lecture notes on [[differential geometry]] and theoretical fundamental [[physics]], combining an introduction to traditional notions with an exposition of their formulation and refinement by [[higher geometry]] and [[extended prequantum field theory]]. With an eye towards [[Hilbert's sixth problem]] approached via [[cohesion]].

Divided into two parts:

\begin{itemize}%
\item \textbf{Part I) \hyperlink{GEOMETRY}{Geometry}}


\item \textbf{Part II) \hyperlink{PHYSICS}{Physics}}



\end{itemize}

\vspace{.5em} \hrule \vspace{.5em}
$\,$

The [[nLab:geometry of physics|geometry of fundamental physics]] is \emph{[[nLab:higher differential geometry|higher differential]] [[nLab:supergeometry]]}.

\begin{tabular}{l|l}
$\phantom{AA}$ [[nLab:physics]] $\phantom{AA}$&$\phantom{AA}$ [[nLab:mathematics]] $\phantom{AA}$\\
\hline 
$\phantom{AA}$ [[nLab:gauge principle]] $\phantom{AA}$&$\phantom{AA}$ [[nLab:higher geometry]] $\phantom{AA}$ $\phantom{AA}$ ([[nLab:(infinity,1)-topos theory\\
$\phantom{AA}$ [[nLab:Pauli exclusion principle]] $\phantom{AA}$&$\phantom{AA}$ [[nLab:supergeometry]] $\phantom{AA}$\\
\end{tabular}

Here:

\begin{enumerate}%
\item \textbf{[[nLab:supergeometry|Supergeometry]]} is [[nLab:geometry]] whose [[nLab:spaces]] may have [[nLab:algebras of functions]] that are $\mathbb{Z}_2$-[[nLab:graded-commutative algebras]]. This is the mathematical reflection of the [[nLab:Pauli exclusion principle]], which says that a [[nLab:fermionic]] [[nLab:wave function]] $\Psi$ on a [[nLab:phase space]] of a [[nLab:physical system]] with [[nLab:fermions]] has to have vanishing square. By linearity this implies that

\begin{displaymath}
\begin{aligned}
    0 & = (\Psi_1 + \Psi_2)^2 
    \\
    & =
    \underset{ = 0}{\underbrace{ (\Psi_1)^2 }}  
    +
    \underset{ = 0}{\underbrace{ \Psi_1 \Psi_2 + \Psi_2 \Psi_1 }}
    +
    \underset{ = 0}{\underbrace{ (\Psi_2)^2 }}
  \end{aligned}
\end{displaymath}
and hence that fermionic [[nLab:wave functions]] \emph{[[nLab:graded commutative algebra|anti-commute]]}, and hence are the odd-graded elements in a \emph{[[nLab:commutative superalgebra]]} (a \emph{slightly} [[nLab:noncommutative algebra]]!)

Ever since the existence of [[nLab:fermions|fermionic]] [[nLab:particles]] was [[nLab:experiment|experimentally]] established, around the time of the [[nLab:Stern-Gerlach experiment]] in the 1920s, it is thus an [[nlab:experiment|experimental]] fact that fundamental physics is described by \emph{[[nLab:supergeometry]]}. (This is \emph{not} necessarily [[nLab:supersymmetry|super]]-, though of course there is a \href{geometry+of+physics+--+supersymmetry#SupersymmetryFromTheSuperpoint}{close relation}.)


\item \textbf{\href{https://ncatlab.org/schreiber/show/Higher+Structures}{Higher structures}} is short for \emph{higher [[nLab:homotopy theory|homotopy theoretic]]} [[nLab:structures]] and reflects the [[nLab:gauge principle]] of [[nLab:physics]]: This says that, generally, it does not make invariant sense to ask if any two things $x$, $y$ (e.g. [[nLab:field histories]]) are [[nLab:equality|equal]], instead one must ask for a \emph{[[nLab:gauge transformation]]} between them, mathematically a \emph{[[nLab:homotopy]]}:

\begin{displaymath}
x \stackrel{\gamma}{\longrightarrow} y
\end{displaymath}
This principle applies also to [[nLab:gauge transformations]] themselves, and thus leads to [[gauge-of-gauge transformations]]

and so on to ever [[higher gauge transformations]]:

mathematically reflected by [[higher homotopies]] in \emph{[[homotopy types|higher homotopy types]]}.

Ever since the existence of [[nLab:gauge fields]] was understood in the 1920s, it is thus an [[nlab:experiment|experimental]] fact that fundamental physics is described by \emph{[[nLab:higher geometry]]}.



\end{enumerate}
A striking consequence is that, both in [[nLab:higher geometry]] as well as in [[nLab:supergeometry]] and therefore in the [[nLab:geometry of physics|geometry of fundamental physics]], [[nLab:spaces]] generally are \emph{not} [[nLab:sets]] of [[nLab:points]], as in the traditional definition of [[nLab:topological spaces]] or [[nLab:differentiable manifolds]].

What, then, \emph{is} the [[nLab:geometry of physics|geometry of fundamental physics]]?

The right framework to answer questions like this has been \emph{urged} by [[nLab:Alexander Grothendieck]] already in \href{functorial+geometry#Grothendieck73}{Grothendieck 73} (see \href{functorial+geometry#Lawvere16Quote}{Lawvere 03}) and has been much expanded on by [[nLab:William Lawvere]] (e.g. [[nLab:Toposes of laws of motion|Lawvere 97]], [[nLab:Some Thoughts on the Future of Category Theory|Lawvere 91]]) and has an evident lift to [[nLab:higher geometry]] ([[nLab:Structured Spaces|Lurie 09]], \href{https://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos}{S. 13}), but has remained somewhat of a ``public secret'':

The answer is known, alternatively, as ([[nLab:higher geometry|higher]]) \emph{[[nLab:functorial geometry]]} (Grothendieck) or \emph{[[nLab:synthetic differential geometry]] in [[nLab:gros toposes]]} (Lawvere), or variants thereof.

In this lecture series we try to give a self-contained introduction to [[nLab:higher differential geometry|higher differential]] [[nLab:supergeometry]] this way, following [[schreiber:differential cohomology in a cohesive topos|Schreiber 13]]. We begin at the beginning, with introducing relevant basics of [[nLab:category theory]] and [[nLab:topos theory]] and will provide brief indication of real-world applications to [[nLab:perturbative quantum field theory]] and [[nLab:fundamental super p-branes]].

The [[nLab:higher differential geometry]] which we lay out subsumes various special cases that are discussed separately in the literature:

[[!include geometries of physics -- table]]

Notably [[diffeological spaces]] find home and company here: We explain how these are equivalently the \emph{[[nLab:concrete objects]]} among the the [[nLab:bosonic]] [[nLab:smooth set|smooth]] [[nLab:h-sets]]:

\begin{displaymath}
\itexarray{
    \big\{  
      \text{diffeological spaces}  
    \big\}
    \\
    \;\simeq\;
    \\
    \big\{
      \text{concrete bosonic smooth h-sets}  
    \big\}
  }
  \,.
\end{displaymath}
and we discuss how, even if one is initially interested only in ordinary [[nLab:smooth manifolds]] or only in [[nLab:diffeological spaces]], it is useful to work with more general [[nLab:super differential homotopy types]].

\begin{quote}%
graphics taken from \emph{\href{https://ncatlab.org/schreiber/show/Higher+Prequantum+Geometry}{Higher Prequantum Geometry}}


\end{quote}
$\,$

$\,$


\vspace{.5em} \hrule \vspace{.5em}
\begin{uremark}
\textbf{of chapters}

\begin{itemize}%
\item \hyperlink{AboutThisPage}{About this text}


\item \hyperlink{References}{References}



\end{itemize}
\textbf{Preliminaries}

\begin{enumerate}%
\item \hyperlink{CategoriesAndToposes}{Categories and Toposes}

\end{enumerate}
\textbf{Part I) \hyperlink{GEOMETRY}{Geometry}}

\begin{enumerate}%
\item \hyperlink{SmoothSpaces}{Smooth sets}


\item \hyperlink{SmoothnGroupoids}{Smooth homotopy types}


\item \hyperlink{StableHomotopyTypes}{Stable homotopy types}


\item \hyperlink{NGroups}{Groups}


\item \hyperlink{PrincipalBundles}{Principal bundles}


\item \hyperlink{Orbifolds}{Manifolds and Orbifolds}


\item \hyperlink{ReductionOfStructureGroups}{G-Structure and Cartan geometry}


\item \hyperlink{AssociatedNBundle}{Representations and Associated bundles}


\item \hyperlink{Modules}{Modules}


\item \hyperlink{FlatConnections}{Flat connections}


\item \hyperlink{deRhamCoefficients}{de Rham coefficients}


\item \hyperlink{PrincipalConnections}{Principal connections}


\item \hyperlink{Integration}{Integration}


\item \hyperlink{SupergeometricCoordinateSystems}{Super-geometry}



\end{enumerate}
\textbf{Transition to part II}

\begin{enumerate}%
\item \hyperlink{PrequantumGeometry}{Prequantum geometry}


\item \hyperlink{WZWTerms}{WZW terms}


\item \hyperlink{BPSCharges}{BPS charges}



\end{enumerate}
\textbf{Part II) \hyperlink{PHYSICS}{Physics}}

\begin{enumerate}%
\item \hyperlink{AFirstIdeaOfQuantumFieldTheory}{Perturbative quantum field theory}


\item \hyperlink{PhysicsMotivationAndSurvey}{Physics in Higher Geometry: Motivation and Survey}


\item \hyperlink{ClassicalMechanicsByPrequantizedLagrangianCorrespondences}{Hamilton-Jacobi-Lagrange mechanics via prequantized Lagrangian correspondences}


\item \hyperlink{HDWFieldTheoryViaHigherCorrespondences}{Hamilton-de Donder-Weyl field theory via Higher correspondences}


\item \hyperlink{LocalTopologicalPrequantumFieldTheory}{Local (topological) prequantum field theory}


\item \hyperlink{ActionFunctionalsForChernSimonsTypeGaugeTheories}{Prequantum Gauge theory and Gravity}


\item \hyperlink{QuantumMechanics}{Quantum mechanics}


\item \hyperlink{GeometricQuantization}{Geometric quantization}

\begin{enumerate}%
\item \hyperlink{GeometricQuantizationWithKUCoefficients}{Geometric quantization with KU-coefficients}

\end{enumerate}


\end{enumerate}
\end{uremark}
\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{AboutThisPage}{About this text}\dotfill \pageref*{AboutThisPage} \linebreak
\noindent\hyperlink{scope_and_perspective}{Scope and perspective}\dotfill \pageref*{scope_and_perspective} \linebreak
\noindent\hyperlink{Layers}{Layers of exposition}\dotfill \pageref*{Layers} \linebreak
\noindent\hyperlink{TabulatedIndex}{The full story in a few formal words}\dotfill \pageref*{TabulatedIndex} \linebreak
\noindent\hyperlink{CategoriesAndToposes}{\textbf{Categories and Toposes}}\dotfill \pageref*{CategoriesAndToposes} \linebreak
\noindent\hyperlink{SmoothSpaces}{\textbf{Smooth set}}\dotfill \pageref*{SmoothSpaces} \linebreak
\noindent\hyperlink{SmoothnGroupoids}{\textbf{Smooth homotopy types}}\dotfill \pageref*{SmoothnGroupoids} \linebreak
\noindent\hyperlink{StableHomotopyTypes}{\textbf{Stable homotopy types}}\dotfill \pageref*{StableHomotopyTypes} \linebreak
\noindent\hyperlink{NGroups}{\textbf{Groups}}\dotfill \pageref*{NGroups} \linebreak
\noindent\hyperlink{PrincipalBundles}{\textbf{Principal bundles}}\dotfill \pageref*{PrincipalBundles} \linebreak
\noindent\hyperlink{Orbifolds}{\textbf{Manifolds and Orbifolds}}\dotfill \pageref*{Orbifolds} \linebreak
\noindent\hyperlink{ReductionOfStructureGroups}{\textbf{$G$-Structure and Cartan geometry}}\dotfill \pageref*{ReductionOfStructureGroups} \linebreak
\noindent\hyperlink{AssociatedNBundle}{\textbf{Representations and Associated bundles}}\dotfill \pageref*{AssociatedNBundle} \linebreak
\noindent\hyperlink{Modules}{\textbf{Modules}}\dotfill \pageref*{Modules} \linebreak
\noindent\hyperlink{FlatConnections}{\textbf{Flat connections}}\dotfill \pageref*{FlatConnections} \linebreak
\noindent\hyperlink{deRhamCoefficients}{\textbf{de Rham Coefficients}}\dotfill \pageref*{deRhamCoefficients} \linebreak
\noindent\hyperlink{PrincipalConnections}{\textbf{Principal connections}}\dotfill \pageref*{PrincipalConnections} \linebreak
\noindent\hyperlink{Integration}{\textbf{Integration}}\dotfill \pageref*{Integration} \linebreak
\noindent\hyperlink{SupergeometricCoordinateSystems}{\textbf{Super-geometry}}\dotfill \pageref*{SupergeometricCoordinateSystems} \linebreak
\noindent\hyperlink{PrequantumGeometry}{\textbf{Prequantum geometry}}\dotfill \pageref*{PrequantumGeometry} \linebreak
\noindent\hyperlink{WZWTerms}{\textbf{WZW terms}}\dotfill \pageref*{WZWTerms} \linebreak
\noindent\hyperlink{BPSCharges}{\textbf{BPS charges}}\dotfill \pageref*{BPSCharges} \linebreak
\noindent\hyperlink{AFirstIdeaOfQuantumFieldTheory}{\textbf{Perturbative quantum field theory}}\dotfill \pageref*{AFirstIdeaOfQuantumFieldTheory} \linebreak
\noindent\hyperlink{PhysicsMotivationAndSurvey}{\textbf{Physics in Higher Geometry: Motivation and Survey}}\dotfill \pageref*{PhysicsMotivationAndSurvey} \linebreak
\noindent\hyperlink{ClassicalMechanicsByPrequantizedLagrangianCorrespondences}{\textbf{Hamilton-Jacobi-Lagrange mechanics via prequantized Lagrangian correspondences}}\dotfill \pageref*{ClassicalMechanicsByPrequantizedLagrangianCorrespondences} \linebreak
\noindent\hyperlink{HDWFieldTheoryViaHigherCorrespondences}{\textbf{Hamilton-de Donder-Weyl field theory via Higher correspondences}}\dotfill \pageref*{HDWFieldTheoryViaHigherCorrespondences} \linebreak
\noindent\hyperlink{LocalTopologicalPrequantumFieldTheory}{\textbf{Local (topological) prequantum field theory}}\dotfill \pageref*{LocalTopologicalPrequantumFieldTheory} \linebreak
\noindent\hyperlink{ActionFunctionalsForChernSimonsTypeGaugeTheories}{\textbf{Prequantum Gauge theory and Gravity}}\dotfill \pageref*{ActionFunctionalsForChernSimonsTypeGaugeTheories} \linebreak
\noindent\hyperlink{QuantumMechanics}{\textbf{Quantum mechanics}}\dotfill \pageref*{QuantumMechanics} \linebreak
\noindent\hyperlink{GeometricQuantization}{\textbf{Geometric quantization}}\dotfill \pageref*{GeometricQuantization} \linebreak
\noindent\hyperlink{model_layer}{Model Layer}\dotfill \pageref*{model_layer} \linebreak
\noindent\hyperlink{1geometric_quantization}{1-Geometric quantization}\dotfill \pageref*{1geometric_quantization} \linebreak
\noindent\hyperlink{GeometricQuantizationWithKUCoefficients}{Geometric quantization with KU-coefficients}\dotfill \pageref*{GeometricQuantizationWithKUCoefficients} \linebreak
\noindent\hyperlink{quantum_3d_chernsimons_theory_for_compact_simple_gauge_group}{Quantum 3d Chern-Simons theory for compact simple gauge group}\dotfill \pageref*{quantum_3d_chernsimons_theory_for_compact_simple_gauge_group} \linebreak
\noindent\hyperlink{higher_geometric_quantization}{Higher geometric quantization}\dotfill \pageref*{higher_geometric_quantization} \linebreak
\noindent\hyperlink{semantics_layer}{Semantics Layer}\dotfill \pageref*{semantics_layer} \linebreak
\noindent\hyperlink{syntactic_layer}{Syntactic Layer}\dotfill \pageref*{syntactic_layer} \linebreak
\noindent\hyperlink{ApplicationsToOpenQuestionsInPhysics}{\textbf{Application to open questions in physics}}\dotfill \pageref*{ApplicationsToOpenQuestionsInPhysics} \linebreak
\noindent\hyperlink{related_expositions}{\textbf{Related expositions}}\dotfill \pageref*{related_expositions} \linebreak
\noindent\hyperlink{References}{\textbf{References}}\dotfill \pageref*{References} \linebreak
\noindent\hyperlink{ReferencesGeneral}{General}\dotfill \pageref*{ReferencesGeneral} \linebreak
\noindent\hyperlink{_mathematical_quantum_field_theory}{ Mathematical quantum field theory}\dotfill \pageref*{_mathematical_quantum_field_theory} \linebreak
\noindent\hyperlink{ReferencesToposTheory}{Topos theory in differential geometry and physics}\dotfill \pageref*{ReferencesToposTheory} \linebreak
\noindent\hyperlink{ReferencesHigherCategoryTheoryInPhysics}{Higher category theory in physics}\dotfill \pageref*{ReferencesHigherCategoryTheoryInPhysics} \linebreak
\noindent\hyperlink{ReferencesLocalPrequantumFieldTheory}{Local prequantum field theory}\dotfill \pageref*{ReferencesLocalPrequantumFieldTheory} \linebreak
\noindent\hyperlink{ReferencesHigherGeometricPrequantumGeometry}{Higher geometric prequantum theory}\dotfill \pageref*{ReferencesHigherGeometricPrequantumGeometry} \linebreak
\noindent\hyperlink{ReferencesFurtherDetails}{Further details}\dotfill \pageref*{ReferencesFurtherDetails} \linebreak
\noindent\hyperlink{ReferencesPhysicalFields}{Physical fields}\dotfill \pageref*{ReferencesPhysicalFields} \linebreak
\noindent\hyperlink{DifferentialFormsAndParallelTransport}{Differential forms and parallel transport}\dotfill \pageref*{DifferentialFormsAndParallelTransport} \linebreak
\noindent\hyperlink{3d_chernsimons_theory_and_wilson_loops}{3d Chern-Simons theory and Wilson loops}\dotfill \pageref*{3d_chernsimons_theory_and_wilson_loops} \linebreak
\noindent\hyperlink{higher_chernsimons_theories}{Higher Chern-Simons theories}\dotfill \pageref*{higher_chernsimons_theories} \linebreak


\hypertarget{AboutThisPage}{}\subsection*{{About this text}}\label{AboutThisPage}

This page is going to contain an introduction to aspects of [[differential geometry]] and their application in fundamental [[physics]]: the [[gauge theory]] appearing in the [[standard model of particle physics]] and the [[Riemannian geometry]] appearing in the [[standard model of cosmology]], as well as the [[symplectic geometry]] appearing in the [[quantization]] of both.

\hypertarget{scope_and_perspective}{}\subsubsection*{{Scope and perspective}}\label{scope_and_perspective}

The intended topic scope and readership of the first layer of this page -- the \emph{\hyperlink{LayerMod}{Model Layer}} -- is much like that of the book (\hyperlink{Frankel}{Frankel}), only that here we make use of a more modern and more transparent conceptual toolbox. We also discuss in two other layers, the \emph{\hyperlink{LayerSem}{Semantic Layer}} and the \emph{\hyperlink{LayerSyn}{Syntactic Layer}} deeper mechanisms at work in the background.

Notably, where traditional expositions of [[differential geometry]] proceed by generalizing the [[geometry]] of abstract [[coordinate|coordinate systems]] $\mathbb{R}^n$ to \emph{[[smooth manifolds]]}, here we instead begin by generalizing, in \emph{\href{SmoothSpacesLayerMod}{Smooth sets -- Model Layer}}, coordinate systems right away to \emph{[[smooth sets]]}, which happens to be both more expressive as well as actually much easier. In parallel (and to be read independently or not at all) we discuss in \emph{\hyperlink{SmoothSpacesLayerSem}{Smooth sets -- Semantic Layer}} how this means that we are working in the \emph{[[sheaf topos]]} over abstract coordinate systems. Smooth manifolds are then introduced later as an intermediate notion, together with that of \emph{[[diffeological spaces]]}. (Many of the constructions in [[differential geometry]] applied in [[physics]] do not actually need the notion of a smooth manifold, and, more importantly, for many notions in modern theoretical physics smooth manifolds are not actually sufficiently general.)

In fact we introduce smooth manifolds only after we introduce \emph{[[smooth groupoids]]} (below in \emph{\hyperlink{SmoothGroupoids}{Smooth homotopy type - Model Layer - Smooth groupoids})}, which are differential geometric structures that are \emph{still} simpler than smooth manifolds, and of course even more expressive than smooth sets. Moreover, smooth groupoids are at the very heart of the geometry of physics: modern fundamental physics is all based on the ``[[gauge symmetry|gauge principle]]'' and in \emph{\hyperlink{GaugeTransformationsInElectromagnetism}{Model Layer -- Gauge transformations in electromagnetism}} we explain how, mathematically, this is essentially nothing but the theory of smooth groupoids. As further background information we discuss in \emph{\hyperlink{SmoothHomotopyTypesSemanticLayer}{Smooth homotopy types - Semantic Layer}} how this means that we are working in a [[(infinity,1)-topos|higher topos]] over abstract coordinate systems, and in \emph{\hyperlink{SmoothHomotopyTypesSyntacticLayer}{Smooth homotopy type - Syntactic Layer}} how this means that we are reasoning about physics using the \emph{[[natural deduction]]} rules of \emph{[[homotopy type theory]]}.

From this setup then naturally flow all the many structures and phenomena seen in the geometry of physics:

\hypertarget{Layers}{}\subsubsection*{{Layers of exposition}}\label{Layers}

We discuss each topic below in three stages, in three \emph{layers}.

\begin{enumerate}%
\item The first layer, called the \textbf{Model Layer}, deals with concrete explicit constructions as familiar from traditional textbooks on differential geometry and physics. This layer is supposed to be readable and useful all in itself and the reader who feels that this is all he or she wants to see can stick to this and ignore the other layers. In particular, while the \emph{Model Layer} does invoke the basic notion of a \emph{[[category]]} and of a \emph{[[functor]]} -- which are as simple as the notions of [[group]] or [[associative algebra|algebra]] --, it does not use any actual \emph{[[category theory]]}.

\end{enumerate}
\begin{enumerate}%
\item The second layer, called the \textbf{Semantic Layer}, makes explicit the ([[(infinity,1)-category theory|higher]]) [[category theory]] and ([[(infinity,1)-topos theory|higher]]) [[topos theory]] at work in the background. This puts the concrete constructions of the \emph{Model Layer} into a more general context and helps to see certain organizational patterns that underlie the seemingly different phenomena. It provides some powerful theorems which the \emph{Model Layer} is secretly benefitting from. For instance this layer gives a systematic rule for generalizing everything at the beginning Model Layers from ordinary [[differential geometry]] to what is called \emph{[[supergeometry]]}, which is the context in which [[fermion|fermionic]] [[particles]] are formalized: the [[matter]] constituents of the [[observable universe]].

\end{enumerate}
\begin{enumerate}%
\item The third layer, called the \textbf{Syntactic Layer}, makes explicit the expression of these phenomena in the [[logical framework|formal]] [[internal language]] of the [[topos]] of [[smooth sets]] -- which is \emph{[[dependent type theory|dependent]] [[type theory]]} -- and of the [[(infinity,1)-topos|higher topos]] of [[smooth infinity-groupoid|smooth higher groupoids]] -- which is \emph{[[homotopy type theory]]}. This makes more transparent various constructions in ([[(infinity,1)-topos theory|higher]]) [[topos theory]] used in \emph{Semantic Layer}, and in fact it provides a [[categorical semantics|natural construction principle]] for objects in a (higher) topos that model some intended \emph{meaning} -- which is precisely what [[mathematical physics]] is all about. This is meant for readers who enjoy seeing fundamental physics \emph{naturally} rooted in genuinely fundamental mathematics, in \emph{[[natural deduction]]} from \emph{[[practical foundations]]}, as it were. Everybody else should ignore this.

\end{enumerate}
\textbf{The three layers}

\begin{itemize}%
\item \textbf{Model Layer} -- [[concrete particular]]: [[models]]


\item \textbf{Semantic Layer} -- [[concrete general]]: [[categorical semantics]] in [[(infinity,1)-topos theory|higher]] [[topos theory]]


\item \textbf{Syntactic Layer} -- [[abstract general]]: [[syntax]] in [[homotopy type theory|homotopy]]-[[type theory]]



\end{itemize}
This [[topos theory|topos-theoretic]] perspective on fundamental [[physics]] which is discussed here is mostly original in the identifications it makes (\hyperlink{SchreiberCohesiveInfinityTopos}{Schreiber}), but it draws insights and inspiration from (and maybe realizes) a vision already expressed since the 1960s by [[William Lawvere]], one of the central figures in the development of [[topos theory]] and [[categorical logic]]. Lawvere links the very inception of topos theory to the motivation to axiomatize physics:

\begin{quote}%
My own motivation $[$ for developing [[topos theory]] $]$ came from my earlier study of [[physics]]. The foundation of the [[continuum physics]] of general materials, $[...]$ involves powerful and clear physical ideas which unfortunately have been submerged under a mathematical apparatus including not only [[Cauchy sequences]] and countably additive [[measures]], but also ad hoc choices of [[charts]] for [[manifolds]] and of [[inverse limits]] of [[Sobolev space|Sobolev]] [[Hilbert spaces]], to get at the simple [[nuclear spaces]] of intensively and extensively variable quantities. But, as Fichera lamented, all this apparatus may well be helpful in the solution of certain problems, but can the problems themselves and the needed [[axioms]] be stated in a direct and clear manner? And might this not lead to a simpler, equally rigorous account? (\hyperlink{Lawvere2000}{Lawvere, 2000})


\end{quote}
More historical pointers along these lines and further related material can also be found at \emph{[[higher category theory and physics]]}.

To give a survey of how the exposition below proceeds in the fashion of these three layers, the following section \emph{\hyperlink{TabulatedIndex}{The full story in a few formal words}} provides what may be read as commented \emph{index} to the central themes of the following text. Whereas the exposition below is organized to start each topic with the discussion of its concrete [[models]] in a \hyperlink{LayerMod}{Model layer}, then pass to a general abstract semantics in a \hyperlink{LayerSem}{Semantic Layer} and then finally to the abstract formal syntax in a \hyperlink{LayerMod}{Syntactic Layer}, these tables indicates how this passage to abstract syntax usefully reflects back onto the concrete theory:

The leftmost columns of the following tables formulate concepts in terms of ordinary language. The second columns translate that ordinary language fairly directly to the formal language of ([[homotopy type theory|homotopy]]) [[type theory]]. The third columns then interprets these formal syntactical expressions as [[universal constructions]] in a ([[(infinity,1)-topos|higher]], [[cohesive (infinity,1)-topos|cohesive]]) [[topos]] by the rules of [[categorical semantics]]. Finally, the fourth columns indicate what this universal construction amounts to when concretely realized in the [[model]] given by [[smooth sets]] and [[smooth ∞-groupoids]]. Finally the rightmost columns point to the chapters in the text below that deal with the given construction.

These tables show that fairly evident and na\"i{}ve sounding statements in ordinary language turn under this translation into what is generally regarded as fairly sophisticated constructions. In fact some of these constructions have only been found by translating along the categorical semantics dictionary this way. So the following tables also serves to show how the general abstract discussion here is a means to facilitate reasoning about seemingly complicated concepts underlying fundamental physics:

\hypertarget{TabulatedIndex}{}\subsubsection*{{The full story in a few formal words}}\label{TabulatedIndex}

We give an overview in the spirit of \emph{\hyperlink{SyntheticQuantumFieldTheory}{Synthetic Quantum Field Theory}}.

The fundamental [[physics]] of the [[observable universe|observed world]] is governed by what is called \emph{[[quantum theory]]}. (This is explicitly so for the [[standard model of particle physics]] and induced from this all fundamental physics ever tested in laboratories; but by all that is known also the remaining ingredient of [[gravity]] is fundamentally a quantum theory, see at [[quantum gravity]] for comments).

Two major axiomatizations of [[quantum theory]] are known, namely

\begin{enumerate}%
\item \emph{[[FQFT]]} where one axiomatizes the assignment of [[spaces of states]] to pieces of [[worldvolume]] (the ``[[Schrödinger picture]]'' of quantum theory)

fragments of which involve:

\begin{itemize}%
\item [[finite quantum mechanics in terms of dagger-compact categories]]


\item [[spectral triples]] and [[graph field theory]] [[quantum mechanics]]


\item [[2-spectral triples]] and [[string]] [[sigma-models]]


\item [[Reshetikhin-Turaev construction]] for 3d [[TQFT]]


\item [[FFRS-formalism|FRS-construction]] of 2d [[CFT]] from this via [[holography]]


\item [[extended topological quantum field theories]]



\end{itemize}

\item \emph{[[AQFT]]} where one axiomatizes the assignment of [[algebras of observables]] to pieces of [[worldvolume]] (the ``[[Heisenberg picture]]'' of quantum theory)

fragments of which involve:

\begin{itemize}%
\item [[Wightman axioms]], [[Haag-Kastler axioms]]


\item [[Bohr toposes]], [[schreiber:bachelor thesis Nuiten|Bohrification of local nets of observables]]


\item [[factorization algebras]], [[factorization homology]], [[topological chiral homology]],



\end{itemize}


\end{enumerate}
(For an attempt at a survey of the state of the art as of 2011 see the collection (\hyperlink{SatiSchreiber}{Sati-Schreiber})).

But all fundamental [[quantum field theories]] observed in (or conjectured to underlie) nature arise by a process called \emph{[[quantization]]} from structures in [[differential geometry]] (or are induced via a mechanism called the [[holographic principle]] from such that do).

This differential geometric data involves

\begin{itemize}%
\item [[smooth function|smooth]] [[nonlinear functional|functionals]] -- called \emph{[[action functionals]]}


\item on [[smooth infinity-groupoid|smooth ``spaces'']] -- called \emph{[[moduli stacks]]}


\item of [[differential geometry|differential geometric]] structures such as [[fiber bundles]] and [[connection on a bundle|connections]] -- called \emph{[[gauge fields|gauge]] [[force|force fields]]}


\item as well as [[sections]] of [[associated bundles]] -- called \emph{[[matter fields]]}.



\end{itemize}
Similar differential geometric structures are involved in the \emph{[[geometric quantization]]} of such an [[action functional]] to an actual [[quantum field theory]].

Hence there is a sequence:

\begin{tabular}{l|l|l|l|l}
[[differential geometry]]&$\to$&[[geometric quantization]]&$\to$&[[quantum field theory]]\\
\hline 
\end{tabular}

We discuss a formalization of central aspects of this entire sequence. Our development proceeds -- as befits a theory of physics and hence of nature -- via \emph{[[natural deduction]]} from \emph{[[practical foundation of mathematics|practical foundations]]}.

$\,$

Fundamentally, a [[metalanguage|language]] for [[physics]] is to be a language about \emph{existence}; a language in which we can express [[judgements]] of the form:

\begin{quote}%
There is a thing $x$ of type $X$.


\end{quote}
For instance:

\begin{quote}%
There is a [[gauge field]] $\nabla$ in the [[standard model of particle physics|standard model]] $[X,\mathbf{B}\left(U\left(1\right)\times SU\left(2\right)\times SU\left(3\right)\right)_{conn}]$ of gauge fields on [[spacetime]] $X$.


\end{quote}
(Here the square bracket expression for a \emph{[[moduli stack]]} of gauge fields will be incrementally explained in the following.)

To be predictive, a [[metalanguage|language]] for physics is moreover to be a language in which we can make [[natural deduction|natural deductions]] to [[deductive reasoning|deduce]] further such [[judgements]] from given ones. For instance:

\begin{quote}%
Given a gauge field $\nabla$ as above, there is an underlying \emph{[[Yang-Mills instanton|instanton]] sector}, $UnderlyingBundle(\nabla)$, in the collection $\left[X,\mathbf{B}\left(U\left(1\right)\times SU\left(2\right)\times SU\left(3\right)\right)\right]$ of instanton configurations in the standard model.


\end{quote}
Quantum [[superpositions]] of such [[Yang-Mills instantons]] are the very substrate out of which the [[vacuum]] of the [[observable universe|observed world]] is build: the \emph{[[instanton liquid in quantum chromodynamics]]}. (For more see at \emph{\hyperlink{Yang-MillsTheory}{Yang-Mills theory}} below.) We consider here a language to reason about such phenomena formally.

The [[metalanguage|formal language]] for such \emph{[[natural deduction]]} of \emph{[[judgements]]} about there being [[terms]] of some [[type]] is called \emph{[[type theory]]}.

\textbf{Expressions in ([[dependent type theory|dependent]]) [[type theory]]}:

(read columns 1+2 first, then 3+4)

\newline | There is a thing $x$ of type $X$. | $\vdash\; x \colon X$ | An [[element]] $\left(* \stackrel{x}{\to} X\right) \in Mor(\mathbf{H})$ of an [[object]] $X$ of $\mathbf{H}$. | A point $x$ in a [[smooth infinity-groupoid|smooth moduli stack]] $X$. | \emph{\hyperlink{Judgments}{Judgements about types and terms}} | | There is a type $X$ of things $x$. | $\vdash\; X \colon Type$ | An [[element]] $(* \stackrel{\vdash X}{\to} Obj) \in Mor(\mathbf{H})$ of the [[small object|small]]-[[object classifier]] $Obj$ of $\mathbf{H}$. | A point in the \emph{[[moduli stack]] of all [[small object|small]] moduli stacks}. | \emph{\hyperlink{Judgments}{Judgements about types and terms}} | | Given a thing $x$ of type $X$ there is a thing $a(x)$ of type $A(x).$ | $x \colon X\;\vdash\; a(x) \colon A(x)$ | An [[element]] of a morphism $(A \to X)$ $\left(\itexarray{ X &&\stackrel{a}{\to}&& A \\ & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow_{} \\ && X }\right)$ in the [[slice (infinity,1)-topos|slice topos]] $\mathbf{H}_{/X}$. | An $X$-family in a moduli stack [[bundle]] $A$ over $X$. | \emph{\hyperlink{SliceCategories}{Slice categories}} and \emph{\hyperlink{SliceToposes}{Slice toposes}} and \emph{\hyperlink{SlicedInfinityToposes}{Slice ∞-Toposes}} | | There is the collection of all things $a(x)$ for all $x$. | $\vdash\; \left(\sum_{x \colon X} A\left(x\right)\right) \colon Type$ | The [[dependent sum]]/[[left adjoint]] to the [[product]]: $\itexarray{ \mathbf{H}_{/X} &\stackrel{X_!}{\to} & \mathbf{H} \\ (A \to X) &\mapsto& A \in \mathbf{H}}$ | The total space of a [[bundle]]. | \emph{\hyperlink{DependentSumTypes}{Natural deduction rules for dependent sum types}} | | There is a thing $t$ in the collection of all things $a(x)$ for all $x$. | $\vdash\; t \colon \sum_{x \colon X} A(x)$ | An element $*\stackrel{t}{\to} A$ of the total space object. | A point in the [[moduli stack]] $A$ over $X$. | |\newline | There is an assignment $f$ of an $a(x)$ to each $x$. | $\vdash \; f \colon \prod_{x \colon X} A(x)$. | An [[element]] in the [[internal hom|internal]] [[object]] of [[sections]] $* \stackrel{f}{\to} [X,A]_X$ | A [[point]] in the smooth relative [[mapping space]] of smooth [[sections]]. | \emph{\hyperlink{NaturalDeductionForDependentProduct}{Natural deduction rules for dependent product types}} | \newline | There is the collection of assignments of an $a(x)$ to each $x$. | $\vdash\; \left( \prod_{x \colon X} A\left(x\right) \right) \colon Type$ | [[internal hom|internal]] space of [[sections]] $[X,A]_X \in \mathbf{H}$ | A smooth relative [[mapping space]] of smooth [[sections]]. | | | In particular, there is the collection of such assignments when $A$ does not depend on $x$, the collection of \emph{functions} from $X$ to $A$. | $\vdash \; \left(X \to A\right) \coloneqq \left(\prod_{x \colon X} A\right) \colon Type$ | The [[internal hom]] [[object]] $[X,A] \in \mathbf{H}$. | A smooth [[mapping space]]. | \emph{\hyperlink{SmoothMappingSpaces}{Smooth mapping spaces and smooth moduli spaces}} | | There is a proof $p$ that it is true that there is $x$ of type $X$. | $\vdash \;  p \colon [X]$ | An [[element]] $* \stackrel{p}{\to}\tau_{-1}(X)$ of the [[truncated object of an (infinity,1)-topos|(-1)-truncation]] of the object $X$. | A point in the [[smooth sets]] of [[equivalence classes]] of points in $X$. | \emph{\hyperlink{Subobjects}{Subobjects}} | | There is a proof $p$ that it is true that there is an $a(x)$ for some $x$. | $\vdash\; p \colon \left(\exists_{x \colon X} A\left(x\right) \right) \coloneqq \left[ \sum_{x \colon X} A\left(x\right)\right]$ | | | |

In order to describe a structured reality, our language needs to be able to speak about \emph{comparison} of things.

Fundamental physics rests on the \emph{[[gauge theory|gauge principle]]}: it is meaningless to say that two things -- such as two [[gauge fields]] $\nabla$ as above -- are \emph{[[equality|equal]]}; instead they are \emph{gauge [[equivalence|equivalent]]} if there is a \emph{[[gauge transformation]]} between them.

So our language needs to express [[judgements]] of the form:

\begin{quote}%
There is a [[gauge transformation|gauge]] [[equivalence]] between [[gauge fields]] $\nabla_1$ and $\nabla_2$.


\end{quote}
And the language needs to be able to make [[natural deduction|natural deductions]] from such judgements to arrive at:

\begin{quote}%
Given an [[equivalence]] $\lambda \colon \nabla_1 \simeq \nabla_2$ there is an equivalence $UnderlyingBundle(\lambda) \colon UnderlyingBundle(\nabla_1) \simeq UnderlyingBundle(\nabla_2)$ between the underlying [[Yang-Mills instanton|instanton sectors]].


\end{quote}
The [[metalanguage|formal language]] based of the [[dependent type theory|dependent]] [[type theory]] which we have so far that contains these statements is \emph{type theory with [[propositional equality]]}. In this language we have [[judgements]] such as the following.

\textbf{Expressions in [[dependent type theory|dependent]] [[type theory]] with [[propositional equality]]}:

\begin{tabular}{l|l|l|l|l}
ordinary language&[[syntax]]&[[semantics]]&[[model]]&chapter\\
\hline 
&[[general abstract]]&[[general concrete]]&[[concrete particular]]&\\
Given $x,x'$, there is the collection of equivalences between $x$ and $x'$ equivalent.&$x,x' \colon X \;\vdash \; \left(x \simeq x'\right) \colon Type$.&The [[mapping cocone]] [[object]] $\itexarray{ P_{x,x'} X &\to& * \\ \downarrow &\swArrow_{e}& \downarrow^{\mathrlap{x}} \\ * &\stackrel{x'}{\to} & X }$&The [[smooth infinity-groupoid&moduli stack]] of [[gauge transformations]] between $x$ and $x'$.\\
There is an equivalence $e$ between $x$ and $x'$.&$\itexarray{\vdash \; e \colon (x \simeq x') \\ or \\ \vdash \; e \colon (x \rightsquigarrow x') }$&An [[element]] of the [[mapping cocone]] object.&A [[gauge transformation]] between $x$ and $x'$.&\\
Given $x,x'$, there is the collection of proofs that it is true that $x$ and $x'$ are equivalent.&$x,x' \colon X \;\vdash \; [x \simeq x'] \colon Type$.&The [[truncated object of an (infinity,1)-topos&(-1)-truncation]] fo the [[mapping cocone]].&The [[smooth set]] of [[equivalence classes]] of [[gauge transformations]] from $x$ to $x'$.\\
\end{tabular}

But the \emph{[[gauge theory|gauge principle]]} reaches deeper: [[gauge transformations]] themselves are subject to the gauge principle.

In general it is meaningless to ask if two gauge transformations are equal, but we may ask if there is a \emph{[[higher gauge theory|higher gauge transformation]]} that transforms one gauge transformation into the other. In the physics literature such \emph{[[gauge-of-gauge transformations]]} are best known in their incarnation as \emph{[[ghost-of-ghost fields]]} in what is called the \emph{[[BRST complex]]} of the given [[gauge theory]].

Careful analysis for instance of the \emph{[[Dirac charge quantization]]} of \emph{[[magnetic charge]]} shows that already quite mundane physical phenomena exhibit such [[higher gauge transformations]]. But more famously they are known to arise in various guises in \emph{[[string theory]]}, which is a hypothetical refinement of the [[standard model of particle physics]] and [[gravity]].

In either case, our [[metalanguage|formal language]] should not allow the [[natural deduction|deduction]] that gauge [[equivalences]] are themselves either [[equality|equal]] or not, but only allow [[judgements]] of the following form:

\begin{quote}%
There is a [[higher gauge transformation|gauge-of-gauge equivalence]] $\rho \colon (\lambda_1 \simeq \lambda_2)$ between two given [[gauge equivalences]] $\lambda_1, \lambda_2 \colon (\nabla_1 \simeq \nabla_2)$ between two given [[gauge fields]] $\nabla_1, \nabla_2$.


\end{quote}
The flavor of [[type theory]] with [[propositional equality]] for which this is the case is called \emph{[[intensional type theory]]}.

Since therefore a [[type]] $X$ in intensional type theory may contain [[homotopies]] between its [[terms]] of arbitrary order, we call it a \emph{[[homotopy type]]}.

The homotopy-type nature of the type of gauge connections $[X,\mathbf{B}G_{conn}]$ is most familiar in the physics literature in its [[infinity-Lie theory|infinitesimal approximation]], which is the (off-shell) \emph{[[BRST complex]]} of the gauge theory: the $n$-fold [[ghost-of-ghost fields]] in the BRST complex correspond to the $n$-fold [[homotopies]] in $[X, \mathbf{B}G_{conn}]$.

In particular, in [[intensional type theory]] we find the [[gauge group]] of a homotopy type, as indicated in the following table.

\textbf{Expressions in [[intensional type theory]]}:

\newline Suppose then that we have such a map between collections of gauge fields

\begin{displaymath}
\phi \colon [X, \mathbf{B}G_{conn}] \to [Y, \mathbf{B}H_{conn}]
\end{displaymath}
on two possibly different [[spacetimes]] with two possibly different [[gauge groups]].

(For instance we might be looking at \emph{[[Montonen-Olive duality]]}/\_[[S-duality]]\_ or \emph{[[Seiberg duality]]} of [[super Yang-Mills theory]].)

Then we should call $\phi$ an [[equivalence]] - in the physics literature often: a \emph{[[duality in physics|duality]]} -- if, while not necessarily being a ``[[bijection]]'', it is such that the preimage $\phi^{-1}(\nabla) \in [X,\mathbf{B}G_{conn}]$ of a gauge field $\nabla \in [Y, \mathbf{B}H_{conn}]$ consists of gauge fields that are all gauge equivalent to each other, with the gauge equivalences exhibiting this equivalence themselves all being gauge equivalent to each other, etc.

If this is the case one says that all [[homotopy fibers]] -- \emph{all gauge pre-images} -- of $\phi$ are [[contractible]] -- are \emph{gauge equivalent to a single gauge field} -- and that $\phi$ is a \emph{[[weak homotopy equivalence]]}.

For consistency we should demand that the notion of equivalence is such that the space of direct equivalences $[X, \mathbf{B}G_{conn}] \simeq [Y, \mathbf{B}H_{conn}]$ is itself equivalent to the space of such weak homotopy equivalences (``[[duality in physics|dualities]]'') $[X, \mathbf{B}G_{conn}] \stackrel{\simeq}{\to} [Y, \mathbf{B}H_{conn}]$.

This requirement is called the \emph{[[univalence]] [[axiom]]}. The [[intensional type theory]]-language considered so far equipped with this axiom is called \emph{[[homotopy type theory]]}.

We indicate now some central judgements that are expressible in homotopy type theory. This involves fundamental judgements in \emph{[[group theory]]} and in \emph{[[representation theory]]}, two of the pillars of modern [[quantum theory]]/[[quantum field theory]].

\textbf{Structures expressible in [[homotopy type theory]]}:

\newline In [[gauge theory]] physics, a [[representation]] $\rho$ of the [[gauge group]] $G$ encodes the [[particle]]-content of the [[model (in theoretical physics)]]: a [[section]] of the $\rho$-[[associated bundle]] to the gauge bundle is a \emph{[[matter field]]} in the [[model (in theoretical physics)|model]].

Therefore all the ingredients so far encode the \emph{[[kinematics]]} of gauge theory, its setup before an actual \emph{[[dynamics]]} is specified.

Dynamics in physics says how things \emph{move}, hence how they trace out [[trajectories]] in a given [[spacetime]] or more generally in some [[phase space]].

Our [[metalanguage|language]] for reasoning about physics should be able to express this. For $X$ a homotopy type that models [[spacetime]] (the collection of all points of spacetime) there should be a homotopy type $\Pi(X)$ whose [[homotopies]] and higher homotopies are the \emph{smooth trajectories}, the \emph{[[path groupoid|smooth paths]]} and higher paths in $X$.

In order to analyse the notion of \emph{smoothness} here -- we will say: the way that points hold together by \emph{[[cohesion]]} -- there should also be

\begin{itemize}%
\item an expression $\flat X$ for the [[discrete space|discrete]] collection of points underlying $X$ -- \textbf{detaching} all points;


\item an expression $\sharp X$ which \textbf{dissolves} the cohesion and produces the [[codiscrete object|codiscrete]] smooth structure on $X$.



\end{itemize}
There are some natural simple [[axioms]] on these constructions. For instance every smooth path in a discrete space $\flat X$ should be constant: $\Pi (\flat X) \simeq \flat X$.

With such natural axioms understood, these three constructions constitute an [[adjoint triple]] of \emph{[[modal logic|modalities]]} $(\Pi \dashv \flat \dashv \sharp)$ in our language. In particular $\Pi$ and $\flat$ are a \emph{[[monad]]} and \emph{[[comonad]]} on the type system, \emph{[[monad (in computer science)|in the sense of computer science]]} and $\sharp$ is even an internal monad.

Equipping the above \emph{[[homotopy type theory]]} with these [[modal logic|modalities]] turns it into what we call \emph{[[cohesive homotopy type theory]]}.

\textbf{Structures expressible in [[cohesive homotopy type theory]]}:

\newline | Given a cohesive homotopy type, there is the map that dissolves the cohesion of the points. | $X \colon Type \;\vdash\;  DeCoh_X \colon X \to \sharp X$ | The [[unit of an adjunction|unit]] of the [[codiscrete object]] [[monad]]. | The function that sends smooth families in a smooth [[moduli stack]] to families of points. | | | Given $X$ there is the collection $\Pi(X)$ of points in $X$ and smooth trajectories between points in $X$. | $\left(X \colon \sharp Type\right) \;\vdash\; \Pi(X) \colon \sharp Type$ | The construction of the [[fundamental ∞-groupoid in a locally ∞-connected (∞,1)-topos]]. | The smooth [[fundamental ∞-groupoid|path ∞-groupoid]] of $X$. | \emph{\hyperlink{InfinityConnectednessOfSmoothInfinityGrpd}{The local ∞-connectedness of the (∞,1)-topos of smooth ∞-groupoids}} | | Given $X$, there is a canonical map to $\Pi(X)$. | $\left(X \colon \sharp Type\right) \;\vdash\; ConstantPathInclusion_X \colon X \to \Pi(X)$. | The [[unit of an adjunction|unit]] of the $\Pi$-[[monad]] on a [[locally ∞-connected (∞,1)-topos]]. | The inclusion of $X$ into its smooth [[fundamental ∞-groupoid|path ∞-groupoid]] as the constant paths. | | | Given $X$, there is the result of detaching the points in $X$. | $\left(A \colon \sharp Type\right) \;\vdash\; \flat A \colon \sharp Type$ | The operation of the [[discrete object]] [[comonad]] on a ([[local (infinity,1)-topos|higher]]) [[local topos]]. | The [[moduli stack]] for [[connection on an infinity-bundle|flat ∞-connections]]. | | | Given $A$, there is a map from flat $A$-connections to the underlying $A$-bundles | $\left(A \colon \sharp Type\right) \;\vdash\; UnderlyingBundle_A \colon \flat A \to A$ | The [[counit of an adjunction|counit]] of the [[discrete object]]-[[comonad]] on a ([[local (infinity,1)-topos|higher]]) [[local topos]]. | The function that sends a flat [[connection on an ∞-bundle|∞-connection]] to its underlying [[principal ∞-bundle]]. | \emph{\hyperlink{FlatConnections}{Flat connections}} |

Adding the [[modal logic|modalities]] $(\Pi \dashv \flat \dashv \sharp)$ to the above language of [[homotopy type theory]] yields a language that we call \emph{[[cohesive homotopy type theory]]} (following a term introduced by [[Bill Lawvere|Lawvere]]).

Fundamental [[judgements]] in [[cohesive homotopy type theory]] include those indicated in the following table, which capture central concepts of [[gauge theory]] and its ([[higher geometric quantization|higher]]) [[geometric quantization]].

\textbf{Structures expressible in [[cohesive homotopy type theory]]}:

[[gauge field|Gauge fields]], [[matter fields]], and smooth [[action functionals]] on their [[moduli stacks]]\ldots{}

\newline | A closed differential form $\omega$ is a flat connection $\nabla$ and a trivialization of the underlying bundle. | $\begin{aligned} & \flat_{dR} \mathbf{B} G  \coloneqq  \\ & \sum_{\nabla \colon \flat \mathbf{B}G} (UnderlyingBundle(\nabla) \simeq *) \end{aligned}$ | $\begin{matrix} \flat_{dR}\mathbf{B}G  & \stackrel{UnderlyingConnection}{ }& \flat \mathbf{B}G \\   & \mathclap{\itexarray{\arrayopts{\align{bottom}}\;  & \itexspace{10}{0}{30} \\ \itexspace{10}{30}{1} & \swArrow}} &  {}^{\mathrlap{Underlying \atop Bundle}} \\ * &\stackrel{}{ }& \mathbf{B}G \end{matrix}$ | The [[coefficients]] for [[de Rham cohomology|de Rham]] [[hypercohomology]] -- flat [[∞-Lie algebra valued differential forms]]. | \emph{\hyperlink{deRhamCoefficients}{de Rham coefficients}} | | A general connection $\nabla$ is the equivalence between the curvature $curv(\mathbf{c})$ of a bundle $\mathbf{c}$ and a closed differential form $\omega$. | $\nabla \colon \underset{{\mathbf{c} \colon \mathbf{B}^n \mathbb{G}} \atop { \omega \colon \Omega^{n+1}_{cl} }}\sum \left( curv\left(\mathbf{c}\right) = \omega\right)$ | $\begin{matrix} \mathbf{B}^n \mathbb{G}_{conn}  & \stackrel{F_{(-)}}{ }& \Omega^{n+1}_{cl} \\   & \mathclap{\itexarray{\arrayopts{\align{bottom}}\;  & \itexspace{10}{0}{30} \\ \itexspace{10}{30}{1} & \swArrow}} &   \\ \mathbf{B}^n \mathbb{G} &\stackrel{curv}{ }& \flat_{dR} \mathbf{B}^{n+1}\mathbb{G} \end{matrix}$ | The [[coefficients]] for smooth [[differential cohomology]]: abelian ([[higher gauge theory|higher]]) [[gauge fields]]. | \emph{\href{CirclePrincipalConnections}{Circle principal n-connections}} | | There is a cohesive function from $G$-gauge fields to higher $\mathbb{G}$-gauge fields. | $\vdash \; \exp(i S) \colon \mathbf{B}G_{conn} \to \mathbf{B}^n \mathbb{G}_{conn}$ | A [[differential cohomology|differential]] [[universal characteristic class]]. | An extended [[action functional]]/[[prequantum circle n-bundle|prequantum n-bundle]] for extended [[schreiber:infinity-Chern-Simons theory|higher Chern-Simons-type]] [[gauge theory]]. | |

\ldots{} and their \emph{[[schreiber:∞-geometric prequantization]]} (see there for a more comprehensive dictionary):

\newline | There is a differentially $\mathbb{G}$-equivariant equivalence $\exp(\hat O)$ from the prequantum bundle to itself. | $\vdash \; \exp(\hat O)  \colon \underset{\nabla \colon \mathbf{B}\mathbb{G}_{conn}}{\prod} \left( P\left(\nabla\right) \stackrel{\simeq}{\to} P\left(\nabla\right) \right)$ | $\itexarray{ X &&\stackrel{\exp(\hat O)}{\to}&&  X \\ & {}_{\mathllap{\nabla}}\searrow &\swArrow& \swarrow_{\nabla} \\ && \mathbf{B} \mathbb{G}_{conn}}$ | A [[quantum operator (in geometric quantization)|prequantum operator]]: an element of the [[quantomorphism group]]/[[Heisenberg group]] of the [[quantum mechanical system|quantum system]]. | \emph{\hyperlink{GeometricQuantization}{Geometric quantization}} |

Finally, in order to be able to concretely speak about not just about any gauge field, but the [[concrete particular]] gauge fields in the [[observable universe]], our language should be able to express the existence of the \emph{[[continuum]] [[real line]]}.

\begin{tabular}{l|l|l|l|l}
ordinary language&[[syntax]]&[[semantics]]&[[model]]&chapter\\
\hline 
&[[general abstract]]&[[general concrete]]&[[concrete particular]]&\\
There is the continuum line.&$\begin{aligned}\vdash\; &  \mathbb{R} \colon Type \\ &  i \colon \mathbb{Z} \to \mathbb{R} \\ &  GeometricallyContract_{\mathbb{R}} \colon (\Pi(\mathbb{R}) \simeq Point) \end{aligned}$&[[line object]]&[[real line]]&\emph{\hyperlink{TheContinuumRealWorldLine}{The continuum real worldline}}\\
\end{tabular}

This then induces the existence of the [[circle group]] $U(1) = \mathbb{R}/\mathbb{Z}$. The [[electromagnetic field]] is a [[gauge field]] for [[gauge group]] $U(1)$. Therefore in the language of cohesive homotopy type theory we can say

\begin{quote}%
Let there be [[light]].


\end{quote}
\newline | There is light. | $\vdash \; \nabla_{em} \colon [X,\mathbf{B}U(1)_{conn}]$ | A [[cocycle]] in [[ordinary differential cohomology]] in degree-2. | A configuration of the [[electromagnetic field]] on [[spacetime]] $X$. | \emph{\hyperlink{CirclePrincipalConnections}{Circle principal connection}} |

$\,$

There are of many more constructions in fundamental ([[quantum theory|quantum]]) [[physics]] that are naturally expressible in [[cohesive homotopy type theory]], but the above should already give an idea and highlight the cornerstones of the following discussion.

$\,$

We now end this introduction and overview and turn to the in-depth account of \emph{geometry of physics}.

\begin{uremark}
\textbf{I) Geometry}

We begin by laying the foundations of [[differential geometry]]. Doing this in the natural abstract way seamlessly leads over to the foundations of [[higher differential geometry]] (see also \emph{[[motivation for higher differential geometry]]}). Once this is set up, we discuss the fundamental constructions: [[groups]], [[actions]]/[[representations]], [[fiber bundles]], [[connection on a bundle|connections]], [[Chern-Weil theory]].

\begin{enumerate}%
\item \hyperlink{SmoothSpaces}{Smooth sets}


\item \hyperlink{HomotopyTypes}{Homotopy types}


\item \hyperlink{SmoothnGroupoids}{Smooth homotopy types}


\item \hyperlink{StableHomotopyTypes}{Stable homotopy types}


\item \hyperlink{NGroups}{Groups}


\item \hyperlink{PrincipalBundles}{Principal bundles}


\item \hyperlink{Orbifolds}{Manifolds and Orbifolds}


\item \hyperlink{ReductionOfStructureGroups}{G-Structure and Cartan geometry}


\item \hyperlink{AssociatedNBundle}{Representations and Associated bundles}


\item \hyperlink{FlatConnections}{Flat connections}


\item \hyperlink{deRhamCoefficients}{de Rham coefficients}


\item \hyperlink{PrincipalConnections}{Principal connections}


\item \hyperlink{Integration}{Integration}


\item \hyperlink{SupergeometricCoordinateSystems}{Super-geometry}


\item \hyperlink{PrequantumGeometry}{Prequantum geometry}


\item \hyperlink{WZWTerms}{WZW terms}


\item \hyperlink{BPSCharges}{BPS charges}



\end{enumerate}
\end{uremark}
\hypertarget{CategoriesAndToposes}{}\subsection*{{\textbf{Categories and Toposes}}}\label{CategoriesAndToposes}

This chapter is as \emph{[[geometry of physics -- Categories and Toposes]]}

\hypertarget{SmoothSpaces}{}\subsection*{{\textbf{Smooth set}}}\label{SmoothSpaces}

This chapter is at \emph{[[geometry of physics -- smooth sets]]}.

\hypertarget{SmoothnGroupoids}{}\subsection*{{\textbf{Smooth homotopy types}}}\label{SmoothnGroupoids}

This chapter is at \emph{[[geometry of physics -- smooth homotopy types]]}.

\hypertarget{StableHomotopyTypes}{}\subsection*{{\textbf{Stable homotopy types}}}\label{StableHomotopyTypes}

This chapter is at \emph{[[geometry of physics -- stable homotopy types]]}.

\hypertarget{NGroups}{}\subsection*{{\textbf{Groups}}}\label{NGroups}

This chapter is at \emph{[[geometry of physics -- groups]]}.

\hypertarget{PrincipalBundles}{}\subsection*{{\textbf{Principal bundles}}}\label{PrincipalBundles}

This chapter is at \emph{[[geometry of physics -- principal bundles]]}.

\hypertarget{Orbifolds}{}\subsection*{{\textbf{Manifolds and Orbifolds}}}\label{Orbifolds}

this chapter is at \emph{[[geometry of physics -- manifolds and orbifolds]]}

\hypertarget{ReductionOfStructureGroups}{}\subsection*{{\textbf{$G$-Structure and Cartan geometry}}}\label{ReductionOfStructureGroups}

this chapter is at \emph{[[geometry of physics -- G-structure and Cartan geometry]]}

\hypertarget{AssociatedNBundle}{}\subsection*{{\textbf{Representations and Associated bundles}}}\label{AssociatedNBundle}

this chapter is at \emph{[[geometry of physics -- representations and associated bundles]]}

\hypertarget{Modules}{}\subsection*{{\textbf{Modules}}}\label{Modules}

this chapter is at \emph{[[geometry of physics - modules]]}

\hypertarget{FlatConnections}{}\subsection*{{\textbf{Flat connections}}}\label{FlatConnections}

this chapter is at \emph{[[geometry of physics -- flat connections]]}

\hypertarget{deRhamCoefficients}{}\subsection*{{\textbf{de Rham Coefficients}}}\label{deRhamCoefficients}

see \emph{[[geometry of physics -- de Rham coefficients]]}

\hypertarget{PrincipalConnections}{}\subsection*{{\textbf{Principal connections}}}\label{PrincipalConnections}

this chapter is at \emph{[[geometry of physics -- principal connections]]}

\hypertarget{Integration}{}\subsection*{{\textbf{Integration}}}\label{Integration}

this chapter is at \emph{[[geometry of physics -- integration]]}

\hypertarget{SupergeometricCoordinateSystems}{}\subsection*{{\textbf{Super-geometry}}}\label{SupergeometricCoordinateSystems}

this chapter is at \emph{[[geometry of physics -- supergeometry and superphysics]]}

\hypertarget{PrequantumGeometry}{}\subsection*{{\textbf{Prequantum geometry}}}\label{PrequantumGeometry}

this chapter is at \emph{[[geometry of physics -- prequantum geometry]]}

\hypertarget{WZWTerms}{}\subsection*{{\textbf{WZW terms}}}\label{WZWTerms}

this chapter is at \emph{[[geometry of physics -- WZW terms]]}

\hypertarget{BPSCharges}{}\subsection*{{\textbf{BPS charges}}}\label{BPSCharges}

this chapter is at \emph{[[geometry of physics -- BPS charges]]}

\begin{uremark}
\textbf{II) Physics}

\begin{enumerate}%
\item \hyperlink{AFirstIdeaOfQuantumFieldTheory}{Perturbative quantum field theory}


\item \hyperlink{PhysicsMotivationAndSurvey}{Physics in Higher Geometry: Motivation and Survey}


\item \hyperlink{ClassicalMechanicsByPrequantizedLagrangianCorrespondences}{Classical mechanics via prequantized Lagrangian correspondences}


\item \hyperlink{LocalTopologicalPrequantumFieldTheory}{Local (topological) prequantum field theory}


\item \hyperlink{ActionFunctionalsForChernSimonsTypeGaugeTheories}{Prequantum Gauge theory and Gravity}


\item \hyperlink{GeometricQuantization}{Geometric quantization}


\item \hyperlink{QuantumMechanics}{Quantum mechanics}



\end{enumerate}
\end{uremark}
\hypertarget{AFirstIdeaOfQuantumFieldTheory}{}\subsection*{{\textbf{Perturbative quantum field theory}}}\label{AFirstIdeaOfQuantumFieldTheory}

This section is at \emph{[[geometry of physics -- perturbative quantum field theory]]}.

\hypertarget{PhysicsMotivationAndSurvey}{}\subsection*{{\textbf{Physics in Higher Geometry: Motivation and Survey}}}\label{PhysicsMotivationAndSurvey}

Before we discuss technical details starting in the \hyperlink{Fields}{next chapter} here we survey general ideas of [[theory (physics)|theories]] in fundamental [[physics]] and motivate how these are naturally formulated in terms of the [[higher geometry]] that we developed in the \hyperlink{GEOMETRY}{first part}.

This chapter is at \emph{[[geometry of physics -- physics in higher geometry]]}.

\hypertarget{ClassicalMechanicsByPrequantizedLagrangianCorrespondences}{}\subsection*{{\textbf{Hamilton-Jacobi-Lagrange mechanics via prequantized Lagrangian correspondences}}}\label{ClassicalMechanicsByPrequantizedLagrangianCorrespondences}

This chapter is at \emph{[[prequantized Lagrangian correspondence]]}.

\hypertarget{HDWFieldTheoryViaHigherCorrespondences}{}\subsection*{{\textbf{Hamilton-de Donder-Weyl field theory via Higher correspondences}}}\label{HDWFieldTheoryViaHigherCorrespondences}

This chapter is at \emph{[[Local field theory via Higher correspondences]]}.

\hypertarget{LocalTopologicalPrequantumFieldTheory}{}\subsection*{{\textbf{Local (topological) prequantum field theory}}}\label{LocalTopologicalPrequantumFieldTheory}

This chapter is at \emph{[[geometry of physics -- local prequantum field theory]]}.

\hypertarget{ActionFunctionalsForChernSimonsTypeGaugeTheories}{}\subsection*{{\textbf{Prequantum Gauge theory and Gravity}}}\label{ActionFunctionalsForChernSimonsTypeGaugeTheories}

this chapter is at \emph{[[geometry of physics -- prequantum gauge theory and gravity]]}

\hypertarget{QuantumMechanics}{}\subsection*{{\textbf{Quantum mechanics}}}\label{QuantumMechanics}

This section is at \emph{[[geometry of physics -- quantum mechanics]]}

\hypertarget{GeometricQuantization}{}\subsection*{{\textbf{Geometric quantization}}}\label{GeometricQuantization}

\hypertarget{model_layer}{}\subsubsection*{{Model Layer}}\label{model_layer}

\hypertarget{1geometric_quantization}{}\paragraph*{{1-Geometric quantization}}\label{1geometric_quantization}

\begin{itemize}%
\item [[geometric quantization]]

\end{itemize}
\hypertarget{GeometricQuantizationWithKUCoefficients}{}\paragraph*{{Geometric quantization with KU-coefficients}}\label{GeometricQuantizationWithKUCoefficients}

this is at \emph{[[geometric quantization with KU-coefficients]]}

\hypertarget{quantum_3d_chernsimons_theory_for_compact_simple_gauge_group}{}\paragraph*{{Quantum 3d Chern-Simons theory for compact simple gauge group}}\label{quantum_3d_chernsimons_theory_for_compact_simple_gauge_group}

\begin{itemize}%
\item [[Reshetikhin-Turaev construction]], [[Turaev-Viro construction]]


\item [[conformal blocks]]



\end{itemize}
\hypertarget{higher_geometric_quantization}{}\paragraph*{{Higher geometric quantization}}\label{higher_geometric_quantization}

\begin{itemize}%
\item [[higher geometric quantization]]


\item [[motivic quantization]]



\end{itemize}
\hypertarget{semantics_layer}{}\subsubsection*{{Semantics Layer}}\label{semantics_layer}

\begin{itemize}%
\item [[n-plectic smooth infinity-groupoid]]

\end{itemize}
\hypertarget{syntactic_layer}{}\subsubsection*{{Syntactic Layer}}\label{syntactic_layer}

(\ldots{})

\hypertarget{ApplicationsToOpenQuestionsInPhysics}{}\subsection*{{\textbf{Application to open questions in physics}}}\label{ApplicationsToOpenQuestionsInPhysics}

What is it that [[higher geometry]], [[higher gauge theory]], [[extended TQFT|extended]]/local [[field theory]] and generally [[higher category theory and physics|higher category theory in physics]] contribute to open research questions in theoretical physics?

Often when this question is asked the most glaring open question of contemporary theoretical physics is forgotten:

\emph{What IS [[local quantum field theory]]?}

While something going by this name is clearly in use, it is just as clear that the full answer to this question is only being discovered these days, with formalizations such as the [[cobordism theorem]] and constructions such as [[factorization algebras]] in [[BV-quantization]] -- both of which are crucially constructions in [[higher geometry]]/[[higher category theory]].

Despite the huge success of quantum field theory, it it worthwhile to remember that all the fundamental open questions in present day fundamental physics quite likely require a deeper understanding of what quantum field theory actually is, notably non-perturbatively:

\begin{itemize}%
\item Why is there [[confinement]]/[[chiral symmetry breaking]] in non-perturbative [[QCD]]/[[Yang-Mills theory]]? (The ``mass gap problem''.)


\item What is beyond-the-standard-model physics?


\item What is [[quantum gravity]]?


\item What is non-perturbative [[string theory]]?



\end{itemize}
For instance the [[standard model of cosmology]] says that the bulk of all [[energy]] and [[matter]] in the [[observable universe]] is entirely unknown to us ([[dark matter]], ``[[dark energy]]''), while at the same time the theoretical prediction what the [[cosmological constant]] [[vacuum energy]] should be is entirely off. How glaring an open question about the nature of quantum field theory this actually is is often forgotten due to the success of [[effective field theory]]-type of reasoning that allows to neatly wrap up all this unknown energy into a single term in some effective equation. Phenomenologically this may be regarded as a success, but for fundamental theoretical physics it is a glaring open question.

And while there is work going in this direction, it may be worthwhile to recall how relatively primitive the available theoretical tools often still are. For instance it seems clear that ``canonical non-covariant quantization'' can hardly be an approrpiate tool to approach anything in the direction of [[quantum gravity]]. Even so fundamental a notion as that of \emph{[[covariant phase space]]} necessary to make progress here is not widely known in the theoretical physics community. Attempts to refine quantization to a ``covariant'' and ``[[local quantum field theory|local]]'' formalism via [[multisymplectic geometry]] have mainly got stuck, since local observables just do not form a sensible structure in ordinary [[Lie theory]]. This is resolved only in [[infinity-Lie theory]] and [[higher differential geometry]], as discussed above (\hyperlink{hgp13}{hgp 13}, \hyperlink{LocalObservables13}{lo 13}).

If one assumes that [[string theory]] is part of the answer as to what underlies the [[standard model of particle physics]] [[standard model of cosmology|and cosmology]], then this situation becomes more drastic even. The fundamental [[field (physics)|fields]] of string theory are clearly objects in [[higher differential geometry]], such as the [[B-field]], the [[RR-field]], the [[supergravity C-field]] etc. For instance the natural identification of the latter as a [[homotopy fiber product]] of [[moduli stacks]] in (\hyperlink{FSS7dCS}{FSS7dCS}, \hyperlink{FSSCField}{FSSCField}) is hardly conceivable when ignoring [[higher differential geometry]]. And this is a structure meant to be at the very heart of what makes up string theory. It is unlikely that the [[landscape of string theory vacua]] and hence the relation of string theory to [[phenomenology]] can really be understood if such basic higher-geometric phenomena of string theory are ignored (see \hyperlink{http://ncatlab.org/schreiber/show/Mathematical+Foundations+of+Quantum+Field+and+Perturbative+String+Theory#ContributionDistlerFreedMoore}{Distler-Freed-Moore 09} on this point).

(\ldots{})

\hypertarget{related_expositions}{}\subsection*{{\textbf{Related expositions}}}\label{related_expositions}

\begin{itemize}%
\item [[fiber bundles in physics]]


\item [[motivation for sheaves, cohomology and higher stacks]]


\item [[string theory FAQ]]


\item [[higher category theory and physics]]


\item [[motivation for higher differential geometry]]


\item [[applications of (higher) category theory]]


\item [[motivation for cohesion]]


\item [[Hilbert's sixth problem]]


\item [[motives in physics]]


\item [[model theory and physics]]


\item [[L-infinity algebras in physics]]



\end{itemize}
\hypertarget{References}{}\subsection*{{\textbf{References}}}\label{References}

\begin{uremark}
\begin{enumerate}%
\item \hyperlink{ReferencesGeneral}{General}


\item \hyperlink{ReferencesMathematicalQFT}{Mathematical quantum field theory}


\item \hyperlink{ReferencesToposTheory}{Topos theory in differential geometry and physics}


\item \hyperlink{ReferencesHigherCategoryTheoryInPhysics}{Higher category theory in physics}


\item \hyperlink{ReferencesLocalPrequantumFieldTheory}{Local prequantum field theory}


\item \hyperlink{ReferencesHigherGeometricPrequantumGeometry}{Higher geometric prequantum theory}


\item \hyperlink{ReferencesFurtherDetails}{Further details}



\end{enumerate}
\end{uremark}
\hypertarget{ReferencesGeneral}{}\subsubsection*{{General}}\label{ReferencesGeneral}

A textbook with basic introductions to [[differential geometry]] and [[physics]] is

\begin{itemize}%
\item [[Theodore Frankel]], \emph{[[The Geometry of Physics - An Introduction]]}

\end{itemize}
A discussion of aspects of quantum field theory with emphasis on the kind of modern tools that we are using here is in

\begin{itemize}%
\item [[Frédéric Paugam]], \emph{Towards the mathematics of quantum field theory} (\href{http://people.math.jussieu.fr/~fpaugam/documents/enseignement/master-mathematical-physics.pdf}{pdf})

\end{itemize}
The present discussion corresponds to section ``1.2 Geometry of phyics'' in

\begin{itemize}%
\item [[Urs Schreiber]], \emph{[[schreiber:differential cohomology in a cohesive topos]]}

\end{itemize}
which gives a more comprehensive account.

Another set of lecture notes along the above lines with an emphasis on aspects in [[gravity]] and [[higher gauge theory]] motivated from [[string theory]] is in

\begin{itemize}%
\item [[Urs Schreiber]], \emph{[[twisted smooth cohomology in string theory]]}, Lectures notes at \emph{Quantum Fields and twisted K-theory}, ESI (2012)

\end{itemize}
An exposition and survey of matters related to [[Chern-Simons theory]] and [[higher geometric quantization]] is in

\begin{itemize}%
\item [[Domenico Fiorenza]], [[Hisham Sati]], [[Urs Schreiber]], \emph{[[schreiber:A higher stacky perspective on Chern-Simons theory]]}

\end{itemize}
The syntactic perspective above is laid out further in

\begin{itemize}%
\item [[Urs Schreiber]], \emph{[[schreiber:Synthetic Quantum Field Theory]]}

\end{itemize}
see also at \emph{[[motivic quantization]]} the section \emph{\href{motivic%20quantization#GeneralAbstractTypeTheoreticSummary}{General abstract type theoretic summary}}.

\hypertarget{_mathematical_quantum_field_theory}{}\subsubsection*{{ Mathematical quantum field theory}}\label{_mathematical_quantum_field_theory}

A textbook (really a collection of lecture notes) on [[quantum field theory]] and [[string theory]] that tries to present material in a conceptually clean way is

\begin{itemize}%
\item [[Pierre Deligne]], [[Pavel Etingof]], [[Dan Freed]], L. Jeffrey, [[David Kazhdan]], [[John Morgan]], D.R. Morrison and [[Edward Witten]], eds. \emph{[[Quantum Fields and Strings]], A course for mathematicians}, 2 vols. Amer. Math. Soc. Providence 1999. (\href{http://www.math.ias.edu/qft}{web version})

\end{itemize}
A collection trying to summarize the state of the art of the formalization of [[QFT]] by [[FQFT]] and [[AQFT]] as of 2011 is

\begin{itemize}%
\item [[Hisham Sati]], [[Urs Schreiber]], \emph{[[schreiber:Mathematical Foundations of Quantum Field and Perturbative String Theory]]}, Proceedings of Symposia in Pure Mathematics, volume 83 AMS (2011)

\end{itemize}
\hypertarget{ReferencesToposTheory}{}\subsubsection*{{Topos theory in differential geometry and physics}}\label{ReferencesToposTheory}

One of the central figures of [[topos theory]] and [[categorical logic]], [[William Lawvere]], has motivated his interest in these subject always with intended application to the formalization of [[physics]] (of [[classical mechanics|classical]] [[continuum mechanics]] in his case).

An influential text is

\begin{itemize}%
\item [[William Lawvere]], \emph{Toposes of laws of notion}, Toposes of laws of motion , transcript of a talk in Montreal, Sept. 1997 (\href{http://www.acsu.buffalo.edu/~wlawvere/ToposMotion.pdf}{pdf})

\end{itemize}
which motivates [[synthetic differential geometry]] from [[differential equations]] appearing as [[equations of motion]] in physics. The early text

\begin{itemize}%
\item [[William Lawvere]], \emph{[[Some Thoughts on the Future of Category Theory]]} in A. Carboni, M. Pedicchio, G. Rosolini, \emph{Category Theory} , [[Como|Proceedings of the International Conference held in Como]], Lecture Notes in Mathematics 1488, Springer (1991)

\end{itemize}
already sketches the formulation of [[cohesive toposes]] and motivates their axioms with heuristics from geometry and physics.

A review by Lawvere is in

\begin{itemize}%
\item [[William Lawvere]], \emph{Comments on the Development of Topos Theory}, Development of Mathematics 1950-2000, 715-734 (2000) Birkh\"a{}user Basel

\end{itemize}
Modern accounts of physics in this spirit includes notably also the book (\hyperlink{Paugam}{Paugam}) listed above.

\hypertarget{ReferencesHigherCategoryTheoryInPhysics}{}\subsubsection*{{Higher category theory in physics}}\label{ReferencesHigherCategoryTheoryInPhysics}

An early proposal that the [[action functional]] of $n$-dimensional [[quantum field theory]] should refine to a structure involving [[n-vector space|(n-k)-vector spaces]] in [[codimension]] $(n-k)$ is in

\begin{itemize}%
\item [[Daniel Freed]], \emph{[[Higher Algebraic Structures and Quantization]]}

\end{itemize}
The full formalization of this for [[extended topological field theory]] is due to

\begin{itemize}%
\item [[Jacob Lurie]], \emph{[[On the Classification of Topological Field Theories]]}

\end{itemize}
Related comments on the extended [[quantization]] of [[infinity-Dijkgraaf-Witten theory]] are in

\begin{itemize}%
\item [[Daniel Freed]], [[Michael Hopkins]], [[Jacob Lurie]], [[Constantin Teleman]] \emph{[[Topological Quantum Field Theories from Compact Lie Groups ]]}

\end{itemize}
For more pointers see at \emph{[[higher category theory and physics]]}.

\hypertarget{ReferencesLocalPrequantumFieldTheory}{}\subsubsection*{{Local prequantum field theory}}\label{ReferencesLocalPrequantumFieldTheory}

The idea of formulating local prequantum field theory by spans in a slice over a ``space of phases'' in [[higher geometry]] has been expressed in the unpublished note

\begin{itemize}%
\item [[Urs Schreiber]], \emph{[[schreiber:Nonabelian cocycles and their quantum symmetries]]} (2008)

\end{itemize}
A formulation of the idea for [[Dijkgraaf-Witten theory]]-type field theories is indicated in section 3 of

\begin{itemize}%
\item [[Daniel Freed]], [[Michael Hopkins]], [[Jacob Lurie]], [[Constantin Teleman]], \emph{[[Topological Quantum Field Theories from Compact Lie Groups]]} (2010)

\end{itemize}
based on the considerations in section 3.2 of

\begin{itemize}%
\item [[Jacob Lurie]], \emph{[[On the Classification of Topological Field Theories]]} (2009).

\end{itemize}
Based on the general formulation of the more general [[QFT with defects|field theory with defects]] described in section 4.3 there, in

\begin{itemize}%
\item [[Domenico Fiorenza]], [[Alessandro Valentino]], \emph{Boundary conditions in local TFTs} (in preparation)

\end{itemize}
the structure of such [[domain walls]]/defects/[[branes]] are analyzed in the prequantum theory, hence with coefficients in an [[(∞,n)-category of spans]].

The study of local prequantum [[schreiber:∞-Chern-Simons theory]] with its codimension-1 [[schreiber:∞-Wess-Zumino-Witten theory]] and codimension 2-[[Wilson line]]-theory in this fashion, in an ambient [[cohesive (∞,1)-topos]] is discussed in (\hyperlink{lpqft}{lpqft})

Much of the content of this entry here are, or arose as, lecture notes for

\begin{itemize}%
\item [[Urs Schreiber]], \emph{[[schreiber:Higher Chern-Simons theory Introduction]]}, at the workshop \emph{\href{http://www.pitt.edu/~jdeblois/CS.html}{Chern-Simons Theory: Geometry, Topology and Physics}} University of Pittsburgh (May 2013)

\end{itemize}
\hypertarget{ReferencesHigherGeometricPrequantumGeometry}{}\subsubsection*{{Higher geometric prequantum theory}}\label{ReferencesHigherGeometricPrequantumGeometry}

\begin{itemize}%
\item [[Domenico Fiorenza]], [[Chris Rogers]], [[Urs Schreiber]], \emph{[[schreiber:Higher geometric prequantum theory]]}

\end{itemize}
\begin{itemize}%
\item [[Domenico Fiorenza]], [[Chris Rogers]], [[Urs Schreiber]], \emph{[[schreiber:L-∞ algebras of local observables from higher prequantum bundles]]}

\end{itemize}
\begin{itemize}%
\item [[Joost Nuiten]], [[Urs Schreiber]], \emph{[[schreiber:Local prequantum field theory]]}


\item [[Joost Nuiten]], \emph{[[schreiber:master thesis Nuiten|Cohomological quantization of local boundary prequantum field theory]]}, thesis 2013



\end{itemize}
\hypertarget{ReferencesFurtherDetails}{}\subsubsection*{{Further details}}\label{ReferencesFurtherDetails}

\hypertarget{ReferencesPhysicalFields}{}\paragraph*{{Physical fields}}\label{ReferencesPhysicalFields}

For references on the tradtional formulation of [[physical fields]] by sections of \emph{[[field bundles]]} as discussed \hyperlink{IdeaOfFieldBundlesAndItsProblems}{above} see there references [[field bundle|there]].

The formulation of physical fields as [[cocycles]] in [[twisted cohomology]] in an [[(∞,1)-topos]] as in the \emph{\hyperlink{Definition}{Definition}}-section above originates around

\begin{itemize}%
\item [[Urs Schreiber]], \emph{[[schreiber:Background fields in twisted differential nonabelian cohomology]]}, talk at \emph{[[Oberwolfach Workshop, June 2009 -- Strings, Fields, Topology]]}

\end{itemize}
Further articles since then are listed at

\begin{itemize}%
\item [[Urs Schreiber]], \emph{[[schreiber:differential cohomology in a cohesive topos]]}

\end{itemize}
In particular the general notion of fields as [[twisted differential c-structures]] appears in

\begin{itemize}%
\item [[Hisham Sati]], [[Urs Schreiber]], [[Jim Stasheff]], \emph{[[schreiber:Twisted Differential String and Fivebrane Structures]]} (\href{http://arxiv.org/abs/0910.4001}{arXiv:0910.4001})

\end{itemize}
and the general theory of [[cohomology]] and [[twisted cohomology]] with [[local coefficient ∞-bundles]] as referred to in \emph{\hyperlink{RelationToTwistedCohomology}{Relation to twisted cohomology}} above as well as the theory of [[associated ∞-bundles]] as in \emph{\hyperlink{SectionsOfAssociatedBundles}{Sections of associated ∞-bundles}} is laid out in

\begin{itemize}%
\item [[Thomas Nikolaus]], [[Urs Schreiber]], [[Danny Stevenson]], \emph{[[schreiber:Principal ∞-bundles -- theory, presentations and applications]]} (\href{http://arxiv.org/abs/1207.0248}{arXiv:1207.0248})

\end{itemize}
Some examples of fields in this sense are called ``relative fields'' in

\begin{itemize}%
\item [[Daniel Freed]], [[Constantin Teleman]], \emph{Relative quantum field theory} (\href{http://arxiv.org/abs/1212.1692}{arXiv:1212.1692})

\end{itemize}
\hypertarget{DifferentialFormsAndParallelTransport}{}\paragraph*{{Differential forms and parallel transport}}\label{DifferentialFormsAndParallelTransport}

The relation between differential 1-forms and smooth incremental path measures as used above is discussed in

\begin{itemize}%
\item [[Urs Schreiber]], [[Konrad Waldorf]], \emph{Parallel transport and functors}, J. Homotopy Relat. Struct. 4, 187-244 (\href{http://arxiv.org/abs/0705.0452}{arXiv:0705.0452})

\end{itemize}
For a commented list of related literature see \href{http://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos+--+references#HistConnAsParTrans}{here}.

(\ldots{})

\hypertarget{3d_chernsimons_theory_and_wilson_loops}{}\paragraph*{{3d Chern-Simons theory and Wilson loops}}\label{3d_chernsimons_theory_and_wilson_loops}

\begin{itemize}%
\item [[Chris Beasley]], \emph{Localization for Wilson Loops in Chern-Simons Theory}, in J. Andersen, H. Boden, A. Hahn, and B. Himpel (eds.) \emph{Chern-Simons Gauge Theory: 20 Years After}, , AMS/IP Studies in Adv. Math., Vol. 50, AMS, Providence, RI, 2011. (\href{http://arxiv.org/abs/0911.2687}{arXiv:0911.2687})

\end{itemize}
\hypertarget{higher_chernsimons_theories}{}\paragraph*{{Higher Chern-Simons theories}}\label{higher_chernsimons_theories}

The discussion of the abelian [[7d Chern-Simons theory]] involved in \href{AdS-CFT#AdS7CFT6}{AdS7/CFT6 duality} is due to (\hyperlink{AdS-CFT#Witten98}{Witten 98}). A discussion of the non-abelian quantum-corrected and [[extended prequantum field theory|extended]] refinement is in

\begin{itemize}%
\item [[Domenico Fiorenza]], [[Hisham Sati]], [[Urs Schreiber]], \emph{[[schreiber:7d Chern-Simons theory and the 5-brane]]}

\end{itemize}
\begin{itemize}%
\item [[Domenico Fiorenza]], [[Hisham Sati]], [[Urs Schreiber]], \emph{[[schreiber:The moduli 3-stack of the C-field]]}

\end{itemize}
Construction of differential cup-product theories is in

\begin{itemize}%
\item [[Domenico Fiorenza]], [[Hisham Sati]], [[Urs Schreiber]], \emph{[[schreiber:Extended higher cup-product Chern-Simons theories]]}

\end{itemize}


\end{document}