\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*{integration of differential forms}

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

\hypertarget{integration_theory}{}\paragraph*{{Integration theory}}\label{integration_theory}

[[!include integration theory - contents]]

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

[[!include synthetic differential geometry - contents]]

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{Description}{Description}\dotfill \pageref*{Description} \linebreak
\noindent\hyperlink{integration_of_topdimension_pseudoforms_pseudoforms_to_measures}{Integration of top-dimension pseudoforms (pseudoforms to measures)}\dotfill \pageref*{integration_of_topdimension_pseudoforms_pseudoforms_to_measures} \linebreak
\noindent\hyperlink{measures_to_pseudoforms}{Measures to pseudoforms}\dotfill \pageref*{measures_to_pseudoforms} \linebreak
\noindent\hyperlink{integration_of_more_general_forms}{Integration of more general forms}\dotfill \pageref*{integration_of_more_general_forms} \linebreak
\noindent\hyperlink{integration_on_other_domains}{Integration on other domains}\dotfill \pageref*{integration_on_other_domains} \linebreak
\noindent\hyperlink{InCohesiveHomotopyTypeTheory}{In cohesive homotopy-type theory}\dotfill \pageref*{InCohesiveHomotopyTypeTheory} \linebreak
\noindent\hyperlink{general_definition}{General definition}\dotfill \pageref*{general_definition} \linebreak
\noindent\hyperlink{recovering_traditional_integration_of_differential_forms}{Recovering traditional integration of differential forms}\dotfill \pageref*{recovering_traditional_integration_of_differential_forms} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

Here we discuss the [[integration]] of a [[differential form]] (possibly twisted in some way) on a [[topological manifold]] (possibly with additional structure) over an appropriately structured [[submanifold]] (or [[formal linear combination]] thereof).

\hypertarget{Description}{}\subsection*{{Description}}\label{Description}

See at \emph{[[differential form]]} for basic definitions.

\hypertarget{integration_of_topdimension_pseudoforms_pseudoforms_to_measures}{}\subsubsection*{{Integration of top-dimension pseudoforms (pseudoforms to measures)}}\label{integration_of_topdimension_pseudoforms_pseudoforms_to_measures}

Let $X$ be an $n$-dimensional [[topological manifold]], and let $\omega$ be a [[continuous map|continuous]] $n$-pseudoform on $X$. Suppose that $X$ is [[paracompact space|paracompact]] and [[Hausdorff space|Hausdorff]], so that we may find a [[locally finite cover]] of $X$ with a subordinate [[partition of unity]] and a continuous coordinate chart on each patch. (When $X$ is [[differentiable manifold|differentiable]], or even [[smooth manifold|smooth]], then these may also be chosen to be differentiable or smooth, which may be convenient but is not necessary.) Then $\omega$ defines a [[measure space|measure]] on $X$ as follows:

\begin{itemize}%
\item On each coordinate patch $U$, fix the orientation given by the coordinates to turn $\omega$ into an untwisted $n$-form $\hat{\omega}$; then write $\hat{\omega}$ in coordinates as

\begin{displaymath}
\hat{\omega} = \omega_U \wedge \mathrm{d}x^1 \wedge \cdots \wedge \mathrm{d}x^n .
\end{displaymath}
In this situation, it is convenient also to write

\begin{displaymath}
\omega = \omega_U \mathrm{d}x^1 \cdots \mathrm{d}x^n ;
\end{displaymath}
in other words, we interpret $\mathrm{d}x^1 \cdots \mathrm{d}x^n$ as the absolute value of $\mathrm{d}x^1 \wedge \cdots \wedge \mathrm{d}x^n$.


\item The coordinates on $U$ define a [[diffeomorphism]] between $U$ and an open subset of $\mathbf{R}^n$ that we'll also call $U$; so use the latter formula to interpret

