It is an $I$-complete parametrization as long as for every computable function $f \colon C \to B$, there is a Turing machine $t_f \colon I \to T$ satisfying

\begin{equation}\label{eq:TM_for_function}
\eval \bigl( t_f, \ph \bigr) = f(\ph).
\end{equation}

This is true by definition of course.

The evaluation function would be a complete parametrization if for every computable function $f \colon A \otimes C \to B$ with two inputs, there is a family

\begin{equation}
\Family{ t_f(a) \colon I \to T  \given  a \in A }
\end{equation}

of Turing machines, indexed by elements of $A$ (thought of as a set), such that we have

\begin{equation}
\forall \, a \in A \qquad \eval \bigl( t_f(a), \ph \bigr) = f(a, \ph)
\end{equation}

and such that the assignment $a \mapsto t_f(a)$ is a computable function of type $A \to T$.

From the point of view of category theory, a better motivated concept than <ref> would be to require that $F$ is an $A$-complete parametrization for all objects $A$ in $\cC$.
In <cit.>, this notion has been called Kleene universality, in <cit.> universal application, and in <cit.> it is the defining property of the so-called program evaluator.

If there was a morphism $C \to B$ in $\cat{Tur}$ for which no suitable Turing machine $t_f$ satisfying <ref> exists, it would be an uncomputable function.
This is the rationale behind the following concept of unreachability, which stipulates that there are behaviors that are inaccessible.

Consider a target–context category with intrinsic behaviors.
A (universal) simulator $s$ has unreachability if the composite $\eval \circ s$ is not an $I$-complete parametrization of maps $C \to B$.

When we refer to unreachability for $P$, we implicitly have in mind a particular simulator of type $P \otimes C \to T \otimes C$ that it refers to.
Note that unreachability for the trivial simulator is of particular conceptual importance since morphisms of type $C \to B$ that cannot be parametrized by $\eval$ are also not required (by <ref>) to be parametrized by a universal simulator.
In that sense such morphisms are not taken into account by the definition of universality.

§.§ Unreachability from Universality and Negation

Let us now generalize Lawvere's Fixed Point Theorem <cit.> in a way that applies to our framework.
In its contrapositive form, this result says that if there is a morphism of type $B \to B$ without a fixed point (such as a negation), then no morphism of type $C \otimes C \to B$ is an $I$-complete parametrization.
For instance, if $T$ and $C$ are isomorphic, then this result entails unreachability for the trivial simulator.
However, this need not be the case for distinct targets and contexts.
Nevertheless, in <ref>, we show that for any universal simulator $s$
unreachability for $s$ implies unreachability for the trivial simulator.
Thus, if there is a negation $B \to B$ and a universal simulator whose programs coincide with contexts, we obtain unreachability .

A fixed point of a morphism $g \colon B\to B$ is a $b \colon A \to B$ that equals $g \circ b$.
If merely

\begin{equation}\label{eq:quasi-fixed}
\behim{b} \imrelop \behim{g} \circ \behim{b}
\end{equation}

holds, where $\behim{b}$ stands for $\Beh(b)$ as before, we say that $b$ is a quasi-fixed point of $g$.

Let $\cC$ be a target–context category with intrinsic behaviors.
If there is a morphism $F \colon C \otimes C \to B$ that is an $A$-complete parametrization of maps $C \to B$ (for some $A$), then every morphism $g \colon B \to B$ has a quasi-fixed point.

There is a similar version of the theorem in any gs-monoidal category without the structure of a target–context category with intrinsic behaviors.
In this case, the notion of a complete parametrization uses equality instead of relation $\imrel$ in (<ref>) and the conclusion is that every $g$ has a fixed point (rather than a quasi-fixed point).
To recover the original Lawvere's Fixed Point Theorem for products from <cit.>, one can instantiate this version in a cartesian monoidal category (which is automatically gs-monoidal) with $A = I$.

Consider an arbitrary $g \colon B \to B$ and define a morphism

\begin{equation}\label{eq:Lawvere_1}
\tikzfig{Lawvere_1}
\end{equation}

which depends on $g$.
Because $F$ is an $A$-complete parametrization, there exists a morphism ${c_f \in \cC_{\rm fun} (A,C)}$ satisfying

\begin{equation}\label{eq:Lawvere_2}
\tikzfig{Lawvere_2}
\end{equation}

Since $c_f$ is functional, the leftmost equation in the chain

\begin{equation}\label{eq:Lawvere_3}
\tikzfig{Lawvere_3}
\end{equation}

follows, while the second relation holds by (<ref>) and the third one by the definition of $f$ in (<ref>).
Consequently, $\gamma \circ c_f$ is a quasi-fixed point of $g$, where $\gamma \coloneqq F \circ \cop_C$.

To gain an intuition of the proof of <ref>, consider $F$ to be the evaluation function ${\eval \colon C \otimes C \to B}$, where we pick a particular isomorphism between strings $C$ and Turing machines $T$, i.e. a computable enumeration of Turing machines with a computable inverse.
Then the key object in the proof is the “self-referential constructor” $\gamma \colon C \to B$ given by $F \circ \cop_C$.
It is a function that takes a generic string $c \colon I \to C$ and runs the Turing machine enumerated by it with input given by $c$ itself.
The fixed point of $g$ is the outcome of running the self-referential constructor $\gamma$ with input given by $c_f$, which is constructed using both $\gamma$ and $g$.

Consider the same situation as in <ref> except for the additional assumption that

*  $F\colon C \otimes C \to B$ is total

*  $F$ is an $A$-complete parametrization (for some $A$) by total morphisms, i.e. for any ${f\colon A \otimes C \to B}$ there exists a total $c_f \colon C \to A$ such that <ref> holds.

Then every morphism $g \colon B \to B$ has a total quasi-fixed point.

Following the same reasoning as in the proof of <ref>, the additional assumptions imply that the quasi-fixed point (as a morphism in $\cC$) constructed in the leftmost expression in (<ref>), is total.

[The non-existence of a total universal Turing machine]
Consider the target–context category $\cat{Tur}^\intr$.
We use <ref> to recover the known fact that there does not exist a total universal Turing machine.
Equivalently, this means that there is no total computable function $u \colon T \times C \to B$ that satisfies

\begin{equation}\label{eq:total compl}
u(t,c) = t(c)
\end{equation}

whenever the Turing machine $t$ halts on input $c$.
To do so, we show that, in $\cat{Tur}^\intr$, there is no universal simulator $s$ with a lax reduction $r^* \colon s \to \id$ such that the composite

\begin{equation}\label{eq:total_computable}
\tikzfig{total_computable}
\end{equation}

is a total morphism.
This is a stronger statement because, for every such simulator, the composite above is a total computable function satisfying <ref>.
In particular, since the trivial simulator is universal with a lax reduction given by the identity, we obtain that $\eval$ itself cannot be a total computable function.

We prove the above claim by contradiction.
That is, consider a simulator $s$ with the desired properties.
Letting $F$ from <ref> be the morphism in diagram (<ref>), condition <ref> is satisfied by assumption.
Moreover, $\eval$ is not just an $I$-complete parametrization as argued in <ref>, but it in fact satisfies the stronger condition <ref> in <ref>.
Since $s$ is universal, using a similar reasoning as in <ref> we conclude that $F$ also satisfies this condition.
Hence, we conclude that every morphism $g\colon B \to B$ has a total quasi-fixed point by <ref>.
This, however, is not true.
For instance, the succesor function does not have a total quasi-fixed point.
Such a simulator therefore cannot exist.

Provided an intrinsic behavior structure, a good candidate for a complete parametrization in $\cC$ is the evaluation morphism $\eval \colon T \otimes C \to B$.
However, in order to apply Lawvere's Fixed Point Theorem, we need to relate its two inputs — targets and contexts — like in the above example of Turing machines with an isomorphism between the two sets.
One way to do so more generally is to use a simulator with programs identical to the contexts $C$.
Such a simulator allows us to construct a composite morphism $\eval \circ s$ with identical inputs.
Let us show that this composite is a complete parametrization as long as $s$ is universal and $\eval$ is itself a complete parametrization.
Having such a universal simulator allows one to build the self-referential constructor $\gamma$ and in this sense universality allows for self-reference.

Consider an intrinsic behavior structure where $\eval$ is an $A$-complete parametrization of maps $C \to B$.
If $s$ is a universal simulator, then $\eval \circ s \colon P \otimes C \to B$ is also an $A$-complete parametrization.

By assumption, we have that for any $f \colon A \otimes C \to B$ there is a functional $t_f \colon A \to T$ such that

\begin{equation}\label{eq:eval_compl_para}
\tikzfig{eval_compl_para}
\end{equation}

