デルタテンソルの定義

$`\require{color}
%\newcommand{\Imp}{\Rightarrow}
% ---
\newcommand{\In}{ \text{ in }}
%\newcommand{\cat}[1]{\mathcal{#1} }
%\newcommand{\id}{\mathrm{id} }
%\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\mrm}[1]{ \mathrm{#1} }
%\newcommand{\u}[1]{ \underline{#1} }
% ---
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\C}[1]{ \textcolor{blue}{\text{#1}} }
\newcommand{\Definition}{\text{🔴}\Keyword{Definition } }
\newcommand{\WeDefine}{\Keyword{WeDefine } }
\newcommand{\WeWillDefine}{\Keyword{WeWillDefine } }
\newcommand{\WeHaveDefined}{\Keyword{WeHaveDefined } }
%\newcommand{\Notation}{\Keyword{Notation } }
\newcommand{\For}{\Keyword{For } }
\newcommand{\Let}{\Keyword{Let } }
\newcommand{\When}{\Keyword{When } }
\newcommand{\Where}{\Keyword{Where } }
\newcommand{\Then}{\Keyword{Then } }
% ---
\newcommand{\if}{\C{if }}
\newcommand{\then}{\C{ then }}
\newcommand{\else}{\C{ else }}
%`$

$`\Definition\\
\For A \in |{\bf Set}|\\
\WeWillDefine \delta_A : A \to {\bf B} \In {\bf Set}\\
\For a \in A\\
\WeDefine \delta_A(a) := 1 \;\in{\bf B}\\
\Then\\
\WeHaveDefined \delta_A \in {\bf UTens}( (A) )
%`$


$`\Definition\\
\For n \in {\bf N}\\
\WeWillDefine \delta^{(n)} \in
\prod_{S\in \mrm{MAP}(\bar{n}, |{\bf Set}|) } \mrm{Map}(\prod( S), {\bf B})\\
\text{i.e. }\delta^{(n)}_S \in \mrm{Map}(\prod( S), {\bf B})\\
\For S \in \mrm{MAP}(\bar{n}, |{\bf Set}|)\\
\text{i.e. } S \text{ is a table-schema or a profile.}\\
\WeWillDefine \delta^{(n)}_S : \prod( S) \to {\bf B} \In {\bf Set}\\
%
\When n = 0\\
\quad \For S \in \mrm{MAP}(\bar{0}, |{\bf Set}|)\\
\quad \text{i.e. } S = \theta_{|{\bf Set}|} = ()\\
\quad \WeWillDefine \delta^{(0)}_{()} : \prod( () ) \to {\bf B} \In {\bf Set}\\
\quad \WeDefine \delta^{(0)}_{()} := \lambda\, *\in \prod( () ).(\, 1 \;\in {\bf B}\,) \\
\quad \Then\\
\quad \WeHaveDefined \delta^{(0)}_{()} \in {\bf UTens}( () )
\:\:\Where ()\in \mrm{MAP}(\bar{0}, |{\bf Set}|)\\
%
\When n = 1\\
\quad \For S \in \mrm{MAP}(\bar{1}, |{\bf Set}|)\\
\quad \text{i.e. } S = (A) \text{ for some }A\in |{\bf Set}|\\
\quad \Let A := S(1) \; \in|{\bf Set}|\\
\quad \Then S = (A)\\
\quad \WeWillDefine \delta^{(1)}_{(A)} : \prod( (A) ) \to {\bf B} \In {\bf Set}\\
\quad \WeDefine \delta^{(1)}_{(A)} := \lambda\, a\in \prod( (A) ).(\, 1 \;\in {\bf B}\,) \\
\quad \Then\\
\quad \WeHaveDefined \delta^{(1)}_{(A)} \in {\bf UTens}( (A) )
\:\:\Where (A)\in \mrm{MAP}(\bar{1}, |{\bf Set}|)\\\\
%
\When n = 2\\
\quad \For S \in \mrm{MAP}(\bar{2}, |{\bf Set}|)\\
\quad \text{i.e. } S = (A, B) \text{ for some }A, B \in |{\bf Set}|\\
\quad \Let A := S(1), B = S(2) \; \in|{\bf Set}|\\
\quad \Then S = (A, B)\\
\quad \WeWillDefine \delta^{(2)}_{(A, B)} : \prod( (A, B) ) \to {\bf B} \In {\bf Set}\\
\quad \WeDefine \delta^{(2)}_{(A, B)} := \lambda\, (a, b)\in \prod( (A, B) ).(\\
\qquad (\if a = b \then 1 \else 0) \;\in {\bf B}\,) \\
\quad \Then\\
\quad \WeHaveDefined \delta^{(2)}_{(A, B)} \in {\bf UTens}( (A, B) )
\:\:\Where (A, B)\in \mrm{MAP}(\bar{2}, |{\bf Set}|)\\\\
%
\When n \ge 3\\
\quad \For S \in \mrm{MAP}(\bar{n}, |{\bf Set}|)\\
\quad \WeWillDefine \delta^{(n)}_{(S(1), \cdots, S(n)) } : \prod( (S(1), \cdots, S(n) ) ) \to {\bf B} \In {\bf Set}\\
\quad \WeDefine \delta^{(n)}_{(S(1), \cdots, S(n))} := \lambda\, (a_1,\cdots, a_n)\in \prod( (S(1), \cdots, S(n)) ).(\\
\qquad \prod_{i, j\in \bar{n}} \delta^{(2)}_{( S(i), S(j) )}(a_i, a_j) \;\in {\bf B}\,) \\
\quad \Then\\
\quad \WeHaveDefined \delta^{(n)}_{S} \in {\bf UTens}( S )
\:\:\Where S \in \mrm{MAP}(\bar{n}, |{\bf Set}|)\\
\Then\\
\WeHaveDefined \delta \in \prod_{n\in {\bf N}}\prod_{S\in \mrm{MAP}(\bar{n}, |{\bf Set}|) } {\bf UTens}( S)
%`$