\begin{equation}
\int_U \omega = \int_U \omega_U(x^1,\ldots,x^n)\, \mathrm{d}x^1 \cdots \mathrm{d}x^n ,
\label{absvalposs}\end{equation}
where the right-hand side is now interpreted in the usual way as as integral with respect to [[Lebesgue measure]].


\item Using the partition of unity, write

\begin{displaymath}
\omega = \sum_U w_U \omega_U ,
\end{displaymath}
where $w_U$ is a weight function defined on $U$ and $\omega_U$ is the [[restriction]] of $\omega$ to $U$. Then we have

\begin{displaymath}
\int_X \omega = \sum_U \int_U w_U(x^1,\ldots,x^n) \omega_U(x^1,\ldots,x^n)\, \mathrm{d}x^1 \cdots \mathrm{d}x^n ,
\end{displaymath}
or more generally,

\begin{displaymath}
\int_E \omega = \sum_U \int_U \chi_E(x^1,\ldots,x^n) w_U(x^1,\ldots,x^n) \omega_U(x^1,\ldots,x^n)\, \mathrm{d}x^1 \cdots \mathrm{d}x^n
\end{displaymath}
for $E$ a measurable subset of $X$ and $\chi_E$ the [[characteristic function]] of $E$.



\end{itemize}
\emph{A priori}, this definition depends not only on the particular coordinate patches chosen but also on the partition of unity chosen to go with them. Furthermore, the defintion could be done just as easily (perhaps even more easily) for something other than an $n$-pseudoform. But the (perhaps surprising) fact that justifies it all is this:

\begin{theorem}
\label{IntegrationTheorem}\hypertarget{IntegrationTheorem}{}
When $\omega$ is an $n$-pseudoform, the definition of $\int_E \omega$ is independent of the coordinates and partition chosen. Furthermore, the map from $n$-pseudoforms to measures is linear.

\end{theorem}
Note that, if $\omega$ were an $n$-form instead of a pseudoform, then the definition would depend on the orientation of the coordinates chosen. We could fix that by using the absolute value ${|\omega_U|}$ in place of $\omega_U$ in \eqref{absvalposs} and the following equations, but then the map from forms to measures would not be linear.

\hypertarget{measures_to_pseudoforms}{}\subsubsection*{{Measures to pseudoforms}}\label{measures_to_pseudoforms}

It may also be enlightening to consider how to go back from a measure to an $n$-pseudoform. If $\omega$ is an [[absolutely continuous measure|absolutely continuous]] [[Radon measure]] on $X$, then it defines an $n$-pseudoform (which we may also call $\omega$) as follows:

\begin{itemize}%
\item Given a point $a$, choose one of the two local orientations at $a$.
\item Given $n$ linearly independent vectors $(v_1,\ldots,v_n)$ at $a$, develop them into a coordinate system on a neighbourhood $U$ of $a$.
\item For sufficiently large natural number $k$, the coordinate cube $C_k$ of points with coordinates in $[0,1/k]^n$ exists (lies within $U$).
\item Let $L$ be $\lim_{k \to \infty} k^n \omega(C_k)$.
\item If the coordinate system on $U$ is positively oriented at $a$, then let $\omega(v_1,\ldots,v_n)$ be $L$; if the coordinate system on $U$ is negatively oriented at $a$, then let $\omega(v_1,\ldots,v_n)$ be $-L$.
\item Extend the definition to $n$ arbitrary vectors by continuity (which necessarily maps a linearly dependent tuple of vectors to zero).

\end{itemize}
Again, this definition is independent of the coordinate system chosen (as long as it extends the given vectors); or if that's not true, then we messed up and need to add further restrictions to the absolutely continuous Radon measure $\omega$. The definition is \emph{not} independent of the orientation chosen, of course; thus we get a pseudoform rather than an untwisted form. You might try to ignore the orientation and take $\omega(v_1,\ldots,v_n)$ to be $L$ always, but that does not define an exterior form, as is most easily seen if two vectors are switched (which does not change $L$). Instead, this would define an [[absolute differential form]] (which is equivalent to a pseudoform when, as here, the degree equals the dimension).

