\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*{general covariance}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

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

[[!include physicscontents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{Idea}{Idea}\dotfill \pageref*{Idea} \linebreak
\noindent\hyperlink{HistoryAndOriginalFormulation}{History and original formulation}\dotfill \pageref*{HistoryAndOriginalFormulation} \linebreak
\noindent\hyperlink{ModernFormulationInDifferentialGeometry}{Modern formulation in differential geometry}\dotfill \pageref*{ModernFormulationInDifferentialGeometry} \linebreak
\noindent\hyperlink{in_gravity}{In gravity}\dotfill \pageref*{in_gravity} \linebreak
\noindent\hyperlink{RelationToPrincipleOfEquivalenceInGravity}{Relation to the ``principle of equivalence'' in gravity}\dotfill \pageref*{RelationToPrincipleOfEquivalenceInGravity} \linebreak
\noindent\hyperlink{in_other_topological_field_theories}{In other topological field theories}\dotfill \pageref*{in_other_topological_field_theories} \linebreak
\noindent\hyperlink{InHomotopyTypeTheory}{Formalization in homotopy type theory}\dotfill \pageref*{InHomotopyTypeTheory} \linebreak
\noindent\hyperlink{InformalIntroduction}{Informal introduction}\dotfill \pageref*{InformalIntroduction} \linebreak
\noindent\hyperlink{introduction_in_terms_of_type_theory}{Introduction in terms of type theory}\dotfill \pageref*{introduction_in_terms_of_type_theory} \linebreak
\noindent\hyperlink{the_ambient_theory}{The ambient theory}\dotfill \pageref*{the_ambient_theory} \linebreak
\noindent\hyperlink{the_diffeomorphism_group}{The diffeomorphism group}\dotfill \pageref*{the_diffeomorphism_group} \linebreak
\noindent\hyperlink{the_context_of_general_covariance}{The context of general covariance}\dotfill \pageref*{the_context_of_general_covariance} \linebreak
\noindent\hyperlink{generally_covariant_field_configuration_spaces}{Generally covariant field configuration spaces}\dotfill \pageref*{generally_covariant_field_configuration_spaces} \linebreak
\noindent\hyperlink{GravityInHoTT}{Generally covariant field of gravity}\dotfill \pageref*{GravityInHoTT} \linebreak
\noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak
\noindent\hyperlink{ReferencesHistory}{History}\dotfill \pageref*{ReferencesHistory} \linebreak
\noindent\hyperlink{ReferencesFormalizations}{Formalizations of general covariance}\dotfill \pageref*{ReferencesFormalizations} \linebreak
\noindent\hyperlink{FormalizationInHomtopyTypeTheory}{Formalization in homotopy type theory}\dotfill \pageref*{FormalizationInHomtopyTypeTheory} \linebreak


\hypertarget{Idea}{}\subsection*{{Idea}}\label{Idea}

In [[physics]], the term \emph{general covariance} is meant to indicate the property of a [[physical system]] or [[model (in theoretical physics)]] whose [[configuration space|configurations]], [[action functional]] and [[equations of motion]] are all [[equivariance|equivariant]] under the [[action]] of the [[diffeomorphism group]] on the [[smooth manifold]] underlying the [[spacetime]] or the [[worldvolume]] of the system. Here ``covariance'' is as in ``[[covariant tensor]]'' another term for behaviour under diffeomorphisms.

The term \emph{[[general relativity]]} for [[Einstein]]-[[gravity]] originates in at least closely related ideas (see \emph{\hyperlink{HistoryAndOriginalFormulation}{History and original formulation}} below), and Einstein-gravity is the archtypical example of a generally covariant physical system:

here, the [[configuration space]] of physical fields over a [[smooth manifold]] $\Sigma$ is not quite the space of [[Riemannian metrics]] on $\Sigma$ itself, but is the [[quotient]] $[\Sigma,\mathbf{Fields}]/\mathbf{Diff}(\Sigma)$ of this space by the [[action]] of the [[diffeomorphism group]] $\mathbf{Diff}(\Sigma)$: two Riemannian metrics $g_1$ and $g_2$ on $\Sigma$ represent the same field of [[gravity]] on $\Sigma$ if there is a [[diffeomorphism]] $f : \Sigma \stackrel{\simeq}{\to} \Sigma$ such that $g_2 = f^* g_1$.

Or rather, such a diffeomorphism is a [[gauge transformation]] between the two field configurations. The configuration space is not the naive [[quotient]] of fields by diffeomorphisms as above, but is the [[homotopy quotient]], or \emph{[[action groupoid]]}, denoted $[\Sigma,\mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma)$. In the physics literature this action groupoid is most familiar in its [[infinitesimal cohesion|infinitesimal approximation]], the corresponding [[Lie algebroid]], whose formal dual is a [[BRST complex]] whose degree-1 elements are accordingly called the \emph{diffeomorphism ghosts} (see there).

As with all [[gauge transformations]], they relate physical configurations which may be nominally different, but [[equivalence|equivalent]]. Therefore \emph{general covariance} is an instance of the general \emph{[[principle of equivalence]]} in mathematics which says that sensible statements about [[objects]] must respect the [[isomorphisms]] and more general [[equivalences]] between these objects.

A physical system which is not generally covariant in this sense is hence one where the [[smooth manifold]] $\Sigma$ as above, underlying [[spacetime]]/[[worldvolume]] is not regarded as modelling an absolute physical system (such as the [[observable universe]] in gravity), but a [[subsystem]] that is equipped with ambient [[structure]] that [[spontaneous symmetry breaking|breaks]] the diffeomorphism symmetry. Notably systems like [[electromagnetism]] or [[Yang-Mills theory]] have traditionally been written in a non-generally covariant form describing gauge fields on a fixed gravitational background, as for instance the space inhabited by a particle accelerator. This ambient structure on the spacetime $\Sigma$ breaks its general diffeomorphism invariance and hence the effective resulting theory on this background is not generally covariant (a special case of the general phenomenon of [[spontaneous symmetry breaking]]).

On the other hand, such a model consisting of background (e.g. the particle accelerator) and quantum fields propagating in it is ultimately to be understood as an approximation to a more encompassing model in which also the background is dynamical, and which is again generally covariant. Specific for electromagnetism and Yang-Mills theory this refined generally covariant model is known as \emph{[[Einstein-Maxwell theory]]} or more generally \emph{[[Einstein-Yang-Mills theory]]}.

The idea of general covariance has a long and convoluted history and the literature witnesses plenty of disagreement about how to interpret and formalize it in technical detail (\hyperlink{Norton}{Norton}). Already early arguments by [[Einstein]] himself (e.g. the ``[[hole paradox]]'' (\hyperlink{EinsteinGrossmann}{Einstein-Grossmann})) show that the discussion has suffered from the beginning from lack of the basic [[category theory|category theoretic]] concept of [[isomorphism]] in the [[category]] [[Diff]] of [[smooth manifolds]]. Below in \emph{\hyperlink{InHomotopyTypeTheory}{Formalization in homotopy type theory}} we indicate a formalization of general covariance that is general, fundamental, and accurately reflects the role of the term in theoretical physics.

\hypertarget{HistoryAndOriginalFormulation}{}\subsection*{{History and original formulation}}\label{HistoryAndOriginalFormulation}

\begin{quote}%
The question of general covariance of physical theories in space and time can be traced back to the famous debate between [[Gottfried Wilhelm Leibniz]] and [[Samuel Clarke]] (the latter assisted by Sir [[Isaac Newton]]) on the [[ontology|ontological]] status of space in the years 1715--1716 (\hyperlink{Alexander}{Alexander}), the central question being if space exists as a substance or as an absolute being and absolute motion is present (Clarke) or if it is constituted only in relation to co-existent things allowing for relativism in motions only (Leibniz). This kind of problems also played an important role when the general theory of relativity was being developed in the years around 1910. While [[Albert Einstein]] first characterized generally covariant field equations as inadmissible since they did not determine the [[Riemannian metric|metric field]] uniquely as shown in the hole argument ( \emph{Lochbetrachtung} ) in the appendix of (\hyperlink{EinsteinGrossmann}{Einstein-Grossmann}), he later accepted (\hyperlink{Einstein1916}{Einstein 1916}) that all [[physical laws]] had to be expressed by [[equations]] that are valid in all [[coordinate systems]], i. e., which are covariant (generally covariant) under arbitrary [[substitution|substitutions]].

\begin{quote}%
\emph{Die allgemeinen Naturgesetze sind durch Gleichungen auszudr\"u{}cken, die f\"u{}r alle Koordinatensysteme gelten, d. h. die beliebigen Substitutionen gegen\"u{}ber kovariant (allgemein kovariant) sind.} (\hyperlink{Einstein1916}{Einstein 1916 p. 776})


\end{quote}
The hole argument was dismissed by the reasoning that it is not the [[spacetime]] [[Riemannian metric|metric]] that has to be fixed uniquely by the [[equations of motion|field equations]], but only the physical phenomena that occur in spacetime need to be given a unique expression with reference to any description of spacetime. All physical statements are given in terms of spacetime coincidences; [[measurement|measurements]] result in statements on meetings of material points of the measuring rods with other material points or in coincidences between watch hands and points on the clockface. The introduction of a reference system merely serves the easy description of the totality of all these coincidences (point-coincidence argument) (\hyperlink{Einstein1916}{Einstein 1916 p. 776f}).

from (\hyperlink{BrunettiPorrmannRuzzi}{Brunetti-Pormann-Ruzzi})


\end{quote}
\hypertarget{ModernFormulationInDifferentialGeometry}{}\subsection*{{Modern formulation in differential geometry}}\label{ModernFormulationInDifferentialGeometry}

We discuss the modern formulation of general covariance in [[differential geometry]].

\hypertarget{in_gravity}{}\subsubsection*{{In gravity}}\label{in_gravity}

Let $\Sigma \in$ [[SmoothMfd]] be a [[smooth manifold]]. Write $Riem(\Sigma)$ for the space of ([[pseudo-Riemannian metric|pseudo]]-)[[Riemannian metrics]] on $\Sigma$. For $f : \Sigma \to \Sigma$ a [[diffeomorphism]], there is a [[function]] $f^* : Riem(\Sigma) \to Riem(\Sigma)$ which sends a Riemannian metric to its pullback:

\begin{displaymath}
(f^*g)(v,w) \coloneqq g(f_* v, f_* w)
  \,,
\end{displaymath}
where $f_* : T\Sigma \to T\Sigma$ is the canonical map induced on the [[tangent bundle]] (see at \emph{[[derivative]]}).

Say that two metrics $g_1, g_2$ are [[gauge transformation|gauge equivalent]] if there is a diffeomorphism $f$ such that $g_2 = f^* g_1$. This is an [[equivalence relation]]. Write $Riem(\Sigma)/Diff(\Sigma)$ for the corresponding set of [[equivalence classes]].

The statement of \emph{general covariance} is that the distinct configurations of the gravitational field form the set $Riem(\Sigma)/Diff(\Sigma)$. In particular, if $\Sigma$ is [[compact topological space|compact]], then the [[Einstein-Hilbert action]] functional which \emph{a priori} is defined on $Riem(\Sigma)$ descends to $Riem(\Sigma)/Diff(\Sigma)$

\begin{displaymath}
S_{EH} : Riem(\Sigma)/Diff(\Sigma) \to \mathbb{R}
  \,.
\end{displaymath}
While this captures the idea of general covariance accurately, for further development of the theory of [[gravity]], however, the set $Riem(\Sigma)/Diff(\Sigma)$ needs to be refined. It is really equipped with the structure of a [[smooth space]] $\mathbf{Riem}(\Sigma)/\mathbf{Diff}(\Sigma)$ (in order to perform [[variational calculus]] and hence derive the [[equations of motion]] of the theory), and second it is to be refined to a [[smooth infinity-groupoid|smooth groupoid]] $\mathbf{Riem}(\Sigma)\sslash\mathbf{Diff}(\Sigma)$.

Finally, for setups that admit to introduce [[fermions]]/[[spinors]] into the model one needs to refine Riemannian metrics to [[vielbein]] fields/[[orthogonal structures]]. The fully refined generally covariance smooth configuration groupoid is then $[\Sigma, \mathbf{orth}]\sslash \mathbf{Diff}(\Sigma)$, discussed in more detail \hyperlink{GravityInHoTT}{below}.

\hypertarget{RelationToPrincipleOfEquivalenceInGravity}{}\subsubsection*{{Relation to the ``principle of equivalence'' in gravity}}\label{RelationToPrincipleOfEquivalenceInGravity}

The \emph{[[equivalence principle (physics)|principle of equivalence]]} in [[general relativity]] is formally the statement that around every point in a ([[pseudo-Riemannian metric|pseudo]]-)[[Riemannian manifold]] one can find a [[coordinate system]] such that the [[Levi-Civita connection]] vanishes (``[[Riemann normal coordinates]]''), which means that to \textbf{first [[infinitesimal space|infinitesimal]] order} around that point particle dynamics subject to the force of gravity is equivalent to dynamics in [[Minkowski spacetime]] with vanishing field of gravity.

By the above, this is a special case of the principle of general covariance: for every field configuration $g$ and every given point there is a gauge equivalent field configuration $f^* g$ such that the ``force of gravity'' (the Levi-Civita connection) vanishes at that point.

It is via this relation that the physical ``[[equivalence principle (physics)|principle of equivalence]]'' relates to the mathematical \emph{[[principle of equivalence]]}: this says that formulations need to respect the given notion of [[equivalence]]/[[gauge transformation]], and so

[[principle of equivalence]] in mathematics $\Rightarrow$ principle of general covariance $\Rightarrow$ principle of equivalence in physics .

\hypertarget{in_other_topological_field_theories}{}\subsubsection*{{In other topological field theories}}\label{in_other_topological_field_theories}

\hypertarget{InHomotopyTypeTheory}{}\subsection*{{Formalization in homotopy type theory}}\label{InHomotopyTypeTheory}

We discuss here that general covariance in field theory has a natural formalization in [[homotopy type theory]], hence internal to any [[(∞,1)-topos]]. For exposition, background and further details on the discussion of [[classical field theory|classical]]/[[quantum field theory]] in this fashion see (\hyperlink{SchreiberLectures}{Schreiber, ESI lectures}) and (\hyperlink{SchreiberShulman}{Schreiber-Shulman}).

The same kind of construction yields important [[moduli stacks]], for instance the [[moduli stack of Riemann surfaces]], see \href{moduli+space+of+curves#InTermsOfTheHigherToposOfSmoothStacks}{this remark} there.

\hypertarget{InformalIntroduction}{}\subsubsection*{{Informal introduction}}\label{InformalIntroduction}

Let $\Sigma$ be a [[smooth manifold]] to be thought of as [[spacetime]].

Then the central idea of \emph{general covariance} is that for

\begin{displaymath}
i_1 \;\colon\; U \hookrightarrow \Sigma
\end{displaymath}
and

\begin{displaymath}
i_2 \;\colon\; U \hookrightarrow \Sigma
\end{displaymath}
two [[subsets]]/[[submanifolds]], they should be regarded as [[equivalence|equivalent]] if there is a [[diffeomorphism]] $\phi \;\colon\; \Sigma \stackrel{}{\longrightarrow} \Sigma$ which takes one to the other, hence such that $i_2 = \phi^\ast i_1 \coloneqq\phi \circ i_1$.

That this statement can be puzzling if one thinks of the case $U = \ast$ as being just a single point is the content of the historical ``[[hole argument]] [[paradox]]''.

But with just a little bit of formalization the apparent paradox is resolved, because the above evidently just says that the ``[[moduli space]]'' for ``subsets of spacetime'' is not the manifold $\Sigma$ itself, but is rather a ``[[moduli stack]]'' namely the [[quotient stack]] $\Sigma //Diff(\Sigma)$ of $\Sigma$ by the [[action]] of the [[diffeomorphism group]].

Indeed, the technical term ``[[quotient stack]]'' is precisely defined by the condition that for $U$ of the shape of a [[disk]]/[[coordinate chart]], then two maps

\begin{displaymath}
i \;\colon\; U \hookrightarrow \Sigma \longrightarrow \Sigma//Diff(\Sigma)
\end{displaymath}
to it are equivalent if (and only if) there is a diffeomorphism relating them, as above.

So if in a generally covariant field theory spacetime is not actually the manifold $\Sigma$, but rather the quotient stack $\Sigma//Diff(\Sigma)$, then also a [[field (physics)|field]] in this generally covariant field theory should be a field on that quotient stack, not on $\Sigma$ itself.

For $\mathbf{Fields}$ a [[moduli space]]/[[moduli stack]] of [[field (physics)|fields]], in a non-generally covariant field theory a field configuration is simply a map

\begin{displaymath}
\Phi \;\colon\; \Sigma \longrightarrow \mathbf{Fields}
\end{displaymath}
and accordingly the [[configuration space|space of all field configurations]] is the [[mapping space]] $[\Sigma, \mathbf{Fields}]$.

From this it is clear that for a generally covariant field theory we are instead to declare that the space of field configurations is

\begin{displaymath}
[\Sigma//Diff(\Sigma), \;\mathbf{Fields}]
  \,.
\end{displaymath}
And it is at this point that the formalism of [[homotopy type theory]]/[[(infinity,1)-topos theory|higher topos theory]] works a little wonder for us. Namely the formalism allows us to prove, and this is what is discussed below, that

\begin{displaymath}
[\Sigma//Diff(\Sigma),\; \mathbf{Fields}]
  \simeq
  [\Sigma,\; \mathbf{Fields}]//Diff(\Sigma)
  \,.
\end{displaymath}
In words, the right hand side is the time-honored answer: two fields \emph{on} a spacetime manifold $\Sigma$ which are such that one goes over into the other when pulled back along a diffeomorphism are [[gauge equivalence|gauge equivalent]]. This is the statement of general covariance, derived here, formally, from just the condition that any two shapes \emph{in} spacetime are to be equivalent if related by a diffeomorphism.

Here to read the above equivalence as a theorem, we have to read the left hand side, as it should, be ``in the context of $Diff(\Sigma)$-actions''. Such [[context]]-dependence is precisely what \emph{[[dependent type theory|dependent]]} [[homotopy type theory]] takes care of, and this is what the following technical statement deals with.

\hypertarget{introduction_in_terms_of_type_theory}{}\subsubsection*{{Introduction in terms of type theory}}\label{introduction_in_terms_of_type_theory}

A basic idea of traditional [[dependent type theory]] is of course that [[types]] $A$ may appear \emph{in [[context]]} of other types $\Gamma$. The traditional interpretation of such a dependent type

\begin{displaymath}
x : \Gamma \vdash A(x) : Type
\end{displaymath}
is that of a $\Gamma$-parameterized family or \emph{[[bundle]]} of types, whose [[fiber]] over $x \in \Gamma$ is $A(x)$.

But in [[homotopy type theory]], types are [[homotopy types]] and, hence so are the contexts. A [[type in context]] is now in general something more refined than just a family of types. It is really a family of types equipped with \emph{[[equivariance]]} structure with respect to the [[homotopy groups]] of the context type.

Hence in homotopy theory [[types in context]] generically satisfy an [[equivariance]]-principle.

Specifically, if the context type is [[n-connected object in an (infinity,1)-topos|connected]] and [[pointed object|pointed]], then it is equivalent to the [[delooping]] $\Gamma \simeq \mathbf{B}G$ of an [[∞-group]] $G$. One finds -- this is discussed at \emph{[[∞-action]]} -- that the [[context]] defined by the type $\mathbf{B}G$ is that of $G$-[[equivariance]]: every type in the context is a type in the original context, but now equipped with a $G$-[[∞-action]]. In a precise sense, the homotopy type theory of $G$-$\infty$-actions is equivalent to plain homotopy type theory \emph{in [[context]]} $\mathbf{B}G$.

In the following we discuss this for the case that $G$ is an [[automorphism ∞-group]] of a type $\Sigma$ which is regarded as representing [[spacetime]] or a [[worldvolume]]. We show that in this context the rules of homotopy type theory automatically induce the principle of general covariance and naturally produce configurations spaces of generally covariant field theories: for $\mathbf{Fields}$ a moduli object for the given fields, so that a field configuration is a function $\phi : \Sigma \to \mathbf{Fields}$, the configuration space of \emph{covariant} fields is the [[function type]] $(\Sigma \to \mathbf{Fields})$ but formed in the ``general covariance context'' $\mathbf{B}\mathbf{Aut}(\Sigma)$. When [[categorical semantics|interpreted]] in [[smooth infinity-groupoid|smooth models]], $\mathbf{Conf}$ is the smooth groupoid of field configurations and diffeomorphism gauge transformations acting on them, the [[Lie integration|Lie integrations]] of the [[BRST complex]] whose degree-1 elements are the \emph{diffeomorphism ghosts}.

More precisely, we show the following.

\begin{defn}
\label{}\hypertarget{}{}
Consider in homotopy type theory two types $\vdash \Sigma, \mathbf{Fields} : Type$, to be called \emph{spacetime} and \emph{field moduli}. Let

\begin{displaymath}
\vdash \mathbf{B}\mathbf{Aut}(\Sigma) : Type
\end{displaymath}
be the image of the name of $\Sigma$, with essentially unique term

\begin{displaymath}
\vdash \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)
  \,.
\end{displaymath}
Perform the canonical context extension of $\Sigma$ and trivial context extension of $\mathbf{Fields}$ to get types in context

\begin{displaymath}
\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)
  \vdash 
  \Sigma : Type
\end{displaymath}
and

\begin{displaymath}
\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)
  \vdash 
  \mathbf{Fields} : Type
  \,.
\end{displaymath}
Form then the type of field moduli ``$\mathbf{Conf} \coloneqq (\Sigma \to \mathbf{Fields})$'' in this context:

\begin{displaymath}
\mathbf{Conf} \coloneqq 
  \;\;\;\;\;
  \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)
  \vdash (\Sigma \to \mathbf{Fields}) : Type
  \,.
\end{displaymath}
\end{defn}
\begin{prop}
\label{}\hypertarget{}{}
The [[categorical semantics]] of $\mathbf{Conf}$ in the model [[Smooth∞Grpd]] of the homotopy type theory and for $\Sigma \in$ [[SmoothMfd]] $\hookrightarrow Smooth \infty Grpd$ is given by the [[diffeological space|diffeological groupoid]]

\begin{displaymath}
\mathbf{Conf} = [\Sigma, \mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma)
\end{displaymath}
whose objects are field configurations on $\Sigma$ and whose morphisms are diffeomorphism gauge transformations between them. In particular the corresponding [[Lie algebroid]] is dual to the [[BRST complex]] of fields with diffeomorphism ghosts in degree 1.

\end{prop}
\hypertarget{the_ambient_theory}{}\subsubsection*{{The ambient theory}}\label{the_ambient_theory}

Write $\mathbf{H}$ for the ambient [[homotopy type theory]], or rather an [[categorical semantics|interpretation]] given by an [[(∞,1)-topos]]. For standard applications in [[physics]] we have $\mathbf{H} =$ [[Smooth∞Grpd]] or [[SmoothSuper∞Grpd]] or similar, but none of the following general discussion depends on a concrete choice for $\mathbf{H}$.

Pick once and for all an [[object]]

\begin{displaymath}
\Sigma \in \mathbf{H}
\end{displaymath}
supposed to represent the [[space]] underlying [[spacetime]] or the [[worldvolume]] of a [[model (in theoretical physics)]],

\hypertarget{the_diffeomorphism_group}{}\subsubsection*{{The diffeomorphism group}}\label{the_diffeomorphism_group}

Write

\begin{displaymath}
\mathbf{Aut}(\Sigma) \in Grp(\mathbf{H})
\end{displaymath}
for the [[automorphism ∞-group]] of $\Sigma$. As discussed there, this is the [[loop space object]] of the [[homotopy image]]-factorization of

\begin{displaymath}
* \stackrel{\vdash \Sigma}{\to} Type
  \,,
\end{displaymath}
hence the factorization by an [[effective epimorphism in an (infinity,1)-category|effective epimorphism]] followed by a [[monomorphism in an (infinity,1)-category|monomorphism]]:

\begin{displaymath}
* \stackrel{}{\to} \mathbf{B}\mathbf{Aut}(\Sigma) 
    \stackrel{}{\hookrightarrow} Type
  \,.
\end{displaymath}
In the standard [[categorical semantics|interpretation]] of the homotopy type theory in $\mathbf{H} =$ [[Smooth∞Grpd]] $\Sigma$ could be an ordinary [[smooth manifold]] or [[orbifold]], in particular, and then $\mathbf{Aut}(\Sigma) = \mathbf{\Diff}(\Sigma)$ is the [[diffeomorphism group]] of $\Sigma$, regarded as a [[diffeological space|diffeological]] [[group object]]. In view of this archetypical example we will in the following often say \emph{[[diffeomorphism]]} for short instead of \emph{auto-equivalence in $\mathbf{H}$} and similarly refer to $\mathbf{Aut}(\Sigma)$ loosely as the \emph{diffeomorphism group} of $\Sigma$. But even in the specifical model $\mathbf{H} =$ [[Smooth∞Grpd]]/[[SmoothSuper∞Grpd]], $\Sigma$ can be much more general than a [[smooth manifold]] or [[supermanifold]] or [[orbifold]].

\hypertarget{the_context_of_general_covariance}{}\subsubsection*{{The context of general covariance}}\label{the_context_of_general_covariance}

Write then $\mathbf{B} \mathbf{Aut}(\Sigma) \in \mathbf{H}$ for the [[delooping]] of the diffeomorphism group. The essentially unique [[term]] of this type is to be thought of as being $\Sigma$ itself, and so we write it as

\begin{displaymath}
\vdash \Sigma : \mathbf{B} \mathbf{Aut}(\Sigma)
  \,.
\end{displaymath}
By the discussion at \emph{[[∞-action]]}, a [[type in context]] of $\mathbf{B}\mathbf{Aut}(\Sigma)$

\begin{displaymath}
\Sigma : \mathbf{B} \mathbf{Aut}(\Sigma) \vdash V(\Sigma)
\end{displaymath}
is a type $\vdash V : Type$ in the absolute context equipped with an $\mathbf{Aut}(\Sigma)$-[[∞-action]] $\rho : V \times \mathbf{Aut}(\Sigma) \to V$ on it. The [[dependent sum]]

\begin{displaymath}
\vdash \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)} V(\Sigma) : Type 
  \,,
