Kronecker Delta Function

The Kronecker delta function on a set X 𝑋 X with Decidable Equality is the function δ : X × X → 2 : 𝛿 → 𝑋 𝑋 2 \delta:X\times X\to 2 defined as

δ⁢(i,j)={1if ⁢i=j0if ⁢i≠j𝛿𝑖𝑗cases1if 𝑖𝑗0if 𝑖𝑗\par\delta(i,j)=\begin{cases}1&\text{if }i=j\\ 0&\text{if }i\neq j\\ \end{cases}