\hypertarget{integration_of_more_general_forms}{}\subsubsection*{{Integration of more general forms}}\label{integration_of_more_general_forms}

One can integrate forms other than $n$-pseudoforms, of course, but only over certain structures within the manifold $X$. Specifically, if $R$ is a $p$-dimensional [[submanifold]] of $X$ (that is a $p$-dimensional manifold $U$ equipped with a map $R\colon U \to X$), then we would like to integrate $p$-forms or $p$-pseudoforms (defined on $X$) over $R$. Here is how we do this:

\begin{itemize}%
\item We may integrate a $p$-form $\eta$ over $R$ if $R$ is \emph{oriented}, that is if $U$ is oriented. We pull back $\eta$ from $X$ to $U$, then use the orientation on $U$ to turn $\eta$ into a $p$-pseudoform, which we can then integrate on the $p$-dimensional manifold $U$.


\item We may integrate a $p$-pseudoform $\eta$ over $R$ if $R$ is \emph{pseudooriented}, that is if it is equipped with a map that, for each point $a$ on $U$, takes a local orientation of $X$ at $R(a)$ to a local orientation of $U$ at $a$, continuously in $a$ and taking opposite orientations to opposite orientations. Then locally, we turn $\eta$ into a $p$-form on $X$ using a local orientation on $X$, pull that back to $U$, and use the corresponding local orientation on $U$ to turn that back into a $p$-pseudoform, which we can then integrate on $U$.



\end{itemize}
Thus, while integration of $n$-pseudoforms is the most basic, integration of general $p$-forms is actually a bit simpler than integration of general $p$-pseudoforms. Integration of other twisted or vector-valued forms can also be done, again given appropriate structure on $R$.

Note that, if $X$ is thought of a submanifold of itself, then it has a natural pseudoorientation that takes each local orientation to itself, and so we recover the original definition of integration of $n$-pseudoforms on $X$. Also, if $X$ is an oriented manifold, then it may be viewed as an oriented submanifold of itself, giving a definition of integration of $n$-forms on $X$.

To integrate on \emph{unoriented} submanifolds of arbitrary dimension, use [[absolute differential forms]]. To integrate \emph{nonlinear} differential forms, use [[cogerm differential forms]].

\hypertarget{integration_on_other_domains}{}\subsubsection*{{Integration on other domains}}\label{integration_on_other_domains}

One often sees the definition of integration given for \emph{parametrised} submanifolds, that is submanifolds where $U$ is an open subset of $\mathbf{R}^p$. This amounts to a combination of the concepts above, with the two uses of $U$ (as a coordinate patch in $X$ or as the source of a submanifold of $X$) identified. The theorem that the integral of an $n$-pseudoform on $X$ is independent of the coordinates chosen now becomes a theorem that the integral of a parametrised submanifold is independent of the parametrisation (up to some details about orientation), which in the end returns the result that one can integrate forms over arbitrary submanifolds (given an orientation or pseudoorientation as above).

We can also integrate on a [[formal linear combination]] of submanifolds, which is handy since these are the [[chains]] of [[de Rham homology]]. This is straightforward:

\begin{displaymath}
\int_{\sum_i \alpha_i U_i} \omega \coloneqq \sum_i \alpha_i \int_{U_i} \omega .
\end{displaymath}
\hypertarget{InCohesiveHomotopyTypeTheory}{}\subsection*{{In cohesive homotopy-type theory}}\label{InCohesiveHomotopyTypeTheory}