\end{displaymath}
which we also write

\begin{displaymath}
V \sslash \mathbf{Aut}(\Sigma)
  \coloneqq 
  \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)}
   V(\Sigma)
  \,,
\end{displaymath}
is the total space of the universal [[associated ∞-bundle|associated]] $V$-[[fiber ∞-bundle]]:

\begin{displaymath}
\itexarray{
     V &\to& \sum_{\mathbf{B}\mathbf{Aut}(\Sigma)} V(\Sigma)
     \\
      && \downarrow^{\overline{\rho}}
     \\
      && \mathbf{B}\mathbf{Aut}(\Sigma)
  }
  \,.
\end{displaymath}
Hence the [[categorical semantics|interpretation]] of the context $\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)$ is the [[slice (∞,1)-topos]] $\mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)}$ and equivalently is the [[(∞,1)-topos]] of objects in $\mathbf{H}$ equipped with $G$-[[∞-actions]] and of $G$-[[equivariance|equivariant]] [[morphisms]] between them:

\begin{displaymath}
\mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)}
  \simeq
  Act_{\mathbf{H}}(\mathbf{Aut}(\Sigma))
  \,.
\end{displaymath}
Hence a [[type in context]] $\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)$ is a ``generally covariant type'' with respect to $\Sigma$ in the sense that it transforms [[covariant functor|covariantly]] by equivalences under diffeomorphisms of $\Sigma$. In summary then

