not liftable

draft/draft.tex

@@ -292,6 +292,7 @@
 \newcommand{\spto}{\mathrel{\tikz{\draw[-{Stealth}] (0.0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
 \newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0.04,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);\draw (0.04,0) -- (0,-0.07);\draw (0.04,0) -- (0,0.07);}}}
 \newcommand{\powf}{\mathcal{P}}
+\newcommand{\powfi}{\mathcal{P}_{\mathsf{inj}}}
 \newcommand{\sappr}{\sqsupseteq}
 \newcommand{\Dom}{\mathsf{Dom}}
 
@@ -433,7 +434,7 @@ We want to say that a natural order structure entails an order over a functor de
 \begin{proof}
 	Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf FZ)$, $k\in\Hom(1,\powf FY)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf Fg(k)$, we define $k'\in\powf FY$ that that $k'=\{y\mid Fg(y)\in h\}$. We show that $k'\subseteq k$ and $\powf Fg(k')=h$.
 	
-	Assuming $y\in k'$ we have $Fg(y)\in h$. Since $h\subseteq \powf Fg(k)$ we have $Fg(y)\in\powf Fh(h)$, so we have $y\in k$ that means $k'\subseteq k$.
+	Assuming $y\in k'$ we have $Fg(y)\in h$. Since $h\subseteq \powf Fg(k)$ we have $Fg(y)\in\powf Fg(k)$, so we have $y\in k$ that means $k'\subseteq k$.
 	
 	Assuming $z\in\powf Fg(k')$, then there exists $y'\in k'$ that $z=Fg(y')$, so $z\in h$ and $\powf Fg(k')\subseteq h$.
 	
@@ -2163,7 +2164,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 %\end{proof}
 \begin{example}
 And another counter-example!!! 
-Assuming that $F$ is the powerset endofunctor over the category of sets and injective maps. Then for every $X$, we define the order on $FX$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder.\\
+Assuming that the functor is the powerset endofunctor over the category of sets and injective maps. We show the functor with $\powfi$. For every $X$, we define the order on $\powfi X$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder. Then we define the order over every $\Hom(X,\powfi Y)$ pointwise. We have chosen the category of sets with injective maps because we could not define a functor from $\Set$ to $\preord$ with the mentioned ordering.\\
 We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
 \begin{gather*}
 	\alpha(x)=
@@ -2186,7 +2187,10 @@ $\sigma$ is defined as below:
 $R$ is symmetric, and $\sigma$ is a witness for $R$ to be an AM-simulation, but $R$ is not a bisimulation in the traditional sense because $(2,1)\in R$, and $2\to 3$, but $(3,1)$ or $(3,2)$ are not in $R$. It is easy to see that it is not an AM-bisimulation as well because we can not define a function that can serve as an evidence for it as $3$ does not appear in any pair in $R$, while it exists in $\alpha(2)$.
 
 This counter-example also works as a counter-example for Hughes-Jacobs definition of simulation. Actually, $\appr;(FR)^\dagger;\appr=\powf X\times \powf X$, so $R\subseteq \appr;(FR)^\dagger;\appr$ that means that $R$ is a simulation. Worth noting that they claim that their setting works for an arbitrary category. So, unlike their definition, in the context of the relator-based definitions that only work in $\Set$, this counter-example does not live.
+
+The mentioned ordering is not liftable. Assuming $h\in\Hom(\nats,\powfi \nats)$, $g\c \nats\to \nats$, and $k\in\Hom(\nats,\powfi \nats)$, and they are defined for every $n$ in $\nats$ as $h(n)=\{2\times n\}$, $g(n)=3\times n$, and $k(n)=\{n\}$, then $|h(n)|=|\powfi g(k(n))|=1$ that means $h\appr\powfi g\comp k$ is satisfied, but there is no $k'$ that $h=\powfi g\comp k$ because we can never have $h(1)=\powfi g\comp k'(1)$, as assuming $k'(1)=\{n\}$, and $n$ must be a natural number, then we should have $2=3\times n$ that is impossible.
 \end{example}
+
 \subsection{The concrete proof}
 %\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}
 %	Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have: