From 99d6862e1271988a08f95c34afc8075c913f9942 Mon Sep 17 00:00:00 2001 From: partowp Date: Mon, 3 Aug 2026 20:16:39 +0100 Subject: [PATCH] liftable --- draft/draft.tex | 216 ++++++++++++++++++++++++++++++------------------ 1 file changed, 134 insertions(+), 82 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index de54c94..861be01 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -406,12 +406,12 @@ We want to say that a natural order structure entails an order over a functor de \end{proof} \begin{definition}[Liftable Order Structure]\label{def:liftable-ord} - A \emph{liftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr Fg\comp k$ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$. + A \emph{liftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr Fg\comp k$ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.\ppnote{I added the surjection condition on $g$.} \end{definition} \begin{definition}[Coliftable Order Structure]\label{def:coliftable-ord} - A \emph{coliftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$. + A \emph{coliftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$. \end{definition} \begin{lemma}\label{lem:set-ord-str} @@ -429,6 +429,47 @@ We want to say that a natural order structure entails an order over a functor de The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures. \end{remark} +\begin{lemma}\label{lem:liftable} + Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every surjective $f\in\Hom(X,FY)$ we have: + \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] + \item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$ + \item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$ + \end{enumerate} +\end{lemma} +\begin{proof} + $(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$. + + Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$. + + $(II)$ Basically, by definition of $\op$ and relation composition we have + \begin{gather*} + (Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\ + (\appr\comp Ff)^\op=(Ff)^\op\comp\sappr. + \end{gather*} + So it follows directly from applying $\op$ on both sides of $(I)$.\qed +\end{proof} +\begin{lemma}\label{lem:coliftable} + Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $f\in\Hom(X,FY)$ we have: + \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] + \item $Ff\comp\appr\quad=\quad\appr\comp Ff$ + \item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$ + \end{enumerate} +\end{lemma} +\begin{proof} + $(I)$ Assuming $t\mathrel{(Ff\comp\appr)} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is coliftable, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{(\appr\comp Ff)} x$. + + Assuming $t\mathrel{(\appr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:coliftable-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$. + + $(II)$ Basically, by definition of $\op$ and relation composition we have + \begin{gather*} + (Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\ + (\appr\comp Ff)^\op=(Ff)^\op\comp\sappr. + \end{gather*} + So it follows directly from applying $\op$ on both sides of $(I)$.\qed +\end{proof} + +\subsection{Powerset Functor} +In this section we discuss set inclusion as an ordering over the powerset functor. \begin{prop}\label{prop:lift-gen-func} For a functor $F\c\Set\to\Set$, a functor of the form $\powf F$, where $\powf$ is the powerset functor, the set inclusion is a liftable order structure. \end{prop} @@ -475,56 +516,98 @@ We want to say that a natural order structure entails an order over a functor de We could not prove a general statement like~\autoref{prop:lift-gen-func} for coliftability even if the surgectivity of $g$ remains in the definition. Perhaps more conditions on $F$ in~\autoref{prop:lift-gen-func} are needed. Conditions like preserving surjections and unions that make the statement extremely limited, and meaningless. \end{remark} -\begin{example} - The subdistribution functor $\sub\c\Set\to\Set$ is defined as $\sub X=\{\mu\c X\to[0,1]\mid \sum_{x\in X}\mu(x)\}$ on objects, and for $\sub f\c \sub X\to\sub Y$, we have - \begin{gather*} - \sub f(\mu)=y\mapsto\sum_{x\in f^{\mone}(y)}\mu(x), - \end{gather*} - on morphisms. We define the ordering on $\sub X$ for $\mu_1,\mu_2\in \sub X$ as - \begin{gather*} - \mu_1\appr \mu_2\iff \forall x\in X, \mu_1(x)\leq\mu_2(x). - \end{gather*} - The definition derives the ordering on morphisms of each hom-set $\hom(X,\sub Y)$ as usual in $\Set$.\\ - Assuming $\mu\in\sub X$, $g\c X\to Y$, $\nu\in\sub Y$, and $\nu\appr \sub g(\mu)$, we need to prove that there exists $\mu'\in \sub X$, that $\mu'\appr\mu$ and $\nu=\sub g(\mu')$. -\end{example} - -\begin{lemma}\label{lem:liftable} - Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every $f\in\Hom(X,FY)$ we have: - \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] - \item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$ - \item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$ - \end{enumerate} -\end{lemma} +\subsection{Maybe Functor} +The order structure that we can define for this functor is that for sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$, and for every $x\in\Dom(f)$ we have $f(x)=g(x)$ ($\Dom(f)$ is the domain of a function $f$). +\begin{prop}\label{prop:maybe-lif} + The order structure on the set-functor $FX=X+1$ is a liftable order. +\end{prop} +% By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases: +% \begin{itemize} + % \item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$. + % \item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed + % \end{itemize} \begin{proof} - $(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$. - - Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$. - - $(II)$ Basically, by definition of $\op$ and relation composition we have + Assuming that $h\in\Hom(X,Z+1)$, $g\c Y\to Z$, $k\in\Hom(X,Y+1)$, such that $h\appr (g+1)\comp k$. We define $k'\in\Hom(X,Y+1)$ as follows: \begin{gather*} - (Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\ - (\appr\comp Ff)^\op=(Ff)^\op\comp\sappr. + k'(x)= + \begin{cases} + \bot&x\notin\Dom(h)\\ + k(x)&x\in\Dom(h) + \end{cases} \end{gather*} - So it follows directly from applying $\op$ on both sides of $(I)$.\qed + We have $\Dom((g+1)\comp k')=\Dom(k')$ and $\Dom(k')=\Dom(h)$, so we have $\Dom((g+1)\comp k')=\Dom(h)$. If $x\in\Dom(h)$, then $h(x)=(g+1)\comp k(x)$ and $(g+1)\comp k(x)=(g+1)\comp k'(x)$, so we have $h(x)=(g+1)\comp k'(x)$. So, we have $h=(g+1)\comp k'$. Additionally, $\Dom(k')\subseteq\Dom(k)$, and for every $x\in \Dom(k')$, we have $k'(x)=k(x)$, so we have $k'\appr k$. \qed \end{proof} -\begin{lemma}\label{lem:coliftable} - Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $f\in\Hom(X,FY)$ we have: - \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] - \item $Ff\comp\appr\quad=\quad\appr\comp Ff$ - \item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$ - \end{enumerate} -\end{lemma} +\begin{prop}\label{prop:maybe-colif} + The order structure on the set-functor $FX=X+1$ is a coliftable order. +\end{prop} \begin{proof} - $(I)$ Assuming $t\mathrel{(Ff\comp\appr)} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is coliftable, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{(\appr\comp Ff)} x$. - - Assuming $t\mathrel{(\appr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:coliftable-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$. - - $(II)$ Basically, by definition of $\op$ and relation composition we have + By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $Fg(k)\appr h$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k\appr k'$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases: + \begin{itemize} + \item $Fg(k)=h$: In this case we take $k'=k$, and then we have $Fg(k')=h$. + + \item $Fg(k)=\bot$: It entails that $k=\bot$. We either have $h=\bot$ or $h\in Y$. If $h=\bot$ then we take $k'=k$, and we are done. If $h\in Y$, then by the surjectivity of $g$, there exists $k'$ such that $g(k')=h$ that entails $Fg(k')=h$ as well.\qed + \end{itemize} +\end{proof} + +\subsection{Subdistribution Functor} +The subdistribution functor $\sub\c\Set\to\Set$ is defined as $\sub X=\{\mu\c X\to[0,1]\mid \sum_{x\in X}\mu(x)\}$ on objects, and for $\sub f\c \sub X\to\sub Y$, we have +\begin{gather*} + \sub f(\mu)=y\mapsto\sum_{x\in f^{\mone}(y)}\mu(x), +\end{gather*} +on morphisms. We define the ordering on $\sub X$ for $\mu_1,\mu_2\in \sub X$ as +\begin{gather*} + \mu_1\appr \mu_2\iff \forall x\in X, \mu_1(x)\leq\mu_2(x). +\end{gather*} +The definition derives the ordering on morphisms of each hom-set $\Hom(X,\sub Y)$ as usual in $\Set$. +\begin{prop} + The pointwise ordering on $\sub$ is a liftable ordering. +\end{prop} +\begin{proof} + Assuming that $\mu\in SX$, $g\c X\to Y$ is surjective, $\nu\in SY$, and $\nu\appr \sub g(\mu)$, then there exists $\mu'\in \sub X$ such that $\mu'\appr \mu$ and $\sub g(\mu')=h$.\\ + The assumption $\nu \appr Sg(\mu)$ means that for every $y \in Y$, \begin{gather*} - (Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\ - (\appr\comp Ff)^\op=(Ff)^\op\comp\sappr. + \nu(y) \leq Sg(\mu)(y) = \sum_{x \in g^{\mone}(y)} \mu(x). \end{gather*} - So it follows directly from applying $\op$ on both sides of $(I)$.\qed + We construct $\mu'$ as follows: + \begin{gather*} + \mu'(x)= + \begin{cases} + \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)&Sg(\mu)(g(x))\neq 0\\ + 0&Sg(k)(g(x))= 0 + \end{cases} + \end{gather*} + First, we need to prove that $\mu'$ is a subdistribution. + For every $x \in X$, $\mu'(x) \ge 0$. The total mass of $\mu'$ is + \begin{align*} + \sum_{x \in X} \mu'(x)&\\ + =& \sum_{x \in X} \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)\\ + =& \sum_{y \in Y} \sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)\\ + =& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)\\ + =& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)\\ + =& \sum_{y \in Y} \nu(y)\\ + \leq& 1 + \end{align*} + Thus $\mu'$ is a subdistribution. Now, we prove $Sg(\mu') = \nu$. + For any $y \in Y$, we have: + \begin{align*} + Sg(\mu')(y)&\\ + = &\sum_{x \in g^{\mone}(y)} \mu'(x)\\ + = &\sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)\;\;(Sg(\mu)(y)\neq 0)\\ + = &\frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)\;\;(Sg(\mu)(y)\neq 0)\\ + = &\frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)\;\;(Sg(\mu)(y)\neq 0)\\ + = &\mu(y) + \end{align*} + (If $Sg(\mu)(y) = 0$, then $\nu(y) = 0$, and the sum is $0$ as well, so the equality still holds.) \\ + Now, we are left to prove that $\mu'\appr\mu$. + For every $x\in X$, have the following cases: + \begin{itemize} + \item $Sg(\mu)(g(x))= 0$: We have $\mu'(x)=0$, and obviously $\mu'\appr\mu$. + \item $Sg(\mu)(g(x))\neq 0$: We have $\frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)$, and since $\nu\appr Sg(\mu)$ then we have: + \begin{align*} + &\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\leq 1\\ + \Rightarrow&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\comp \mu(x)\leq \mu(x) + \end{align*}\qed + \end{itemize} \end{proof} @@ -2400,39 +2483,8 @@ Now, we prove our main statement. \end{cor} Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor. \subsection{Maybe Functor} -We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$, and for every $x\in\Dom(f)$ we have $f(x)=g(x)$ ($\Dom(f)$ is the domain of a function $f$). -Now, we prove that the given order on the maybe functor is liftable and coliftable. -\begin{lemma}\label{lem:maybe-lif} - The order structure on the set-functor $FX=X+1$ is a liftable order. -\end{lemma} -\begin{proof} -% By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases: -% \begin{itemize} -% \item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$. -% \item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed -% \end{itemize} -Assuming that $h\in\Hom(X,Z+1)$, $g\c Y\to Z$, $k\in\Hom(X,Y+1)$, such that $h\appr (g+1)\comp k$. We define $k'\in\Hom(X,Y+1)$ as follows: -\begin{gather*} - k'(x)= - \begin{cases} - \bot&x\notin\Dom(h)\\ - k(x)&x\in\Dom(h) - \end{cases} -\end{gather*} -We have $\Dom((g+1)\comp k')=\Dom(k')$ and $\Dom(k')=\Dom(h)$, so we have $\Dom((g+1)\comp k')=\Dom(h)$. If $x\in\Dom(h)$, then $h(x)=(g+1)\comp k(x)$ and $(g+1)\comp k(x)=(g+1)\comp k'(x)$, so we have $h(x)=(g+1)\comp k'(x)$. So, we have $h=(g+1)\comp k'$. Additionally, $\Dom(k')\subseteq\Dom(k)$, and for every $x\in \Dom(k')$, we have $k'(x)=k(x)$, so we have $k'\appr k$. \qed -\end{proof} -\begin{lemma}\label{lem:maybe-colif} - The order structure on the set-functor $FX=X+1$ is a coliftable order. -\end{lemma} -\begin{proof} - By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $Fg(k)\appr h$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k\appr k'$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases: - \begin{itemize} - \item $Fg(k)=h$: In this case we take $k'=k$, and then we have $Fg(k')=h$. - - \item $Fg(k)=\bot$: It entails that $k=\bot$. We either have $h=\bot$ or $h\in Y$. If $h=\bot$ then we take $k'=k$, and we are done. If $h\in Y$, then by the surjectivity of $g$, there exists $k'$ such that $g(k')=h$ that entails $Fg(k')=h$ as well.\qed - \end{itemize} -\end{proof} -So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alpha)$ of a functor with a liftable order, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$. +We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$.\\ +Proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alpha)$ of a functor with a liftable order, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$. We have shown that the ordering on the maybe functor is liftable and coliftalbe in~\autoref{prop:maybe-lif} and~\autoref{prop:maybe-colif} %\begin{lemma}\label{lem:maybe-func-set} % Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ % \begin{gather*} @@ -2441,7 +2493,7 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph % \end{gather*} %\end{lemma} %\begin{proof} -% By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. %Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}: +% By~\autoref{prop:alph-prod-dubut} and~\autoref{prop:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. %Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}: %% \begin{enumerate} %% \item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1} %% \item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2} @@ -2585,7 +2637,7 @@ Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g \arrow["{f'}"', tail, from=2-1, to=1-2] \end{tikzcd} \end{equation*} -\begin{lemma}\label{lem:maybe-lif-abs} +\begin{lemma}\label{prop:maybe-lif-abs} The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order. \end{lemma} \begin{proof} @@ -3061,7 +3113,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{proof} \begin{definition}[Mid-lax Barr relator] - Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if we have: + Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$, and $\pi_1$ and $\pi_2$ are surjective, assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if we have: % A relator over a functor $F$ is a one-sided Barr relator, shown by $\overrightarrow{F}$, iff for a partial order $\appr$ over $F$, a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have: \begin{gather*} \overrightarrow{F}r=F\pi_2\comp\appr\comp(F\pi_1)^\op @@ -3194,7 +3246,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i % Since $\appr$ is a coliftable order structure by~\autoref{def:coliftable-ord} there exists a $w$ such that $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$, $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed %\end{proof} \begin{prop}\label{prop:all-rel-compa} - For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that a set-functor $F$ has an order structure $\appr$, the following propositions hold: + For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $\pi_1$ and $\pi_2$ are surjective, assuming that a set-functor $F$ has an order structure $\appr$, the following propositions hold: \begin{enumerate} \item If $\appr$ is liftable, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad F\pi_2\comp(F\pi_1)^\op\comp\appr$ \item If $\appr$ is coliftable, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op$