\textbf{Fact.} $\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)$ \emph{is the \textbf{[[context]] of general covariance} with respect to $\Sigma$.}

In the precise formal sense.

In particular, $\Sigma$ itself is canonically equipped with the defining action of $\mathbf{Aut}(\Sigma)$ on it, which [[syntax|syntactically]] we may write

\begin{displaymath}
\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \Sigma : Type
\end{displaymath}
and which [[categorical semantics|semantically]] is exhibited by the universal [[associated ∞-bundle|associated]] $\Sigma$-[[fiber ∞-bundle]]

\begin{displaymath}
\itexarray{
    \Sigma &\to& \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)} \Sigma
    \\
    && \downarrow^{\overline{\rho_{\Sigma}}}
    \\
    && \mathbf{B} \mathbf{Aut}(\Sigma)
  }
  \,,
\end{displaymath}
given by the [[pullback]] of the [[universe]] $\widetilde Type \to Type$ along the defining [[monomorphism in an (infinity,1)-category|inclusion]] $\mathbf{B}\mathbf{Aut} \hookrightarrow Type$.

Here the total space

\begin{displaymath}
\Sigma \sslash \mathbf{Aut}(\Sigma) 
  \coloneqq 
  \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) } \Sigma
\end{displaymath}
is the [[homotopy quotient]] or [[action groupoid]] of $\Sigma$ by $\mathbf{Aut}(\Sigma)$. This is the type characterized by the fact that a [[function]] $f : U \to \Sigma \sslash \mathbf{Aut}(\Sigma)$ is a function to $\Sigma$ which is regarded as ([[gauge equivalence|gauge]]) [[equivalence|equivalent]] to another function to $\Sigma$ if both differ by postcomposition with a diffeomorphism of $\Sigma$.