Let us denote the reduction of $s$ to the trivial simulator by $r \colon T \to P$.
Then for every $t_f$ we define $p_f \coloneqq r \circ t_f$, for which

\begin{equation}\label{eq:weak_pt_surj}
\tikzfig{weak_pt_surj}
\end{equation}

holds by <ref>.
Note that $p_f$ is a composition of functional morphisms and thus functional itself.
Combining relations (<ref>) and (<ref>) shows that $\eval \circ s$ is an $A$-complete parametrization of maps $C \to B$.

In the contrapositive form, <ref> says that given a universal simulator whose evaluation is not a complete parametrization, we necessarily have unreachability in the sense of <ref>.
This is the meaning of the implication mentioned in the sec:Introduction:

unreachability (for $P$) + universality $\implies$ unreachability (for particular solutions in $T$),

where we think of unreachability for $P$ as saying that the morphism $\eval \circ s$ that is not an $I$-complete parametrization.

In the framework of monoidal , the above complete parametrization property of $\eval \circ s$ is among the axioms of the framework.
As mentioned in <ref>, $\eval \circ s$ corresponds to the so-called universal evaluation denoted by $\{\}$, which is assumed to be programmable <cit.>.
That is, for every computation $f \colon C \to B$, there exists a program $p \colon I \to P$ such that composing the universal evaluation with $p$ yields $f$.
In light of <ref>, it is appropriate to think of a universal evalulation from <cit.> as a composition of the evaluation function $\eval$ with a universal simulator $s$ rather than a generic simulator.

Consider an intrinsic behavior structure where $\eval$ is a $A$-complete parametrization of maps $C \to B$.
If there exists a universal simulator $s$ of type $C \otimes C \to T \otimes C$, then every morphism $g \colon B \to B$ has a quasi-fixed point.

By <ref>, $\eval \circ s$ is a complete parametrization and the claim follows from <ref>.

The contrapositive of <ref> says:
If there is a morphism $B \to B$ without a quasi-fixed point, then either $\eval$ is not a complete parametrization or there is no universal simulator of type $C \otimes C \to T \otimes C$.
While morphisms without quasi-fixed points can arise in many circumstances, the paradigmatic example is the negation that exchanges the truth values of a Boolean variable.
This fixed-point-free morphism is the one that is generally used to prove undecidability and other kinds of unreachability.
We can thus summarize the contrapositive of <ref> with the slogan (depicted in <ref>):

negation + universality $\implies$ unreachability

* negation refers to a quasi-fixed-point-free morphism of type $B \to B$,

* universality refers to the existence of a universal simulator with $P = C$, and

* unreachability refers to unreachability of the trivial simulator in the sense of <ref>.

In a target–context category with intrinsic behaviors (<ref>), if there exists a universal simulator $s$ of type $C\otimes C\to T\otimes C$, and a morphism $B\to B$ without a quasi-fixed point (such as negation), then the trivial simulator has unreachability.
This means that there is a morphism $f \colon C\to B$ for which $\eval(t,\ph) \imrelop f(\ph)$ does not hold for any $t \colon I\to T$.