We discuss here a [[general abstract]] formulation of [[differential forms]], their [[integration]] and the [[Stokes theorem]] in [[cohesive (∞,1)-toposes]], hence the axiomatics of [[cohesive homotopy type theory]] (following \hyperlink{BunkeNikolausVoelkl13}{Bunke-Nikolaus-V\"o{}lkl 13, theorem 3.2}).

\hypertarget{general_definition}{}\subsubsection*{{General definition}}\label{general_definition}

Let $\mathbf{H}$ be a [[cohesive (∞,1)-topos]]. We write $(\Pi \dashv \flat \dashv \sharp)$ for the defining triple of [[adjoint modalities]] ([[shape modality]] $\dashv$ [[flat modality]] $\dashv$ [[sharp modality]]).

As usual (see at \href{cohesive+%28infinity%2C1%29-topos+--+structures#deRhamCohomology}{structures in a cohesive ∞-topos -- de Rham cohomology}) we deduce from this the secondary cohesive modalities $\Pi_{dR}$ and $\flat_{dR}$: for a pointed object with [[loop space object]] $G$ (for instance the [[delooping]] $\mathbf{B}G$) $\flat_{dR}G$ is defined by the long [[homotopy fiber sequence]]

\begin{displaymath}
G \stackrel{\theta_G}{\longrightarrow} \flat_{dR} G \stackrel{}{\longrightarrow} \flat \mathbf{B}G \longrightarrow \mathbf{B}G
\end{displaymath}
where the morphism on the right is the $\flat$-[[counit of a comonad|counit]]. Here $\theta_G$ is the \emph{[[Maurer-Cartan form]]} on $G$.

\begin{quote}%
(Beware that elsewhere we write $\flat_{dR}\mathbf{B}G$ for what here we write $\flat_{dR}G$.)


\end{quote}
Dually $\Pi_{dR}$ is defined.

Write now

\begin{displaymath}
Stab(\mathbf{H}) = T_\ast \mathbf{H} \hookrightarrow T \mathbf{H} \to \mathbf{H}
\end{displaymath}
for [[tangent cohesive (∞,1)-topos]] of $\mathbf{H}$, extending it by its [[stabilization]] $Stab(\mathbf{H})$ given by [[spectrum objects]] in $\mathbf{H}$.

We assume that there is an [[interval object]]

\begin{displaymath}
\ast \cup \ast \stackrel{(i_0, i_1)}{\longrightarrow}  \Delta^1
\end{displaymath}
``exhibiting the cohesion'' (see at \emph{[[continuum]]}) in that there is a (chosen) [[equivalence]] between the [[shape modality]] $\Pi$ and the [[localization of an (∞,1)-category|localization]] $L_{\Delta^1}$ at the the [[projection]] maps out of [[Cartesian products]] with this line $\Delta^1\times (-) \to (-)$

\begin{displaymath}
\Pi \simeq L_{\Delta^1}
  \,.
\end{displaymath}
This is the case for instance for the ``standard [[continuum]]'', the [[real line]] in $\mathbf{H} =$ [[Smooth∞Grpd]].

It follows in particular that there is a chosen [[equivalence of (∞,1)-categories]]

\begin{displaymath}
\flat(\mathbf{H})\simeq L_{\Delta^1}\mathbf{H}
\end{displaymath}
between the [[flat modality|flat]] [[modal types|modal homotopy-types]] and the $\Delta^1$-homotopy invariant homotopy-types.

Given a [[stable homotopy type]] $\hat E \in Stab(\mathbf{H})\hookrightarrow T \mathbf{H}$ [[cohesion]] provides two objects

\begin{displaymath}
\Pi_{dR} \hat E \,,\;\;  \flat_{dR}\hat E
  \;\;
  \in Stab(\mathbf{H})
\end{displaymath}
which may be interpreted as [[de Rham complexes]] with [[coefficients]] in $\Pi(\flat_{dR} \Sigma \hat E)$, the first one restricted to negative degree, the second to non-negative degree. Moreover, there is a canonical map

\begin{displaymath}
\itexarray{
    \Pi_{dR}\hat E && \stackrel{\mathbf{d}}{\longrightarrow} && \flat_{dR}\hat E
    \\
    & {}_{\mathllap{\iota}}\searrow && \nearrow_{\mathrlap{\theta_{\hat E}}}
    \\
    && 
    \hat E
  }
\end{displaymath}
which interprets as the [[de Rham differential]] $\mathbf{d}$. See at \emph{[[differential cohomology diagram]]} for details.

Throughout in the following we leave the ``inclusion'' $\iota$ of ``differential forms regarded as $\hat E$-connections on trivial $E$-bundles'' implicit.

\begin{defn}
\label{CohesiveIntegrationOfDifferentialForms}\hypertarget{CohesiveIntegrationOfDifferentialForms}{}
\emph{Integration of differential} forms is the morphism

\begin{displaymath}
\int_{\Delta^1} \;\colon\;  [\Delta^1, \flat_{dR}\hat E] \longrightarrow \Pi_{dR}\hat E
\end{displaymath}
which is induced via the [[homotopy cofiber]] property of $\flat_{dR}\Omega \hat E$ from the [[counit of a comonad|counit]] naturality square of the [[flat modality]] on $[(\ast \coprod \ast \stackrel{(i_0, i_1)}{\to} \Delta ^1 ), -]$, using that this square exhibits a [[null homotopy]] due to the $\Delta^1$-homotopy invariance of $\flat \hat E$.

\end{defn}
(\hyperlink{BunkeNikolausVoelkl13}{Bunke-Nikolaus-V\"o{}lkl 13, (9), (10)}

\begin{prop}
\label{}\hypertarget{}{}
The [[Stokes theorem]] holds:

\begin{displaymath}
\int_0^1 \circ \mathbf{d} \simeq i_1^\ast - i_0^\ast
  \,.
\end{displaymath}
\end{prop}
(\hyperlink{BunkeNikolausVoelkl13}{Bunke-Nikolaus-V\"o{}lkl 13, theorem 3.2}

\hypertarget{recovering_traditional_integration_of_differential_forms}{}\subsubsection*{{Recovering traditional integration of differential forms}}\label{recovering_traditional_integration_of_differential_forms}

\begin{prop}
\label{}\hypertarget{}{}
In $\mathbf{H} =$ [[Smooth∞Grpd]] let $\hat E \in Stab(\mathbf{H})$ be given, under the [[stable Dold-Kan correspondence]], by the traditional truncated [[de Rham complex]] $\hat E \coloneqq \Omega^{\bullet \geq n }$.

Then on this object the general cohesive integration map of def. \ref{CohesiveIntegrationOfDifferentialForms} reduces on the $-n$th [[homotopy group]] to the tradition [[fiber integration]] of differential forms as \hyperlink{Description}{above}:

\begin{displaymath}
\int_{(\Delta^1 \times X)/X} 
  \;\colon\;
  \Omega(\Delta^1 \times X)_{cl}^n
  \longrightarrow
  \Omega^{n-1}(X)/im(\mathbf{d})
  \,.
\end{displaymath}
\end{prop}
(\hyperlink{BunkeNikolausVoelkl13}{Bunke-Nikolaus-V\"o{}lkl 13, lemma 4.2 (7)}

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\begin{itemize}%
\item \emph{[[Stokes theorem]]}


\item [[kernel of integration is the exact differential forms]]



\end{itemize}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[Lie integration]]


\item [[cohomological integration]]


\item [[iterated integral]], [[parallel transport]], [[holonomy]]


\item [[absolute differential form]], [[cogerm differential form]]


\item [[motivic integration]], [[p-adic integration]]



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

An exposition with an eye towards applications in [[physics]] is in section 3 of

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

\end{itemize}
Discussion in the abstract context of [[cohesion]] and [[differential cohomology]] is in

\begin{itemize}%
\item [[Ulrich Bunke]], [[Thomas Nikolaus]], [[Michael Völkl]], \emph{Differential cohomology theories as sheaves of spectra} (\href{http://arxiv.org/abs/1311.3188}{arXiv:1311.3188})

\end{itemize}
[[!redirects integral of differential forms]] [[!redirects integrals of differential forms]]



\end{document}