\hypertarget{generally_covariant_field_configuration_spaces}{}\subsubsection*{{Generally covariant field configuration spaces}}\label{generally_covariant_field_configuration_spaces}

Let now

\begin{displaymath}
\mathbf{Fields} \in \mathbf{H}
\end{displaymath}
be an object that represents the [[moduli ∞-stack]] of field configurations on $\Sigma$ for some [[model (in theoretical physics)]] to be described. For instance for $G \in Grp(\mathbf{H})$ an [[∞-group]] and $\mathbf{H}$ a [[cohesive homotopy type theory]], we could have $\mathbf{Fields} = \mathbf{B}G_{conn}$ the moduli for a choice of $G$-[[connection on an ∞-bundle|principal ∞-connection]], being the moduli for $G$-([[higher gauge theory|higher]])[[gauge fields]]. For general $\mathbf{Fields} = X \in \mathbf{H}$ we may always regard $X$ as the [[target space]] of a [[sigma-model]].

Then the [[internal hom]]

\begin{displaymath}
\mathbf{Fields}(\Sigma) \coloneqq [\Sigma, \mathbf{Fields}] \in \mathbf{H}
\end{displaymath}
hence the [[function type]]

\begin{displaymath}
\vdash \Sigma \to \mathbf{Fields} : Type
\end{displaymath}
is the \emph{naive} [[configuration space]] of the model. This is not generally covariant, precisely so by the above definition: it is not in the generally covariant context $\mathbf{H}_{/\mathbf{B} \mathbf{Aut}(\Sigma)}$.