[Cantor's Theorem]
Consider the ambient category $\cat{Set}$ of sets and functions with the canonical shadow functor given by the inclusion into $\cat{Rel}$.
For the intrinsic behaviour structure, we take an arbitrary set $C$ as contexts, the power set $[2]^C$ as targets, the evaluation $\eval \colon [2]^C \times C \to [2]$ to be

\begin{equation}
\eval(t,c) \coloneqq t(c)
\end{equation}

and $\brel$ as the equality relation on $[2] \coloneqq \{0,1\}$.
Clearly, there exists a function $g \colon [2] \to [2]$ without a quasi-fixed point, namely the negation given by

\begin{equation}
g(0) = 1 \qquad \qquad g(1) = 0.
\end{equation}

Moreover, by construction, $\eval$ is a complete parametrization of maps $C \to [2]$.
Hence, by <ref>, there does not exist a universal simulator $s \colon C \times C \to [2]^C \times C$.

Cantor's Theorem says that there is no surjective map of type $l \colon C \to [2]^C$.
If there was such an $l$, then the simulator with compiler $s_T \coloneqq l$ and context reduction $s_C \coloneqq \discard_C \times \id_C$ would clearly be universal with respect to the lax reduction given by any right inverse of $l$.

Let us now argue that the existence of a universal simulator $s$ as above is in fact equivalent to the existence of such a surjection.
By definition, if $s$ is universal, then there exists a function $r \colon [2]^C \to C$ such that we have

\begin{equation}\label{eq:Cantor_1}
\tikzfig{Cantor_1}
\end{equation}

since the imitation relation is also the equality relation by <ref>.
Taking $A = C$ and the function $\eval \circ s \colon C \times C \to [2]$ as $f$ in <ref>, we obtain that there is a function $l \colon C \to [2]^C$ satisfying

\begin{equation}\label{eq:Cantor_2}
\tikzfig{Cantor_2}
\end{equation}

because $\eval$ is a $C$-complete parametrization.
Precomposing <ref> with $r \times \id_C$ and using <ref> to simplify the right-hand side gives

\begin{equation}\label{eq:Cantor_3}
\tikzfig{Cantor_3}
\end{equation}

Therefore, by the universal property of $[2]^C$ as an exponential object, we obtain $l \circ r = \id_{[2]^C}$ or in other words that $r$ is a right inverse of $l$.
This implies that $l$ is indeed a surjection of type $C \to [2]^C$.
Hence, <ref> allows us to restate Cantor's Theorem as the non-existence of universal simulators of a certain type.

§.§ Complete Parametrization and Singleton Universal Simulators

In this section, we discuss two general methods to construct singleton universal simulators in target–context categories with reachability.
Recall that $s$ is a singleton simulator if the functional image of the compiler $s_T$ is a single element $u \colon I \to T$.
If, additionally to the assumptions of <ref>, we have $B=C$, then there exists a singleton universal simulator which uses $\eval$ as the context reduction.
If, in addition, $T\otimes C$ can be reversibly embedded within $C$, there also exists another singleton universal simulator with the embedding $\sigma$ as a context reduction.

Consider an intrinsic behavior structure satisfying $B = C$ and where $\eval$ is a $I$-complete parametrization of maps $C \to C$.

There is a $t_{\id} \colon I\to T$ such that

\begin{equation}
\tikzfig{retract_singleton}
\end{equation}

is a singleton universal simulator of type $T\otimes C \to T \otimes C$.

If $T\otimes C$ is a retract of $C$, with section $\sigma \colon T\otimes C \to C$ and retraction $\pi \colon C \to T\otimes C$, then there is a $t_u \colon I\to T$ such that

\begin{equation}
\tikzfig{retract_singleton_2}
\end{equation}

is a singleton universal simulator of type $T\otimes C \to T \otimes C$.

Note that property <ref> holds under a weaker assumption than that of $\eval$ being a complete parametrization.
The only fact we need about $\eval$ to prove universality of this simulator is that there be a functional state $t_{\id} \colon I\to T$ satisfying

\begin{equation}\label{eq:t_id}
\tikzfig{t_id}
\end{equation}

This, of couse, holds under the assumed complete parametrization property.
Let us now prove statements <ref> and <ref>.

Precomposing relation (<ref>) with $\eval$ and using the fact that imitation relations are preserved by precomposition (see the proof of <ref>), we obtain

\begin{equation}\label{eq:t_id_2}
\tikzfig{t_id_2}
\end{equation}

which says $s_{\rm id} \mrelop \id_{T \otimes C}$, so that $s_{\rm id}$ is a universal simulator indeed.

The composite $u \coloneqq  \eval \circ \pi$ is a morphism of type $C \to B$.
As $\eval$ is a complete parametrization by assumption, there is a functional state $t_u \colon I\to T$ such that

\begin{equation}\label{eq:singleton_proof_1}
\tikzfig{singleton_proof_1}
\end{equation}

holds, which is nothing but $t_u \otimes \id_C \mrelop \pi$.
Precomposing the latter relation with $\sigma$ and using the assumed $\pi \circ \sigma = \id_{T \otimes C}$ we get

\begin{equation}\label{eq:singleton_proof_2}
\tikzfig{singleton_proof_2}
\end{equation}

which proves the claim that $s_u$ is a universal simulator.

Note that both simulators constructed in <ref> identify programs and targets, i.e. we have ${P=T}$.
That is why they cannot be used to obtain a non-trivial application of <ref>.

§ COMPARING INSTANCES OF THE FRAMEWORK

In this paper, we focus on studying individual target–context categories and concepts that can be described within each such instance of our framework — (universal) simulators, their reductions, morphisms, etc.
However, we also pave the way for explorations of questions that have to do with multiple, a priori distinct, notions of universality.
To do so, we define target–context functors  (<ref>) and show that the construction of simulator categories is functorial with respect to it.
That is, given a relation at the level of ambient categories (the target–context functor), one obtains a functor between the corresponding simulator categories (<ref>).
Moreover, the induced functor preserves universality of simulators.

A target–context functor preserves targets, contexts, and the behavioral relation (<ref>).

Consider two target–context categories $(\cC, T, C, \mrel)$ and $(\cC',T',C', \mrel')$.
A target–context functor of type $(\cC, T, C, \mrel) \to (\cC',T',C', \mrel')$ is a strong gs-monoidal functor $F \colon \cC \to \cC'$ which preserves targets, contexts and the behavioral relation.
That is, we have

\begin{align}
F(T) &= T', \\
F(C) &= C',
\end{align}

\begin{equation}
f \mrelop g \quad \implies \quad F(f) \mrelop' F(g)
\end{equation}

for all $A$, and all $f,g \colon A \to T\otimes C$.

The construction of simulator categories is functorial with respect to target–context functors (<ref>).

A target–context functor ${F\colon \mathcal{A} \to \mathcal{A}'}$ induces a functor $\mathrm{Sim}(F) \colon \textrm{Sim}(\mathcal{A}) \to  \textrm{Sim}(\mathcal{A}')$ defined as:

\begin{equation}
s \mapsto Fs  \qquad  (r^*,q_*) \mapsto \big ((F r)^*,(F q)_*\big)
\end{equation}

We omit any coherence isomorphisms of $F$.
We have to show that

*  given a simulator morphism $(q_*,r^*) \colon s_1 \to s_2$, we obtain a simulator morphism ${((F q)_*,(F r)^*) \colon F s_1 \to F s_2}$,

*  $ F$ maps identity morphisms to identity morphisms, and

*  $ F$ preserves the composition of simulator morphisms.

First, note that $F$ maps total morphisms of $\cC$ to total morphisms of $\cC'$ and functional morphisms to functional ones, as a direct consequence of being a strong gs-monoidal functor.
In particular, for any total $f \colon A\to B$, we find

\begin{equation}
\discard_{FB} = F(\discard_B) = F(\discard_B \circ f) = \discard_{FB} \circ Ff .
\end{equation}

Similarly, for any functional $f \colon A\to B$, we have

\begin{equation}
(Ff \otimes Ff)\circ \cop_{FA} = F \bigl( (f\otimes f)\circ \cop_A \bigr) = F(\cop_B \circ f) = \cop_{FB} \circ Ff .
\end{equation}

Let $s \colon P\otimes C \to T \otimes C$ be a simulator.
By definition, $s$ comes equipped with a splitting into $s_C$ and $s_T$ as in diagram (<ref>).
Applying $F$ to $s$, we thus find

\begin{equation}
Fs = (Fs_T \otimes Fs_C)\circ (\cop_{FP} \otimes \id_{FC}).
\end{equation}

Since $F$ preserves functionality of the compiler $s_T$, $Fs$ has the desired decomposition and is also a simulator.

To show property <ref>, consider a simulator morphism $(q_*,r^*) \colon s_1 \to s_2$.
That is, let ${q \colon P\otimes T \otimes C \to T \otimes C}$ be a processing, i.e. a simulator that satisfies relations (<ref>) and (<ref>).
We now show that $((Fq)_*,(Fr)^*)$ is a simulator morphism of type $F s_1 \to F s_2$.
Relation (<ref>) reads

\begin{equation}
\discard_P \otimes \id_T \otimes \id_C \mrelop q
\end{equation}

and applying $F$ to both sides yields

\begin{equation}
\discard_{FP} \otimes \id_{T'}\otimes \id_{C'} \mrelop' Fq,
\end{equation}

which is the appropriate relation (<ref>) in $\cC'$.
Similarly, applying $F$ to both sides of <ref> gives the relevant property in the image.
Since $F$ preserves the functionality of the reduction $r^*$, we find that $((Fq)_*,(Fr)^*)$ is indeed a simulator morphism of type $F s_1 \to F s_2$.

The identity simulator morphism $\id_s \colon s \to s$ is given by the pair

\begin{equation}
\Bigl( \bigl( \discard_P \otimes \id_{T \otimes C} \bigr)_*, \ \id_P^* \Bigr).
\end{equation}

Applying $F$ to its components, we obtain

\begin{equation}
\Bigl( \bigl( \discard_{FP} \otimes \id_{T' \otimes C'} \bigr)_*, \ \id_{FP}^* \Bigr),
\end{equation}

which is the identity simulator morphism $\id_{Fs}$.

Let $(q_{1*}, r_1^*) \colon s_1 \to s_2$ and $(q_{2*},  r_2^*) \colon s_2 \to s_3$ be two morphisms of simulators.
Their composition is given by $(\tilde q_*, (r_1\circ r_2)^*)$, where $\tilde q$ is given by <ref>.
Since $F$ preserves string diagrams, it also commutes with composition of morphisms.

Note that when $F\colon \cC \to \cC'$ and $G \colon \cC' \to \cC''$ then it additionally holds that $\mathrm{Sim}(G \circ F) = \mathrm{Sim}(G) \circ \mathrm{Sim}(F)$. In other words, mapping target–context categories $\cC$ to their corresponding simulator categories $\mathrm{Sim}(\cC)$ and target–context functors $F$ to their induced functors $\mathrm{Sim}(F)$
is itself functorial.

A target–context functor $F\colon \mathcal{A} \to \mathcal{A}'$ maps universal simulators to universal simulators and singleton simulators to singleton simulators.

Let $s \colon P \otimes C \to T \otimes C$ be a universal simulator, so that there exists a functional morphism ${r \colon T \to P}$ such that

\begin{equation}
s \circ (r \otimes \id_C) \mrelop \id_{T \otimes C}
\end{equation}

Using the assumption that $F$ preserves the ambient relation $\mrel$, we find

\begin{equation}
Fs \circ (Fr \otimes \id_{C'}) \mrelop' \id_{T' \otimes C'}.
\end{equation}

Since $F$ preserves functional morphisms, we conclude that $Fs$ is universal with the reduction given by $Fr$.

On the other hand, let $s$ be a singleton simulator, that is, one whose compiler satisfies ${s_T = t \circ \discard_P}$ for a state $t \colon I\to T$.
Since $F$ is strong gs-monoidal, we have

\begin{equation}
Fs_T = F(t \circ \discard_P) = Ft \circ \discard_{FP}
\end{equation}

where $Ft$ is a state of type $I'\to FT$.
Hence, $Fs_T$ is a singelton simulator.

Consider the situation of two instances of the framework with the same ambient category, same targets and same contexts, but distinct behavior relations.
Then the identity functor is a target–context functor if and only if the domain behavior relation implies the codomain one, i.e. if and only if we have
Since there is a behavioral relation for each $A \in \cC$, we need to interpret the inclusion (<ref>) also as being quantified over all objects of $\cC$.

\begin{equation}\label{eq:beh_enlarge}
\mrel \, \subseteq \, \mrel'.
\end{equation}

In particular, enlarging behavioral relations preserves universality of simulators by <ref>.

[Modifying the behavioral relation for Turing machines]
Let us exemplify this with Turing machines.
In <ref>, we define two ambient categories for which the identity functor $\cat{Tur} \to \cat{Tur}^\intr$ is a target–context functor because the respective behavioral relations indeed satisfy condition (<ref>).
By <ref>, every universal simulator in $\cat{Tur}$ is also a universal simulator in $\cat{Tur}^\intr$.  One can easily construct simulators that are universal in $\cat{Tur}^\intr$ but not in $\cat{Tur}$.

§ SUMMARY, CONCLUSIONS & OUTLOOK

In this work we provide a categorical framework for studying universality and related concepts.
It comes in two main variants.
Let us summarize the key results of our work and highlight which variant they rely on, respectively.

Results applicable to any target–context category
<Ref> of a target–context category sets up the minimal structure we need for our analysis.
It includes a specification of the morphisms of the ambient category $\cC$, an ambient relation $\mrel$, and objects $T$ and $C$ of targets and contexts.
Given this structure, we define simulators (<ref>), and their universality (<ref>).
In <ref>, we provide a recipe to generate necessary conditions for universality of a given simulator.
These are used to show that there is no universal spin model of finite cardinality (<ref>).
In order to compare simulators via the so-called parsimony ordering (<ref>), we propose the notion of a simulator category (<ref>), whose morphisms model ways to transform one simulator into another.
<Ref> then give conditions that allow one to decide whether such a morphism exists or not.
In <ref>, we use them to show that the simulator associated to a universal Turing machine (<ref>) is strictly more parsimonious than the trivial simulator.
Finally, we define target–context functors and show that they preserve simulator categories and universal simulators in <ref>.

Results applicable to target–context categories with intrinsic behaviors
Provided that the target–context category in question additionally has a behavior structure in accordance with <ref>, and in particular one that is intrinsic (<ref>), we can study fixed point theorems and unreachability (<ref>).
Specifically, <ref> generalizes Lawvere's original fixed point theorem to our framework.
One of its consequences is the fact that there exists no total universal Turing machine (<ref>).
In <ref>, we also prove that universal simulators allow one to further extend this result to the case of two non-isomorphic inputs.
To explicate its potential use, we show in <ref> that the non-existsence of certain universal simulators  is equivalent to the conclusion of Cantor's Theorem, namely that the power set always has a larger cardinality than the original set.

Instances of our framework
We illustrate our constructions and results with a wealth of examples.
The two most important examples are those of Turing machine universality and of universal spin models.
Besides the aforementioned concrete results, expressing spin systems in the framework helps us understand the meaning of spin model universality.

Others mentioned throughout the text include completeness for complexity classes (<ref>), cofinal subsets of preordered sets (<ref>), dense subsets of topological spaces (<ref>), and universal sets (<ref>).
Apart from completeness for complexity classes, all examples come with an intrinsic behavior structure.
Notably, however, among the two ambient categories for Turing machines that we present, only the one with more permissive ambient relation $\mrel$ has intrinsic behaviors.
See <ref> for more details.

Besides the above, we expect that there are many relevant instances of our framework, whose details are yet to be worked out:

* Universal graphs: A graph $G$ within a given class is called a universal graph if all graphs from this class can be embedded into $G$ (<cit.>).
Distinct notions of universality arise for different types of embeddings.
In the simplest case, a universal graph contains all other ones as subgraphs.

* Neural networks: In order to construct complex functions from basic building blocks, one can use neural networks.
By the universal approximation theorem <cit.>, feed-forward neural networks with one hidden layer can approximate any continuous function to arbitrary precision.
Analogous results hold for restricted Boltzmann machines <cit.>.
As such, these neural network architectures are universal for the task of expressing an unknown function in a compositional manner. (See also <cit.> for similarities between this type of universality, universal spin models and universal Turing machines).

* Universal grammar: In order to explain that an individual is capable of learning any natural language, Chomsky proposed the idea of a universal grammar as a `meta-grammar' with unfixed parameters <cit.> (see also <cit.>).
“Programming” (in the sense of our discussion from the sec:Introduction) is synonymous with fixing particular parameter values, upon which the universal grammar specializes to the grammar of any natural language.

* Generating sets: Every algebraic structure gives rise to the notion of a generating set.
For instance any set of vectors $S \coloneqq \{v_1, \ldots , v_k\}$ whose span is the whole vector space itself is termed a generating set of this vector space.
Generating sets can be seen as universal in the sense that every vector $v$ is a linear combination $\lambda_1 \cdot v_1+ \ldots + \lambda_k \cdot v_k$ for some coefficients, which we think of as the program for $v$.

* Universal quantum spin models: While <ref> captures universality for classical spin models, there are also notions of universality for quantum spin models <cit.>.

While all of the above can be instantiated in uninsightful ways — e.g. as a special case of <ref> of a cofinal subset (or, specifically, the top element) of a preordered set — the challenge is to find more informative target–context categories.
Not only should these notions of universality correspond to universal simulators therein, but one should also be able to recover relevant information about the way in which they are universal from the data provided, such as the context reduction $s_C$ or the lax reduction $r^*$ to the trivial simulator.

For instance, one could also think of a universal spin model in the sense of <cit.> as a cofinal subset of the set of all spin systems, given an appropriate preorder relation.
Two spin systems would be related if there is a spin system simulation <cit.> from one to the other.
In our treatment of spin model universality in <ref>, we go beyond such austere description.
The context reduction of a 2D Ising model simulator specifies, in particular, how to relate the respective spin configurations, which is part of the data needed to identify a simulation of spin systems.
Nevertheless, even our approach here leaves much to be desired.
For example, a generic context reduction does not satisfy some of desirable properties of a spin system simulation, such as the preservation of the hypergraph structure at the level of spin configurations <cit.>.
This is precisely the reason why a generic universal simulator in the target–context category $\cat{SpinSys}$ need not correspond to a universal spin model in the sense of <cit.>.

Potential further development of the framework
A related open problem is to establish desiderata for distinguishing between trivial and insightful ways to instantiate examples of universality in our framework.
One is that simulators (of particular type) can be shown to be universal if and only if an independently motivated notion of universality is present in the example.
This is the case for the ambient category $\cat{Tur}$ of Turing machines, but as we argue above, it is not true for the ambient category $\cat{SpinSys}$ of spin systems.
Certainly, an insightful instantiation would lead to an improved understanding of the situation at hand.
In this sense, our present spin system example is already non-trivial.

Additionally, we would like to understand the parsimony preorder of universal simulators better, both in specific instances and in the abstract.
This preorder identifies “non-trivial” universal simulators as those universal simulators that are strictly more parsimonious than the trivial simulator.
One may wish to characterize which target–context categories feature such non-trivial universality.
<Ref> serve as first steps in this direction.

We envision a generalization of the framework with unfixed targets $T$ and contexts $C$.
This would allow one to describe Turing completeness via the corresponding notion of universal simulators.

Universality beyond our framework
On a broader and less precise level, we would like to understand whether our framework relates to notions of universality that are not as easily expressible in the mathematical language used here.
One of them is the idea of xenobots <cit.>, which are biological systems that are capable of programmable biosynthesis.
Controlling (i.e.  programming) their environment allows one to implement a range of biological process that are not accessible by such a relatively simple system under normal circumstances.
A chemputer <cit.> — on the other hand — is a programmable modular system capable of chemical synthesis.
Universals in biology <cit.>, complex systems <cit.>, and statistical physics refer to emergent properties, which can serve as universal solutions (see the sec:Introduction) to the problem of explaining the phenomena of specific systems enjoying such emergence.
In this sense, instantiating these examples in our framework would amount to expressing universal explanations as the universality of certain simulators.
A general version of this problem is known as the problem of universals in metaphysics <cit.>.
We are taking some steps in these and related directions in the complementary work of <cit.>.

§ BACKGROUND ON CATEGORY THEORY

§.§ Basic Definitions

We start by providing some basic definitions.
For an introduction to category theory for readers with some background in mathematics, we recommend <cit.>.

A category $\cat{C}$ consists of a collection of objects and a collection of morphisms (or arrows) with the following properties:

* For every morphism $f$ there are two objects $A$ and $B$ called the domain and codomain of $f$, in which case we express this information as $f \colon  A \to B$ and refer to $A \to B$ as the type of $f$.

* For every object $A$, there is a morphism $\id_A \colon  A \to A$ called the identity morphism (on $A$).

* For every pair of morphisms $f \colon  A \to B$ and $g \colon  B \to C$, there is a morphism $g\circ f \colon  A \to C$ called the sequential composite of $f$ and $g$.

* Composing every morphism $f \colon  A \to B$, with identities gives $f$, i.e. $\id_B\circ f$ and $f\circ \id_A$ are both equal to $f$.

* Composition is associative, i.e. for all morphisms $f \colon  A \to B$, $g \colon  B \to C$ and $h \colon  C \to D$, we have $(h\circ g)\circ f = h\circ (g\circ f)$.

In words, the objects can be thought of as types (in the computer science way) and morphisms as functions mapping from one type to another.
Composition of morphisms is hence only possible when the output type of one morphism is the input type of the other.
Graphically, a (small) category can be imagined as a directed graph, where the objects are nodes and the morphisms are directed edges.

We depict morphisms of categories by string diagrams.
Each morphism $f \colon A \to X$ corresponds to a box such as

\begin{equation}
\tikzfig{box}
\end{equation}

while each object (and thus also each identity morphism) is a wire carrying a label with a name of the object.
For more details on string diagrams, see <cit.>.

Given two objects $A$ and $B$, we denote the set of morphisms from $A$ to $B$ (i.e. the set of morphisms with domain $A$ and codomain $B$) by $\cat{C}(A,B)$.
This set is also called the hom-set of $A$ and $B$.

A functor is a map between two categories that preserves morphism composition.

A functor $F \colon \cat{C} \to \cat{D}$ consists of

* a map on objects $A \in Ob(\cat{C}) \mapsto FA \in Ob(\cat{D})$ and

* a map on morphisms $(f \colon  A \to B )\mapsto (Ff \colon  FA \to FB)$,

such that for any objects $A$, $B$, and $C$ and any morphisms $f \colon A\to B$, $g \colon B\to C$:

* the identity morphism $\id_A$ is mapped to $F\id_A=\id_{FA}$ and

* the composition $g\circ f$ is mapped to $F(g\circ f)=Fg\circ Ff$.

A subcategory $\cat{D}$ of a category $\cat{C}$ consists of a subcollection of objects and a subcollection of morphisms such that $\cat{D}$ is itself a category.

§.§ Categories With Copying and Discarding

The definition of a gs-monoidal category is described in <ref>, for more details we recommend <cit.>.

A functor $F \colon \cat{C} \to \cat{D}$ between two monoidal categories $\cat{C}$ and $\cat{D}$ is called lax monoidal if there exists a morphism

\begin{equation}
\psi_0 \colon I_\cat{D} \to F(I_\cat{C})
\end{equation}

and a natural transformation

\begin{equation}
\psi_{A,B} \colon F(A) \otimes F(B) \to F(A \otimes B)
\end{equation}

such that the following diagrams commute:

* For all objects $A, B, C \in \cat{C}$

\begin{equation}
\begin{tikzcd}
(F(A)\otimes F(B)) \otimes F(C) \arrow[rr, "{\alpha_{F(A),F(B),F(C)}}"] \arrow[d, "{\psi_{A,B}\otimes \id_{F(C)}}"'] &  & F(A)\otimes (F(B) \otimes F(C)) \arrow[d, "{\id_{F(A)}\otimes \psi_{B,C}}"] \\
F(A\otimes B)\otimes F(C) \arrow[d, "{\psi_{A\otimes B, C}}"']                                                       &  & F(A)\otimes F(B\otimes C) \arrow[d, "{\psi_{A,B\otimes C}}"]                \\
F((A\otimes B)\otimes C) \arrow[rr, "{F(\alpha_{A,B,C})}"']                                                           &  & F(A\otimes (B\otimes C))
\end{tikzcd}
\end{equation}

where $\alpha$ are the associators on $\cat{C}$ and $\cat{D}$.

* For all objects $A \in \cat{C}$

\begin{equation}
%	I_\cat{D}\otimes F(X) \arrow[r, "\psi_0\otimes \id_{F(X)}"] \arrow[d, "\ell_{F(X)}"'] & F(I_\cat{C})\otimes F(X) \arrow[d, "{\psi_{I_\cat{C},X}}"] \\
%	F(X)                                                                                & F(I_\cat{C}\otimes X) \arrow[l, "F(\ell_X)"]
%	\end{tikzcd}
\begin{tikzcd}
I_\cat{D}\otimes F(A) \arrow[r, "\psi_0\otimes \id_{F(A)}"] \arrow[d, "\ell_{F(A)}"'] & F(I_\cat{C})\otimes F(A) \arrow[d, "{\psi_{I_\cat{C},A}}"] \arrow[rr, "\mathrm{and}", phantom, shift right=9] &  & F(A)\otimes I_\cat{D} \arrow[d, "r_{F(A)}"] \arrow[r, "\id_{F(A)}\otimes \psi_0"] & F(A) \otimes F(I_\cat{C}) \arrow[d, "{\psi_{A, I_\cat{C}}}"] \\
F(A)                                                                                & F(I_\cat{C}\otimes A) \arrow[l, "F(\ell_A)"]                                                                  &  & F(A)                                                                            & F(A\otimes I_\cat{A}) \arrow[l, "F(r_A)"]
\end{tikzcd}
\end{equation}

where $\ell$ and $r$ are the left and right unitors on $\cat{C}$ and $\cat{D}$.

If $\cat{C}$ and $\cat{D}$ are symmetric monoidal categories, then a lax monoidal functor $F$ is called lax symmetric monoidal if the following diagrams commute for any objects $A,B$ of $\cat{C}$:

\begin{equation}
\begin{tikzcd}
F(A)\otimes F(B) \arrow[d, "{\psi_{A,B}}"'] \arrow[r, "{\beta_{F(A), F(B)}}"] & F(B)\otimes F(A) \arrow[d, "{\psi_{B,A}}"] \\
F(A\otimes B)  \arrow[r, "{F(\beta_{A,B})}"']                                 & F(B\otimes A)
\end{tikzcd}
\end{equation}

where $\beta$ is the braiding map on $\cat{C}$ and $\cat{D}$.

A lax symmetric monoidal functor $F \colon \cat{C} \to \cat{D}$ between two gs-monoidal categories $\cat{C}$ and $\cat{D}$ is called lax gs-monoidal if the following diagrams commute for any object $A$ of $\cat{C}$:

\begin{equation}
\begin{tikzcd}
F(A) \arrow[rd, "\cop_{F(A)}"'] \arrow[rr, "F(\cop_A)"] &                                              & F(A\otimes A) &  & F(A) \arrow[rr, "F(\discard_A)"] \arrow[rd, "\discard_{F(A)}"'] &                         & F(I_\cat{C}) \\
& F(A)\otimes F(A) \arrow[ru, "{\psi_{A,A}}"'] &               &  &                                                                 & I_\cat{D} \arrow[ru, "\psi_0"'] &
\end{tikzcd}
\end{equation}

where $I_\cat{C}, I_\cat{D}$ are the monoidal units on $\cat{C}$ and $\cat{D}$, respectively and where $\psi_{A,A}, \psi_0$ are the lax monoidal structure morphisms.

Let $F \colon \cat{C} \to \cat{D}$ be a lax gs-monoidal functor.
Then for every morphism $g$ in $\cat{C}$ we have

\begin{equation}\label{eq:sha_dom}
F \bigl( \dom(g) \bigr) = \dom \bigl( F(g) \bigr)
\end{equation}

Here, given $f \colon A \to X$, domain of $f$ (<ref>) is the morphism $\dom(f) \colon A \to A$ given by

\begin{equation}
\tikzfig{domain}
\end{equation}

We denote with an overline objects and morphisms in the image of $F$, e.g. $\overline{A}\coloneqq F(A)$.
Using the definition of domain in gs-monoidal categories, we can write the left hand side as the top path in the following commutative diagram:

\begin{equation}
% https://q.uiver.app/?q=WzAsOCxbMCwwLCJcXG92ZXJsaW5le0F9Il0sWzIsMCwiXFxvdmVybGluZXtBIFxcb3RpbWVzIEF9Il0sWzQsMCwiXFxvdmVybGluZXtBIFxcb3RpbWVzIEJ9Il0sWzYsMiwiXFxvdmVybGluZXtBIFxcb3RpbWVzIEl9Il0sWzAsMiwiXFxvdmVybGluZXtBfSBcXG90aW1lcyBcXG92ZXJsaW5le0F9Il0sWzIsMiwiXFxvdmVybGluZXtBfSBcXG90aW1lcyBcXG92ZXJsaW5le0J9Il0sWzQsMiwiXFxvdmVybGluZXtBfSBcXG90aW1lcyBcXG92ZXJsaW5le0l9Il0sWzQsNCwiXFxvdmVybGluZXtBfSBcXG90aW1lcyBJIl0sWzAsMSwiXFxvdmVybGluZXtcXGNvcF9BfSJdLFsxLDIsIlxcb3ZlcmxpbmV7QSBcXG90aW1lcyBnfSJdLFsyLDMsIlxcb3ZlcmxpbmV7QSBcXG90aW1lcyBcXGRpc2NhcmRfQn0iXSxbMCw0LCJcXGNvcF97XFxvdmVybGluZXtBfX0iLDJdLFs0LDEsIlxccHNpX3tBLEF9IiwyXSxbNCw1LCJcXG92ZXJsaW5le0F9IFxcb3RpbWVzIFxcb3ZlcmxpbmV7Z30iLDJdLFs1LDIsIlxccHNpX3tBLEJ9IiwyXSxbNSw2LCJcXG92ZXJsaW5le0F9IFxcb3RpbWVzIFxcb3ZlcmxpbmV7XFxkaXNjYXJkX0J9IiwyXSxbNiwzLCJcXHBzaV97QSxJfSIsMl0sWzUsNywiXFxvdmVybGluZXtBfSBcXG90aW1lcyBcXGRpc2NhcmRfe1xcb3ZlcmxpbmV7Qn19IiwyXSxbNywzLCJcXGNvbmciLDJdXQ==
\begin{tikzcd}
{\overline{A}} && {\overline{A \otimes A}} && {\overline{A \otimes B}} \\
\\
{\overline{A} \otimes \overline{A}} && {\overline{A} \otimes \overline{B}} && {\overline{A} \otimes \overline{I}} && {\overline{A \otimes I}} \\
\\
&&&& {\overline{A} \otimes I}
\arrow["{\overline{\cop_A}}", from=1-1, to=1-3]
\arrow["{\overline{A \otimes g}}", from=1-3, to=1-5]
\arrow["{\overline{A \otimes \discard_B}}", from=1-5, to=3-7]
\arrow["{\cop_{\overline{A}}}"', from=1-1, to=3-1]
\arrow["{\psi_{A,A}}"', from=3-1, to=1-3]
\arrow["{\overline{A} \otimes \overline{g}}"', from=3-1, to=3-3]
\arrow["{\psi_{A,B}}"', from=3-3, to=1-5]
\arrow["{\overline{A} \otimes \overline{\discard_B}}"', from=3-3, to=3-5]
\arrow["{\psi_{A,I}}"', from=3-5, to=3-7]
\arrow["{\overline{A} \otimes \discard_{\overline{B}}}"', from=3-3, to=5-5]
\arrow["\cong"', from=5-5, to=3-7]
\end{tikzcd}
\end{equation}

The inner cells commute by the assumed coherences and we can read off the bottom path as the right hand side of <ref>.

§ SUPPLEMENTARY MATERIAL ON GS-MONOIDAL CATEGORIES

Let $f \colon A \to X$ be a normalized morphism in a gs-monoidal category.
Then its domain $\dom(f) \colon A \to A$ is a functional morphism.

We can show this directly from the definition of functional morphisms:

\begin{equation}\label{eq:dom_fun}
\tikzfig{dom_fun}
\end{equation}

The first equation holds because $f$ is normalized and the second used just the associativity of copying.

The following definitions are needed only needed for the construction of the pointed shadow functor in <ref>.
We start with notions of causality and supports, which have been defined elsewhere for Markov categories (i.e. gs-monoidal categories in which all morphisms are total).

A gs-monoidal category $\cat{C}$ is causal if whenever ${f \colon A \to W}$, $g \colon W \to X$ and $h_1, h_2 \colon X \to Y$ satisfy

\begin{equation}\label{eq:causal1}
\tikzfig{causal1}
\end{equation}

then the stronger equation

\begin{equation}\label{eq:causal2}
\tikzfig{causal2}
\end{equation}

also holds.

Let $f \colon A \to X$ and $g \colon Z \to X$ be morphisms in a gs-monoidal category.
We say that $\bm{f}$ is absolutely continuous with respect to $\bm{g}$, denoted $f \ll g$, if the implication

\begin{equation}\label{eq:abs_cont}
\tikzfig{abs_cont}
\end{equation}

holds for arbitrary objects $Y$, $W$ and any two parallel morphisms $h, h' \colon W \otimes X \to Y$.

Let $\cC$ be a gs-monoidal category.
A support for $f \colon A \to X$ is given by an object $\Supp{}$ and a deterministic morphism $\suppinc{} \colon \Supp{} \to X$, such that we have

\begin{equation}\label{eq:supp_asfaithful}
\tikzfig{supp_factor_1}
\end{equation}

for all $h, h' \colon W \otimes X \to Y$ with arbitrary $W$ and $Y$.

We say that $\cC$ has point liftings if for all $f \colon A \to X$ and all $x \in \cC_\det (I,X)$ satisfying $x \ll f$, there exists an $a \in \cC_\det (I,A)$ satisfying $x \ll f \circ a$.

Let $\cC$ be a causal gs-monoidal category with supports and point liftings.
Then we have a functor $\Upsilon \colon \cC \to \cat{Rel}$ defined on objects as

\begin{align}\label{eq:point_sha_obj}
\Upsilon(A) \coloneqq \cC_\det (I,A)
\end{align}

and on morphisms as $f \mapsto \Upsilon(f)$ where $\Upsilon(f)$ is a relation in $\cat{Rel}(\Upsilon(A), \Upsilon(X))$ defined via

\begin{equation}\label{eq:point_sha_morph}
\Upsilon(f) \, (a) \coloneqq \Set*[\big]{ x \in \cC_\det(I,X)  \given  x \ll f \circ a }.
\end{equation}

Furthermore, $\Upsilon$ is a strong gs-monoidal functor with respect to the monoidal structure of $\cat{Rel}$ as in <ref>.
A strong gs-monoidal functor $\cC \to \cat{Rel}$ is similar to a lax gs-monoidal functor (<ref>), but moreover the structure morphisms $\psi_0$ and $\psi_{A,B}$ are isomorphisms.
See <cit.> for more details on gs-monoidal functors.

While the theorem has been proven in <cit.> for the case of Markov categories, it works just as well for gs-monoidal categories.
We discuss $\Upsilon$ further in the next section under the name of pointed shadow functor.

§ POINTED SHADOW FUNCTOR

We think of the shadow functor, which is needed to specify a behavior structure from <ref>, as a concrete relational model of the ambient category.
At first sight, it is unclear how strong is the assumption that such a shadow functor exists.
Here, we show how to construct a specific shadow functor, called the pointed shadow functor purely in terms of the data provided by the ambient category itself, as long as it satisfies a few additional properties.
One should keep in mind that a given ambient category may have multiple plausible shadow functors.
A pointed shadow functor, however, is the one we use most often because it is consistent with interpreting objects in the ambient category as particular sets of “points”, e.g. like $T$ in $\cat{Tur}$ is the set of Turing machines.

This interpretation, thinking of the objects $T$ and $C$ as sets of targets and contexts respectively, also allows us to express the universality of a simulator $s$ in terms of equality of behaviors (of $s$ and the trivial simulator) for every target $t \in T$ and every context $c \in C$ as in relation (<ref>) from sec:motivation.

The pointed shadow functor takes an abstract process $f$ to a relation $\behim{f}$.
When applied to a deterministic point $a$, this relation returns the set $\behim{f}(a)$ of all deterministic points $x$ that are within the support of $f(a)$ in the ambient category.

Construction of pointed shadows
Consider an ambient category $\cC$ that is causal, has supports and point liftings (a detailed presentation of these properties can be found in <ref>).
This means, in particular, that for every morphism $f \colon A \to X$ we can refer to a deterministic subobject $\suppinc{f} \colon \Supp{f} \to X$ which is both necessary and sufficient for equality of processes in the future of $f$, i.e. we have equivalence (<ref>).
In $\cat{Rel}$, the support object $\Supp{f}$ is the union of all the images of points in $A$ under relation $f$:

\begin{equation}
\Supp{f} = \Set*[\big]{ x \in X  \given  \exists \, a \in A \text{ such that } x \in f(a) }
\end{equation}

This set is canonically embedded within $X$ as a subset thereof.
We can use supports in a general ambient category $\cC$ to give a canonical description of its morphisms as relations, and this allows us to define the pointed shadow functor $\Upsilon$.

For any object $A$ of $\cC$, let the set $\behim{A}$ consist of the deterministic states of $A$, i.e. it is the hom-set $\cC_\det(I,A)$.
Furthermore, for any morphism $f \in \cC(A,X)$, the relation $\behim{f} \in \cat{Rel}(\behim{A},\behim{X})$ is given by supports as subsets of $\behim{X}$:
While <ref> superficially differs from <ref> used to define $\Upsilon(f)$ in the statement of <ref>, they are in fact equivalent under the assumptions of the theorem <cit.>.

\begin{equation}\label{eq:point_sha_morph_2}
\behim{f}(a) \coloneqq \cC_\det \left( I, \Supp{f(a)} \right) .
\end{equation}

One can view $\behim{f}(a)$ as a subset of $\behim{X}$ by composing its elements with the associated support inclusion ${\suppinc{f(a)} \colon \Supp{f(a)} \to X}$.
The mapping

\begin{align}
\Upsilon(A) &\coloneqq \behim{A}  &  \Upsilon(f) &\coloneqq \behim{f}
\end{align}

then gives a functor $\Upsilon \colon \cC \to \cat{Rel}$, which we term the pointed shadow functor (<ref>).
Moreover, $\Upsilon$ can be provided with a strong gs-monoidal structure (<ref>), so that it can be used to define a behavior structure on the ambient category (<ref>).

There are two main sources of examples of pointed shadow functors in this article.
One of them is provided by forgetful functors as in the case of spin systems.
The other is given by inclusion functors for those subcategories of $\cat{Rel}$, which are valid target–context categories in their own right.

Let $\cC$ be a (normalized) gs-monoidal category that has strong supports and is a subcategory $\iota \colon \cC \hookrightarrow \cat{Rel}$ of the category of relations.
Assume that for all objects $X$ and morphisms $f$ of $\cC$ we have

\begin{align}
\label{eq:incl_det_states} \cC_\det(I,X) &= \cat{Rel}_\det \bigl( I,\iota(X) \bigr),  \\
\label{eq:incl_supp} \iota \left( \Supp{f} \right) &= \Supp{\iota(f)}.
\end{align}

Then the inclusion functor $\iota \colon \cC \hookrightarrow \cat{Rel}$ coincides with the pointed shadow functor $\Upsilon$.

This is an immediate consequence of the definition of the pointed shadow functor.

[Pointed shadow for functions]
For the category $\cat{Set}$ of sets and functions, the inclusion ${\iota \colon \cat{Set} \hookrightarrow \cat{Rel}}$ is its pointed shadow.
Indeed, all morphisms in $\cat{Set}$ are deterministic, and deterministic morphisms of $\cat{Rel}$ are precisely functions, so that we have

\begin{equation}
\cat{Set}_\det = \cat{Set} = \cat{Rel}_\det,
\end{equation}

which implies <ref>.
Furthermore, the support of a function (both in $\cat{Set}$ as well as in $\cat{Rel}$) is its image:

\begin{equation}
\Supp{f} = \im(f) = \Supp{\iota(f)}
\end{equation}

so that <ref> follows.

Ambient imitation relation for intrinsic behaviors and pointed shadow
Given a target–context category with intrinsic behaviors whose shadow functor is the pointed shadow functor, we can think of the behavioral relation as a relation on the hom-set $\cC_\det(I,B)$, which in this case coincides with $\behim{B}$.
The resulting ambient imitation relation $f \mrelop g$ then holds ifand only if for all $a \in \behim{A} \coloneqq \cC_\det(I,A)$, we have that

* for every deterministic state $v \in \cC_\det(I,B)$ within the support of the composite

\begin{equation}\label{eq:behavior_of_g}
\begin{tikzcd}
I & A & {T \otimes C} & B
\arrow["a", from=1-1, to=1-2]
\arrow["g", from=1-2, to=1-3]
\arrow["\eval", from=1-3, to=1-4]
\end{tikzcd}
\end{equation}

there exists a deterministic state $u_v \in \cC_\det(I,B)$ within the support of

\begin{equation}\label{eq:behavior_of_f}
% https://q.uiver.app/?q=WzAsNCxbMCwwLCJJIl0sWzEsMCwiQSJdLFsyLDAsIlQgXFxvdGltZXMgQyJdLFszLDAsIkIiXSxbMCwxLCJhIl0sWzEsMiwiZiJdLFsyLDMsIlxcZXZhbCJdXQ==
\begin{tikzcd}
I & A & {T \otimes C} & B
\arrow["a", from=1-1, to=1-2]
\arrow["f", from=1-2, to=1-3]
\arrow["\eval", from=1-3, to=1-4]
\end{tikzcd}
\end{equation}

satisfying $u_v \brelop v$; and conversely

* for every $u \in \cC_\det(I,B)$ within the support of the state from (<ref>), either

* there exists a $v_u \in \cC_\det(I,B)$ within the support of the state from (<ref>), such that $u \brelop v_u$ holds, or

* there are no deterministic states in the support of the state from (<ref>).

These two conditions of course come from the enhancement and degradation requirements respectively, as expressed in <ref>.

§ INTRINSIFICATION

In this section, starting from an arbitrary target–context category with behaviors, $\cC$, we construct a target–context category with intrinsic behaviors, $\cC_{\intr}$, which is defined in terms of the same ambient category, same $T$ and $C$, and the same shadow functor.
We call $\cC_{\intr}$ the intrinsification of $\bm{\cC}$.
The construction of $\cC_{\intr}$ is such that whenever $f$ behaviourally subsumes $g$ within $\cC_{\intr}$ then $f$ also behaviourally subsumes $g$ within $\cC$.
In particular, universality in $\cC_{\intr}$ implies universality .

Let $(\cC,T,C,\Beh,\behim{B},\behim{\eval},\brel)$ be a target–context category with behaviors, then there is a target–context category with intrinsic behaviors $(\cC,T,C,\Beh,B_{\intr},\eval_{\intr},\brel')$ such that for any $f,g \colon A \to T \otimes C$, we have

\begin{equation}\label{eq:intrinsification_weakening}
f \mrelop' g \implies f \mrelop g,
\end{equation}

where $\mrel$ and $\mrel'$ are the associated ambient imitation relations (<ref>).

Note that implication (<ref>) equivalently means that the identity is a target–context functor from $\cC_{\intr}$ to $\cC$.

We define

\begin{align}
B_{\intr} &\coloneqq T \otimes C,  & \eval_{\intr} &\coloneqq \id_{T \otimes C},
\end{align}

and for $b_1, b_2 \in \behim{B_{\intr}}$ also

\begin{equation}\label{eq:newrel}
b_1 \brelop' b_2 \quad \coloniff \quad \behim{\eval} \circ b_1 \imrelop \behim{\eval} \circ b_2,
\end{equation}

where by abuse of notion we denote by $b_1$ and $b_2$ both the elements of $\behim{B_{\intr}}$ as well as the corresponding deterministic states.

Let us now prove that $f \mrelop' g$ implies $f \mrelop g$.
First, we show that if $\behim{\eval}\circ \behim{g}(a)$ is defined for an $a \in \behim{A}$ (which implies that $\behim{g}(a)$ is defined), then so is $\behim{\eval} \circ \behim{f}(a)$.
When we say that a relation of type $I \to X$ is defined, we mean that it is non-empty as a subset of $I \times X \cong X$, or in other words that it is total as a morphism in $\cat{Rel}$.
The assumption $f \mrelop' g$ is equivalent to $\behim{f} \imrelop' \behim{g}$ since $\eval_{\intr}$ is just the identity on $T \otimes C$.
Hence, by <ref> of the imitation relation $\imrelop'$, $\behim{f}(a)$ is defined whenever $\behim{g}(a)$ is, and there exists a $\brel'$-enhancement

\begin{equation}\label{eq:old enh type}
\mathrm{enh}_a \colon \behim{g}(a) \to \behim{f}(a).
\end{equation}

This means that for any $y \in \behim{g}(a)$ we have $\mathrm{enh}_a(y) \brelop' y$, which is equivalent to

\begin{equation}\label{eq:enhy}
\behim{\eval} \circ \mathrm{enh}_a(y) \imrelop \behim{\eval} (y)
\end{equation}

by the definition of $\brelop'$ in (<ref>).
Since $\behim{\eval}\circ \behim{g}(a)$ is defined by assumption, there exists at least one $y \in \behim{g}(a)$ such that $\behim{\eval}(y)$ is defined.
But then, by relation (<ref>), $\behim{\eval} \circ \mathrm{enh}_a(y)$ is also defined.
Since $\mathrm{enh}_a(y)$ is an element of $\behim{f}(a)$, this in particular implies that that $\behim{\eval}\circ \behim{f}(a)$ is defined.

Next, we prove that $f \mrelop g$ holds.
We consider an arbitrary $a \in \behim{A}$ such that $\behim{\eval} \circ \behim{g}(a)$ is defined.
Then, the task is to construct a $\brel$-enhancement

\begin{equation}
\mathrm{Enh}_a \colon \behim{\eval}\circ \behim{g}(a) \to \behim{\eval}\circ \behim{f}(a)
\end{equation}

as well as a $\brel$-degradation

\begin{equation}
\mathrm{Deg}_a \colon \behim{\eval}\circ \behim{f}(a) \to \behim{\eval}\circ \behim{g}(a).
\end{equation}

We only show the construction of $\mathrm{Enh}_a$ explicitly; the one of $\mathrm{Deg}_a$ is analogous.

By assumption, we have $f \mrelop' g$ and as before this implies that there exists a $\brel'$-enhancement as in (<ref>).
That is, relation (<ref>) holds for every $y \in \behim{g}(a)$, which implies that there exists a $\brel$-enhancement

\begin{equation}\label{eq:double enh}
\mathrm{enh}_{a,y} \colon \behim{\eval}(y) \to \behim{\eval} \circ \mathrm{enh}_a(y).
\end{equation}

Let $b$ be an arbitrary element of the domain $\behim{\eval}\circ \behim{g}(a)$ of the desired enhancement $\mathrm{Enh}_a$.
We can choose a $y \in \behim{g}(a)$ such that $b$ is within its image under $\behim{\eval}$.
Using it, we then define

\begin{equation}
\mathrm{Enh}_a(b) \coloneqq \mathrm{enh}_{a,y}(b).
\end{equation}

This indeed defines a $\brel$-enhancement of correct type.

§ POLYNOMIALLY BOUNDED RELATIONS

In this section, we construct the ambient category $\cat{Rel}_{\mathrm{poly}}$ used in <ref> to describe universality of spin models.
An objects of $\cat{Rel}_{\mathrm{poly}}$ is a set $S$ equipped with a size function $\abs{\ph}_S \colon S \to \R_{\geq 0}$.
A generic morphism $f \colon S \to R$ is given by a relation $f \in \cat{Rel}( S, R)$ that is polynomially bounded, i.e. such that there exists a non-decreasing polynomial $\mathfrak{p}_f\in \R_{\geq 0}[x]$ satisfying

\begin{equation}\label{eq:poly constr}
r \in f(s) \quad \implies \quad \abs{r}_R \leq \mathfrak{p}_f(\abs{s}_S)
\end{equation}

for all $r\in R$ and all $s\in S$.
It is straightforward to check that this condition is preserved by the composition of relations.
Moreover, choosing $\mathfrak{p}_{\id}$ to be the identity function shows that $\cat{Rel}_{\mathrm{poly}}$ contains all identities and is thus a category.

Next we equip $\cat{Rel}_{\mathrm{poly}}$ with the relevant structure to turn it into a gs-monoidal category.
This structure is inherited from $\cat{Rel}$ as in <ref>, we just need to show that all relevant morphisms involved in the construction satisfy implication <ref>.
Specifically, we define the tensor product of objects to be

\begin{equation}
\left( S, \abs{\ph}_S \right) \otimes \left(R, \abs{\ph}_R \right) \coloneqq \left(S \times R, \abs{\ph}_{S\otimes R} \right),
\end{equation}

where $\times$ is the cartesian product of sets and the size function is

\begin{equation}
\abs{\ph}_{S \otimes R}(s,r) \coloneqq \max \left\{ \abs{s}_S, \abs{r}_R \right\} .
\end{equation}

The tensor product of morphisms $f \colon S \to M$ and $ g \colon R \to N$ is defined by

\begin{equation}
(m,n) \in (f \otimes g)(s,r) \quad \iff \quad  m \in f(s)  \text{ and } n \in g(r).
\end{equation}

Note that this defines a morphism in $\cat{Rel}_{\mathrm{poly}}$, since we can derive

\begin{equation}
\abs{(m,n)}_{M \otimes N} \leq (\mathfrak{p}_f + \mathfrak{p}_g) \left( \abs{(s,r)}_{S \otimes R} \right)
\end{equation}

via the definition of $\abs{\ph}_{S \otimes R}$ and the fact that $\mathfrak{p}_f$ and $\mathfrak{p}_g$ are non-decreasing.
The unit of $\otimes$ is given by $I \coloneqq \{\sngltn \}$ with $\abs{\sngltn}_I = 0$.
Finally, we define $\cop_S(s)=(s,s)$ and $\discard_S(s)=\{\sngltn\}$ as in $\cat{Rel}$.
It is straightforward to see that these morphisms satisfy implication (<ref>).
Moreover, $\cat{Rel}_{\mathrm{poly}}$ is normalized for the very same reason as $\cat{Rel}$.

§ MONOIDAL COMPUTERS

A related framework to the one we present here is that of monoidal computers <cit.>, which provides a categorical model of computation and in this sense also shares many motivations with our approach.
Here, we discuss this relation more precisely.
In particular, we show what additional data, on top of a target–context category with intrinsic behaviors, is sufficient to obtain a monoidal computer.

The ambient category $\cC$ in works on monoidal computers is assumed to be gs-monoidal, just like in our case.
A monoidal computer, as characterized by <cit.>, consists of

* a fixed object $\prog$,

* a morphism $\{\} \colon \prog \otimes W \to B$ called program evaluator for all objects $W$ and $B$, and

* a deterministic morphism $[] \colon \prog \otimes X \to \prog$ called partial evaluator for all objects $X$,

which satisfy compatibility conditions

\begin{equation}\label{eq:pavlovic_compatibility}
\tikzfig{pavlovic_compatibility}
\end{equation}

and the following `surjectivity' conditions:

\begin{equation}\label{eq:pavlovic_universality}
\tikzfig{pavlovic_universality}
\end{equation}

where the search for $r_f \colon A \to \prog$ is restricted to the deterministic subcategory $\cC_\det$ of $\cC$.
Equations (<ref>) are the programmability conditions that justify calling the program evaluator $\{\}$ a universal evaluator.

This notion does not exactly coincide with the concept of universality introduced in <ref>.
Instead, it corresponds to reachability in the sense of <ref>, since conditions (<ref>) and (<ref>) are demanding that $\{\} \colon \prog \otimes W \to B$ is an $A$-complete parametrization of maps $W \to B$ (<ref>)

Properties (<ref>) and (<ref>) allow one to express any morphism $f \colon A \otimes W \to B$ as an application of the universal evaluator to some program $r_f(a)$ in $\prog$ and to reduce computations with $n$ inputs to computations with $n-1$ inputs via the partial evaluator.
While there is no explicit partial evaluator in our approach, we can compare a universal evaluator with the evaluation of a given simulator $s$ in the form of $\eval \circ s \in \cC(\prog \otimes C,  B)$.
We formalize this observation in <ref> below.

One of the consequences of the definition of monoidal computers is that every object $A \in \cC$ has an associated idempotent $p_A$

\begin{equation}\label{eq:objects_from_idempotents}
\tikzfig{objects_from_idempotents}
\end{equation}

that splits through $A$ and moreover $\sigma_A$ is deterministic.

Consider a target–context category with intrinsic behaviors $(\cC,T,C,\eval,\brel)$ such that $C$ is identical to $B$ and denoted by $\prog$.
For every $A \in \cC$, assume that

* the ambient relation $\mrel$ on $\cC(A,T \otimes \prog)$ is trivial, i.e. it coincides with equality,

* $\eval \colon T \otimes \prog \to \prog$ is an $A$-complete parametrization of maps $\prog \to \prog$, and

* there is a split idempotent $p_A \colon \prog \to \prog$ as in <ref>.

If there is a universal simulator $s$ of type $\prog \otimes \prog \to T \otimes \prog$, then $\cC$ is a monoidal computer.

We need to construct program evaluators that satisfy conditions (<ref>).
We define the basic one of type $\prog \otimes \prog \to \prog$ from the universal simulator and the evaluation morphism.
Other program evaluators can be obtained from this one by split idempotents.

That is, we define

\begin{equation}\label{eq:program_evaluator_1}
\tikzfig{program_evaluator_1}
\end{equation}

By <ref>, this program evaluator is an $A$-complete parametrization of maps $\prog \to \prog$ for any $A$, so that it satisfies conditions (<ref>).
We define other partial evaluators as

\begin{equation}\label{eq:program_evaluator_2}
\tikzfig{program_evaluator_2}
\end{equation}

For any $f \colon A \otimes W \to B$, define

\begin{equation}\label{eq:program_evaluator_test}
\tikzfig{program_evaluator_test}
\end{equation}

Then the deterministic morphism $r_f \colon A \to \prog$ for which we have <ref> is given by $r_{\tilde f}$, which exists by the fact that the program evaluator defined by <ref> is an $A$-complete parametrization of maps $\prog \to \prog$.

Partial evaluators can also be constructed from the data provided by the assumptions of <ref>, as one can use the reachability of program evaluators to define them so that the compatibility conditions are satisfied.
This is essentially because in condition (<ref>), we can choose $f$ to be $\{  \} \colon (\prog \otimes A) \otimes W \to B$ and the partial evaluator $[] \colon \prog \otimes A \to \prog$ is then the corresponding morphism $r_{\{\}}$ coming from <ref>.

While <ref> is technically correct, it is not clear whether its direct application is of particular interest.
In particular, note that one of its assumptions, that the ambient relation $\mrel$ is equality, can only be satisfied if all morphisms in $\cC$ are total, i.e. if it is a Markov category.
Additionally, the assumption of intrinsic behaviors is not satisfied for the target–context category $\cat{Tur}$ in which singleton universal simulators coincide with universal Turing machines.

Nevertheless, we believe that the result is of interest as it can inspire strategies to build monoidal computers even in case its assumptions are not in fact satisfied.
Let us illustrate this with $\cat{Tur}$ from <ref>.
There contexts $C$ are given by strings in $\Sigma^\star$, but behaviors do not.
Instead, $\behim{B}$ is the set $\Sigma^\star \times \pwrset(\Sigma^\star)$.
Let us identify $\prog$ as the set of finite strings, so that $\prog = C$ holds.
Then, instead of <ref>, we use

\begin{equation}\label{eq:program_evaluator_3}
\tikzfig{program_evaluator_3}
\end{equation}

to define the program evaluator, where $\eval^\intr$ is the evaluation morphism in the target–context category $\cat{Tur}^\intr$ (see <ref>), which can be expressed as

\begin{equation}
\tikzfig{eval_intr}
\end{equation}

in terms of the evaluation function $\behim{\eval}$ in $\cat{Tur}$.