$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\u}[1]{ \underline{#1} }
\newcommand{\In}{ \text{ in }}
\newcommand{\hyp}{\text{-} }
\newcommand{\H}{\text{-} }
\newcommand{\twoto}{\Rightarrow }
`$
プロファイル:
$`\quad (\u{\mbb{L}_\Sigma})_\mrm{obj} : |P\H\mbf{Bun}_C| \to |P\H\mbf{Bun}_C| \In \mbf{SET}`$
定義:
$`\text{For }P : \mbf{Set} \to \mbf{Set} \In \mbf{CAT}\\
\text{For }C \in |\mbf{Set}| \\
\text{For }\Sigma \in |P\H\mbf{Sign}_C| \\
\quad (\u{\mbb{L}_\Sigma})_\mrm{obj} :=
\lambda\, X\in |P\H\mbf{Bun}_C |.\,\Phi(X) \\
\quad \text{where }\: \Phi(X) := \\
{\displaystyle
\qquad \int_{P(C)}
\lambda\, A\in P(C).\left(\\
\qquad\qquad \left(\sum_{H\in |P\H\mbf{Bun}^\mrm{fin}_C| }
\mrm{Templ}^\Sigma_X(H, A) \times P\H\mbf{Bun}_C(H, X)
\right)/\sim\\
\qquad\quad \right)\\
}
`$
別レイアウト:
$`\text{For }P : \mbf{Set} \to \mbf{Set} \In \mbf{CAT}\\
\text{For }C \in |\mbf{Set}| \\
\text{For }\Sigma \in |P\H\mbf{Sign}_C| \\
\quad (\u{\mbb{L}_\Sigma})_\mrm{obj} :=
\lambda\, X\in |P\H\mbf{Bun}_C |.\,\Phi(X) \\
\quad \text{where }\: \Phi(X) := \\
\qquad {\displaystyle\int_{P(C)}}
\lambda\, A\in P(C).(\\
\qquad\qquad \left({\displaystyle\sum_{H\in |P\H\mbf{Bun}^\mrm{fin}_C| }}
\mrm{Templ}^\Sigma_X(H, A) \times P\H\mbf{Bun}_C(H, X)
\right)/\sim\\
\qquad\qquad )
`$