But by the [[inverse image]] of the $\mathbf{B}\mathbf{Aut}(\Sigma)$-[[dependent product]] [[étale geometric morphism]]

\begin{displaymath}
\mathbf{H}_{/\mathbf{B}G}
  \stackrel{\overset{\sum_{\mathbf{B}\mathbf{Aut}(\Sigma)}}{\to}}{
  \stackrel{\overset{}{\leftarrow}}{\underset{\prod_{\mathbf{B}\mathbf{Aut}(\Sigma)}}{\to}}}
  \mathbf{H}
\end{displaymath}
which is [[context enlargement]] by $\mathbf{B}\mathbf{Aut}(\Sigma)$, the moduli type $\mathbf{Fields}$ is freely moved to the general covariant context, where it is regarded as equipped with the \href{infinity-action#TrivialAction}{trivial ∞-action}. Accordingly we will write just $\mathbf{Fields} \in \mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)}$ with that trivial action understood, which is justified by the precise syntactic expression for it:

\begin{displaymath}
\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \mathbf{Fields} : Type
\end{displaymath}
We may then form the \emph{configuration space of fields in the generally covariant context} . As before, a field $\phi$ should be a function on $\Sigma$ with values in the moduli type of field configurations, but now we interpret this statement in the generally covariant context. Syntactically this simply means that a field is now a term in $\mathbf{B}\mathbf{Aut}(\Sigma)$-context

\begin{displaymath}
\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) 
  \vdash
  \phi : \Sigma \to \mathbf{Fields}
