$\newcommand{\SMT}{\mathsf{SMT}}$
$\newcommand{\NMT}{\mathsf{NMT}}$
$\newcommand{\NOM}{\mathbf{NOM}}$
$\newcommand{\ORD}{\mathbf{ORD}}$
$\newcommand{\PROP}{\mathsf{PROP}}$
$\newcommand{\nPROP}{\mathsf{nPROP}}$
$\newcommand{\Prop}{\mathsf{Prop}}$
$\newcommand{\nProp}{\mathsf{nProp}}$
$\newcommand{\F}{\mathbb{F}}$
$\newcommand{\nF}{{\mathsf{n}\mathbb{F}}}$
$\newcommand{\A}{\mathbb{A}}$
$\newcommand{\nA}{{\mathsf{n}\mathbb{A}}}$
$\newcommand{\lsem}{[\![}$
$\newcommand{\rsem}{]\!]}$
$\newcommand{\lbox}[1]{\lsem #1 \rangle\!\rangle}$
$\newcommand{\rbox}[1]{\langle\!\langle #1 \rsem}$
$\newcommand{\nfnmt}{\mathit{nfnmt}}$

# SMT and NMT

## Preliminaries

The set (or category ?) $\SMT$

The set (or category ?) $\NMT$

The category $\PROP$

The category $\nPROP$

For any PROP $\mathcal S$ there is a nominal PROP
$\NOM(\mathcal S)$. In fact, there is a functor

$$\NOM:\PROP\to\nPROP$$

For any nominal PROP $\mathcal T$ there is a PROP
$\ORD(\mathcal T)$. In fact, there is a functor

$$\ORD:\nPROP\to\PROP$$

We have seen in the CALCO paper that these functors constitute an equivalence of categories.

## $\nF$ is the $\nPROP$ of $\F$

Recall that $\F$ is the category of finite cardinals and all functions. $\NOM(\F)$ is the category of finite nominal subsets of the set of names:

**Proposition (nF):** There is an isomorphism of categories $\NOM(\F)\cong \nF$.

*Proof:* We define functors $\phi:\NOM(\F)\to\nF$ and $\psi:\nF\to\NOM(\F)$.

$$\phi([a\rangle g\langle b]) = \lbox a g\rbox b$$

where the "semantic box" needs to be defined. (Recall that $g$ here is a function between cardinals). [^needtoshow]
[^needtoshow]: We define $\phi$ on the free nPROP generated by the $[a\rangle g\langle b]$ ... then $\phi$ is a homomorphism of nPROP by definition ... then we have to show that $\phi$ preserves the equations of $E_{SNMT}$ ... to show that $\phi$ is onto and injective we define $\psi$ next

Conversely, consider $f:A\to B$. We associate to each object $A$ a short list $a$. Then, we define [^needtoshow2]

$$\psi(f)=[a\rangle\rbox a f \lbox b \langle b]$$

$\phi\circ\psi$ is the identity because $\lbox a\rbox a$ is the identity.

**We need to show** that $\psi\circ\phi$ is the identity.

## From Theories to Categories

There are functors

$$\Prop:\SMT\to\PROP$$

$$\nProp:\NMT\to\nPROP$$

taking a theory $\langle\Sigma,E\rangle$ to the category which has arrows given by $Term(\Sigma)$ and quotiented by $E$.

## From SMT to NMT

Given an SMT $(\Sigma,E)$, there is a translation of terms

\begin{align}
nmt: Term_\SMT(\Sigma) & \ \to \ Term_\NMT(Term_\SMT(\Sigma))\\
t & \ \mapsto\ [a\rangle t\langle b]
\end{align}

and of equations

$$nmt(E) \cup E_{SNMT}$$

where $E_{SNMT}$ denotes the equations of the translation.

This defines an operation

$$nmt:\SMT\to\NMT$$

There is a translation of terms
\begin{align}
nf: Term_\NMT(Term_\SMT(\Sigma)) & \ \to \ Term_\NMT(\Sigma)
\end{align}

which induces a translation of theories from $\langle\Sigma,E\rangle$ to $\langle\Sigma,nf(nmt(E))\rangle$

\begin{align}
\sigma & \ \mapsto\ \sigma\\
t=t' & \mapsto\ nf \circ nmt(t)=nf\circ nmt(t')
\end{align}

This defines an operation

$$\nfnmt:\SMT\to\NMT$$

**Proposition (from SMT to nPROP):** For any SMT $\langle \Sigma, E\rangle$, we have

\begin{align}
& \nProp\langle Term_\NMT(Term_\SMT(\Sigma), nmt(E)\cup E_{SNMT}\rangle \cong \\
&
\nProp\langle Term_\NMT(\Sigma), nmt(E)\rangle
\end{align}

or, in shorter form,

\begin{align}
& \nProp (nmt\langle\Sigma,E\rangle) \cong
\nProp (\nfnmt\langle\Sigma,E\rangle)
\end{align}

*Proof:* ...

## Completing the square, from SMT to NMT

**Proposition (completing the square from SMT):** For any SMT $\langle\Sigma,E\rangle$ we have

$$\NOM(\Prop\langle\Sigma,E\rangle)\cong \nPROP(\nfnmt\langle\Sigma,E\rangle)$$

**Remark:** there should be an analogous proposition starting at NMT.

*Proof:* Let

$$\mathbb A\ =\ \Prop\langle\Sigma,E\rangle$$

and

$$\nA=\nPROP(\nfnmt\langle\Sigma,E\rangle)$$

We define functors $\phi:\NOM(\A)\to\nA$ and $\psi:\nA\to\NOM(\A)$ as follows. For $g\in\Sigma$, we let

$$\phi([a\rangle g\langle b]) = \lbox a g\rbox b$$

and extend to $\A$ by induction. Then $\phi$ is a morphism of $\nPROP$s by definition. The equations defining $\NOM$ guarantee that the equation $\phi([a\rangle g\langle b]) = \lbox a g\rbox b$ holds not only for generators, but for all $g$ in $\Prop\langle\Sigma,E\rangle$.

Conversely, let $\sigma\in\Sigma$ and $[a\rangle\sigma\langle b]$ in $\nA$. Then we define $\psi:\nA\to\NOM(\A)$ on generators as

$$\psi([a\rangle\sigma\langle b])=[a\rangle\sigma\langle b]$$

and extend inductively to all of $\nA$.

$\phi\circ\psi$ is the identity because $\lbox a\rbox a$ is the identity.

Conversely, for $\psi\circ\phi$ and $g\in\A$ we have

\begin{align}
\psi(\phi(g))
&=
[\overrightarrow A\rangle
\rbox{\overrightarrow A}
\lbox a g \rbox b
\lbox{\overrightarrow B}
\langle \overrightarrow B]
\\
&=
[\overrightarrow A\rangle
\langle\overrightarrow A]
[ a\rangle g \langle b ]
[\overrightarrow B\rangle
\langle \overrightarrow B]
\\
&=
[ a\rangle g \langle b ]
\end{align}

## Completeness for $\nF$

Completeness for $\F$ is the statement that the PROP presented by $\langle\Sigma_\F,E_\F\rangle$ is isomorphic to the category $\F$ of finite cardinals and functions.

$$\Prop\langle\Sigma_\F,E_\F\rangle \cong \F$$

Completeness for $\nF$ is the statement that the nominal PROP presented by $\langle\Sigma_\nF,E_\nF\rangle$ is isomorphic to the category $\nF$ of finite sets of names and functions.

$$\nProp\langle\Sigma_\nF,E_\nF\rangle \cong \nF$$

The idea to prove completeness for $\nF$ from completeness of $\F$ is the following.

Starting with $\langle\Sigma_\F,E_\F\rangle$, we know $\Prop\langle\Sigma_\F,E_\F\rangle \cong \F$.

From Proposition (completing the square) we know that

$$\NOM(\Prop\langle\Sigma_\F,E_\F\rangle)\cong \nProp(\nfnmt\langle\Sigma_\F,E_\F\rangle)$$

From Proposition (nF) we know that

$$\NOM(\F)\cong \nF$$

From completeness of for $\F$ we know

$$\Prop\langle\Sigma_\F,E_\F\rangle \cong \F$$

Putting these together, we obtain

$$\nProp(\nfnmt\langle\Sigma_\F,E_\F\rangle)\cong \nF$$

that is, $\nfnmt\langle\Sigma_\F,E_\F\rangle$ is complete for $\nF$.

## Completeness for other nominal calculi ?

We can certainly do bijections, injections, ...

## Completing the square, from NMT to SMT

**Proposition (completing the square from NMT):** For any NMT $\langle\Sigma,E\rangle$ we have

$$\ORD(\nProp\langle\Sigma,E\rangle)\cong \PROP(\langle\Sigma,ord(E)\rangle)$$

*Proof:* Let

$$\nA\ =\ \nProp\langle\Sigma,E\rangle$$

and

$$\A=\nPROP(\langle\Sigma,ord(E)\rangle)$$

We define functors $\phi:\ORD(\nA)\to\A$ and $\psi:\A\to\ORD(\nA)$ as follows. For $g\in\Sigma$, we let

$$\phi(\langle a] g [b\rangle) = \rbox a g\lbox b$$

and extend to $\A$ by induction. Then $\phi$ is a morphism of $\PROP$s by definition. The equations defining $\ORD$ guarantee that the equation $\phi(\langle a] g [b\rangle) = \rbox a g\lbox b$ holds not only for generators, but for all $g$ in $\nProp\langle\Sigma,E\rangle$.

Conversely, consider $f:\bf n\to\bf m$ in $\A$. For each number $n$ choose globally a short list of $n$ names written as $\overrightarrow n$. Then, we define

$$\psi(f)=
\langle\overrightarrow n]
\lbox{\overrightarrow n}
f
\rbox{\overrightarrow m} [ \overrightarrow m\rangle$$

$\phi\circ\psi$ is the identity because $\rbox{\overrightarrow n}
\lbox{\overrightarrow n}$ is the identity.

Conversely, for $\psi\circ\phi$ and $g\in\nA=\nPROP(\langle\Sigma,ord(E)\rangle)$ we have

\begin{align}
\psi(\phi(g))
&=
\langle\overrightarrow n]
\lbox{\overrightarrow n}
\rbox a g\lbox b
\rbox{\overrightarrow m} [ \overrightarrow m\rangle\\
&=
\langle\overrightarrow n]
[\overrightarrow n\rangle
\langle a] g [b\rangle
\langle\overrightarrow m][\overrightarrow m\rangle\\
&=
\langle a] g [b\rangle
\end{align}

## Completeness of SMTs from NMTs?

[^needtoshow2]: Need to show that $\psi$ is a homomorphism. For example, for $f:A\to C$ and $g:C\to B$ in $\nF$,
\begin{align}
\psi(f;g)
&=[a\rangle \rbox a \,(f;g)\,\lbox b\langle b] & \textrm{def of } \psi
\\
&=[a\rangle \rbox a \,( f\lbox c \rbox c g \,)\,\lbox b\langle b] & \lbox c ; \rbox c= id
\\
&=[a\rangle
\,(\, \rbox a f\lbox c \,)\, ;
\,(\, \rbox c g\lbox b\,)\,
\langle b]
& \textrm{set theory}
\\
&=[a\rangle \rbox a f\lbox c \langle c ] ; [c\rangle \rbox c g\lbox b\langle b] & E_{SNMT}\\
&= \psi(f);\psi(g) & \textrm{def of } \psi
\end{align}
and for $f:A\to B$ and $g:C\to D$ with $X=A\cup C$ and $Y=B\cup D$
\begin{align}
\psi(f\uplus g)
&= [x\rangle\rbox{x} \,f\uplus g\ \lbox{y}\langle y]
& \textrm{def of } \psi
\\
&= [x\rangle\rbox x\lbox{a+c}\rbox{a+c} \,f\uplus g\ \lbox{b+d}\rbox{b+d}\lbox{y}\langle y]
& \lbox{a+c}\rbox{a+c}=id
\\
&= [x\rangle\rbox x\lbox{a+c} \ (\ \rbox{a} \,f\,\lbox{b} \oplus \rbox c \,g\ \lbox{d} \ )\ \rbox{b+d}\lbox{y}\langle y]
& \textrm{set theory }
\\
&= [x\rangle\langle x|a+c\rangle \ (\ \rbox{a} \,f\,\lbox{b} \oplus \rbox c \,g\ \lbox{d} \ )\ \langle b+d|y\rangle\langle y]
& \textrm{def of $\langle x|a+c\rangle$ }
\\
&= [a+c\rangle \ (\ \rbox{a} \,f\,\lbox{b} \oplus \rbox c \,g\ \lbox{d} \ )\ \langle b+d]
& E_{SNMT}
\\
&= [a\rangle \rbox{a} \,f\,\lbox{b} \langle b]
\uplus
[c\rangle\rbox c \,g\ \lbox{d} \langle d]
& E_{SNMT}
\\
&= \psi f \uplus\psi g
& \textrm{def of $\psi$ }
\end{align}

[^needtoshow3]: Should be similar to Proposition (nF).