\end{displaymath}
and that accordingly the configuration space of fields is

\begin{displaymath}
\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) 
  \vdash
  \Sigma \to \mathbf{Fields} : Type
  \,.
\end{displaymath}
The [[categorical semantics|semantics]] of this is the [[internal hom]] in the [[slice (∞,1)-topos]], the \emph{\href{infinity-action#CartesianClosedMonoidalStructure}{Internal hom of ∞-actions}}

\begin{displaymath}
\mathbf{Conf} 
    \coloneqq
  [\Sigma \sslash \mathbf{Aut}(\Sigma), \mathbf{Fields}]
  \in
  \mathbf{H}_{/\mathbf{Aut}(\Sigma)}
  \,,
\end{displaymath}
The central observation now is that discussed at \emph{\href{infinity-action#GeneralCovariance}{∞-action -- Examples -- General covariance}}:

\begin{displaymath}
\mathbf{Conf} \simeq [\Sigma,\mathbf{Fields}] \sslash \mathbf{Aut}(\Sigma)
\end{displaymath}
is the [[homotopy quotient]] of the naive fields $\in \mathbf{Fields}(\Sigma)$ by the action of the [[diffeomorphism group]], exhibiting a [[gauge equivalence]] between any two field configurations that differ after pullback along a diffeomorphism.

This is precisely as it should be for configuration space of generally covariant theories. We have found:

\textbf{Fact}. In terms of homotopy type theory, configuration spaces of a generally covariant theory over $\Sigma$ are precisely the ordinary configuration spaces of fields, but formed in the context $\mathbf{B}\mathbf{Aut}(\Sigma)$:

\begin{displaymath}
\mathbf{Conf} =_{def}
  \;\;\;\;\;\;
\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Field}) : Type
  \,.
\end{displaymath}
\hypertarget{GravityInHoTT}{}\subsubsection*{{Generally covariant field of gravity}}\label{GravityInHoTT}

We now spell out the example of ordinary [[Einstein]]-[[gravity]] in this language. Plenty of further examples work analogously.

For pure [[gravity]], we choose $\mathbf{H} =$ [[Smooth∞Grpd]] or $=$[[SynthDiff∞Grpd]].

If we denote by $D^n \in$ [[SynthDiff∞Grpd]] the first order [[infinitesimal object|infinitesimal neighbourhood]] of the origin in the [[Cartesian space]] $\mathbb{R}^n$, then

\begin{displaymath}
GL(n) = \mathbf{Aut}(D^n)
\end{displaymath}
is the [[automorphism ∞-group]] of $D^n$. Accordingly we write the unique term of the [[delooping]] $\mathbf{B}GL(n)$ as

\begin{displaymath}
\vdash D^n : \mathbf{B}GL(n)
  \,.
\end{displaymath}
The fields of Einstein gravity are [[orthogonal structures]] ([[Riemannian metrics]]) on a [[smooth manifold]] $\Sigma \in$ [[SmoothMfd]] $\hookrightarrow \mathbf{H}$ of [[dimension]] $n$. As discussed at \emph{[[orthogonal structure]]} and \emph{[[vielbein]]}, we are to regard $\Sigma$ in the [[context]] of the [[delooping]] of the [[general linear group]] $GL(n) \in Grp(\mathbf{H})$ via its [[tangent bundle]] $T \Sigma \to \Sigma$, by which we always mean here the $GL(n)$-[[principal bundle]] to which the tangent bundle is [[associated bundle|associated]].

By the discussion at \emph{[[principal ∞-bundle]]} this is modulated by a morphism

\begin{displaymath}
(\Sigma \stackrel{\vdash T \Sigma}{\to} \mathbf{B} GL(n))
  \in
  \mathbf{H}_{/\mathbf{B} GL(n)}
\end{displaymath}
to the [[delooping]] $\mathbf{B}GL(n)$ of $GL(n)$ (the [[moduli stack]] of $GL(n)$-[[principal bundles]]) in that we have a [[fiber sequence]]

\begin{displaymath}
\itexarray{
    T \Sigma &\to& \Sigma
    \\
    && \downarrow^{\mathrlap{\vdash T \Sigma}}
    \\
    && \mathbf{B}GL(n) 
  }
\end{displaymath}
in $\mathbf{H}$. (A detailed exposition of this and the following, with further pointers, is in (\hyperlink{SchreiberLectures}{Schreiber, ESI lectures}).)

Therefore the [[syntax]] of the tangent bundle as a [[dependent type]] is

\begin{displaymath}
D^n : \mathbf{B}GL(n) \vdash T \Sigma(D^n) : Type
\end{displaymath}
and since $D^n$ is essentially unique we will notationally suppress it in the [[succedent]] on the right and just write

\begin{displaymath}
D^n : \mathbf{B}GL(n) \vdash T \Sigma : Type
  \,.
\end{displaymath}
Let then

\begin{displaymath}
(\mathbf{B} O(n) \stackrel{\mathbf{orth}}{\to} \mathbf{B} GL(n)) 
  \in 
  \mathbf{H}_{/\mathbf{B}GL(n)}
\end{displaymath}
be the [[delooping]] of the inclusion $O(n) \to GL(n)$ of the [[maximal compact subgroup]] of $GL(n)$, the [[orthogonal group]] $O(n)$, regarded as an [[object]] in the [[slice-(∞,1)-topos]] over $\mathbf{B}GL(n)$. Since this sits in the [[homotopy fiber sequence]]

\begin{displaymath}
\itexarray{
    GL(n)/O(n) &\to& \mathbf{B}O(n)
    \\
    && \downarrow^{\mathrlap{orth}}  
    \\
    && \mathbf{B}GL(n)
  }
\end{displaymath}
with the [[coset]] [[smooth space]] $GL(n)/O(n)$, the [[syntax]] of this object is the [[dependent type]]

\begin{displaymath}
D^n : \mathbf{B}GL(n) \vdash GL(n)/O(n) : Type
  \,.
\end{displaymath}
In view of the [[equivalence of (∞,1)-categories]]

\begin{displaymath}
\mathbf{H}_{/\mathbf{B}GL(n)} \simeq Act_{\mathbf{H}}(GL(n))
\end{displaymath}
this expresses the canonical $GL(n)$-[[∞-action|action]] on the coset $GL(n)/O(n)$ (by mutliplication from the ``other side'').

The [[syntax]] of the [[moduli stack]] of [[vielbein]] fields / [[Riemannian metrics]] on $\Sigma$ is

\begin{displaymath}
\vdash \prod_{D^n : \mathbf{B}GL(n)} T \Sigma \to GL(n)/O(n) : Type
  \,.
\end{displaymath}
This almost verbatim expresses the familiar statement:

\begin{quote}%
A [[vielbein]] on $\Sigma$ is a $GL(n)$-equivariant map from $T \Sigma$ to the coset $GL(n)/O(n)$.


\end{quote}
The [[categorical semantics]] of such a [[vielbein]] $e$ is as a diagram

\begin{displaymath}
\itexarray{
    \Sigma && \stackrel{}{\to}&& \mathbf{B}O(n)
    \\
    & \searrow &\swArrow_{e}& \swarrow_{\mathrlap{orth}}
    \\
    && \mathbf{B}GL(n)
  }
  \,.
\end{displaymath}
This in turn almost verbatim expresses the familar equivalent statement

\begin{quote}%
A vielbein is a [[reduction of the structure group]] of the $GL(n)$-[[principal bundle]] $T \Sigma$ along $O(n) \to GL(n)$.


\end{quote}
This is still the naive space of fields, not yet generally covariant. So we next pass to the general covariant $\mathbf{B}\mathbf{Aut}(T\Sigma)$-[[context]] and form the correct generally covariant space of fields, being the [[type in context]] $\mathbf{B} \mathbf{Aut}(T \Sigma)$ given by

\begin{displaymath}
\mathbf{Conf}
  \coloneqq
  \vdash
   \prod_{D^n : \mathbf{B}GL(n)}
   \sum_{T\Sigma : \mathbf{B}\mathbf{Aut}(T\Sigma)}
   T \Sigma \to GL(n)/O(n)   : Type
  \,,
\end{displaymath}
which is the integrated [[BRST complex]] of Einstein gravity field configurations modulo diffeomorphism ghosts: the [[smooth infinity-groupoid|smooth groupoid]] whose

\begin{itemize}%
\item [[objects]] are [[vielbein]] fields $e$ on $X$;


\item [[morphisms]] are

\begin{enumerate}%
\item orthogonal frame transformations of the fibers of the tangent bundle;


\item general diffeomorphisms of the base $\Sigma$.



\end{enumerate}


\end{itemize}
We unwind this a bit more.

A slight subtlety in interpreting the above expression is that in

\begin{displaymath}
D^n : \mathbf{B}GL(n) \vdash \mathbf{B}Aut(T \Sigma) : Type
\end{displaymath}
the [[automorphism ∞-group]] of the tangent bundle it to be formed in the [[context]] of $\mathbf{B}GL(n)$. By the discussion at \emph{[[automorphism ∞-group]]} the [[delooping]] $\mathbf{B}Aut(T \Sigma)$ is the [[∞-image]] of the name

\begin{displaymath}
(* \stackrel{}{\to} Type) \in \mathbf{H}_{/\mathbf{B}GL(n)}
\end{displaymath}
of $(\Sigma \to \mathbf{B}GL(n))$ in the slice. By the discussion at \href{over-%28infinity%2C1%29-topos#ObjectClassifier}{slice-(∞,1)-topos -- Object classifier} the [[object classifier]] in the slice is the [[projection]] $(Type \times \mathbf{B}GL(n) \to \mathbf{B}GL(n))$.

So the name and its pullback are given by a diagram of the form

\begin{displaymath}
\itexarray{
    \Sigma &&\to&& \widehat{Type} \times \mathbf{B}GL(n)
    \\
    {}^{\mathllap{}}\downarrow &&\swArrow&& \downarrow
    \\
    \mathbf{B}GL(n) &&\stackrel{(\vdash \Sigma, id)}{\to}&& Type \times \mathbf{B}GL(n)
    \\ 
    & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow
    \\
    && \mathbf{B}GL(n)
  }
\end{displaymath}
in $\mathbf{H}$. Here the [[∞-image]] is directly read off to be the factorization in the third column of

\begin{displaymath}
\itexarray{
    T \Sigma
    &\to&
    \Sigma 
     &\to&  
      (T \Sigma \sslash \mathbf{Aut}(T\Sigma)) \times \mathbf{B}GL(n)
     &\to& 
    \widehat{Type} \times \mathbf{B}GL(n)
    \\
    \downarrow 
    &&
    {}^{\mathllap{}}\downarrow && \downarrow
     && \downarrow
    \\
    * &\to& 
       \mathbf{B}GL(n) 
       &\stackrel{}{\to}& 
       \mathbf{B}\mathbf{Aut}(T \Sigma) \times \mathbf{B}GL(n)
       &\to& 
       Type \times \mathbf{B}GL(n)
    \\ 
    && & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow
    \\
    && && \mathbf{B}GL(n)
  }
  \,,
\end{displaymath}
where each square and hence each rectangle is an [[(∞,1)-pullback]] in $\mathbf{H}$. This shows that the automorphism $\infty$-group of $T \Sigma$ in the context of $\mathbf{B}GL(n)$ is just the absolute automorphism $\infty$-group freely [[context extension|context extended]]. The [[categorical semantics]] of the [[dependent type]]

\begin{displaymath}
D^n \colon \mathbf{B}GL(n), T \Sigma \colon \mathbf{B}\mathbf{Aut}(T \Sigma)
  \vdash
  T \Sigma \colon Type
\end{displaymath}
is the third column from the left in the above diagram. This means that the dependent sum in

\begin{displaymath}
\mathbf{Conf}
  \coloneqq
  \vdash
   \prod_{D^n : \mathbf{B}GL(n)}
   \sum_{T\Sigma : \mathbf{B}\mathbf{Aut}(T\Sigma)}
   T \Sigma \to GL(n)/O(n)   : Type
  \,,
\end{displaymath}
forms the internal hom in $\mathbf{H}_{/\mathbf{B}GL(n)}$ between the homotopy fiber of that third column formed in $\mathbf{H}_{/\mathbf{B}GL(n)}$, which is the second column (and therefore now does rememeber the $GL(n)$-action on $T \Sigma$) with $\mathbf{orth}$, rememeberting that the result has an $\mathbf{Aut}(T\Sigma)$-action by precomposition.

\hypertarget{References}{}\subsection*{{References}}\label{References}

\hypertarget{ReferencesHistory}{}\subsubsection*{{History}}\label{ReferencesHistory}

The pre-history of the idea of general covariance is reviewed in

\begin{itemize}%
\item H. G. Alexander (ed.), \emph{The Leibniz-Clarke Correspondence: Together With Extracts from Newton's Principia and Opticks}, Manchester University Press (1998)

\end{itemize}
The original articles by Einstein on the idea of general covariance include his \emph{Entwurf} (sketch)

\begin{itemize}%
\item [[Albert Einstein]], M. Grossmann, \emph{Entwurf einer verallgemeinerten Relativit\"a{}tstheorie und einer Theorie der Gravitation} Zeitschrift f\"u{}r Math. Phys. 62, 225--259 (1914)

\end{itemize}
of the theory of [[gravity]] (where the notion of general covariance is still rejected) and then the full development of [[general relativity]]

\begin{itemize}%
\item [[Albert Einstein]], \emph{Die Grundlage der allgemeinen Relativit\"a{}tstheorie. Ann. Phys. (Leipzig) 49, 769--822 (1916)}

\end{itemize}
where it is fully embraced.

An attempt at a fairly comprehensive review of the history of the idea of general covariance and its reception up to modern days is in

\begin{itemize}%
\item J. D. Norton, \emph{General covariance and the foundations of general relativity: eight decades of dispute}, Rep. Prog. Phys \textbf{56} (1993), (\href{http://www.pitt.edu/~jdnorton/papers/decades.pdf}{original pdf}, \href{http://www.pitt.edu/~jdnorton/papers/decades_re-set.pdf}{reprint pdf})

\end{itemize}
\hypertarget{ReferencesFormalizations}{}\subsubsection*{{Formalizations of general covariance}}\label{ReferencesFormalizations}

A formalization in the context of [[AQFT]] is proposed and discussed in

\begin{itemize}%
\item [[Klaus Fredenhagen]], [[Rudolf Haag]], \emph{Generally covariant quantum field theory and scaling limits}, Comm. Math. Phys. Volume 108, Number 1 (1987), 91-115. (\href{http://projecteuclid.org/euclid.cmp/1104116359}{EUCLID})


\item [[Romeo Brunetti]], [[Klaus Fredenhagen]], [[Rainer Verch]], \emph{The generally covariant locality principle -- A new paradigm for local quantum physics}, Commun.Math.Phys.237:31-68,2003 (\href{http://arxiv.org/abs/math-ph/0112041}{math-ph/0112041})



\end{itemize}
A review is in

\begin{itemize}%
\item [[Romeo Brunetti]], Martin Porrmann, Giuseppe Ruzzi, \emph{General Covariance in Algebraic Quantum Field Theory} (\href{http://arxiv.org/abs/math-ph/0512059}{arXiv:math-ph/0512059})

\end{itemize}
For more see the references at \emph{[[AQFT on curved spacetimes]]}.

\hypertarget{FormalizationInHomtopyTypeTheory}{}\subsubsection*{{Formalization in homotopy type theory}}\label{FormalizationInHomtopyTypeTheory}

Background and context for the above formalization of [[classical field theory|classical]]/[[quantum field theory]] in [[homotopy type theory]] see

\begin{itemize}%
\item [[Urs Schreiber]], \emph{[[twisted smooth cohomology in string theory]]}, Lectures at \emph{\href{http://maths-old.anu.edu.au/esi/2012/}{ESI program on K-theory and quantum fields}} (2012)

\end{itemize}
\begin{itemize}%
\item [[Urs Schreiber]], [[Mike Shulman]], \emph{[[schreiber:Quantum gauge field theory in Cohesive homotopy type theory]]} (2012)

\end{itemize}
See also \emph{[[higher category theory and physics]]}.



\end{document}