diff --git a/draft/draft.tex b/draft/draft.tex index 99fd0c0..0810210 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2341,15 +2341,15 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{enumerate} \end{definition} -\begin{definition}[Good Order Structure]\label{def:good-ord} - A \emph{good 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'$. +\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'$. \end{definition} -\begin{definition}[Cogood Order Structure]\label{def:cogood-ord} - A \emph{cogood 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'$. +\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'$. \end{definition} \begin{lemma}\label{lem:set-ord-str} - In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a good order structure. + In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a liftable order structure. \end{lemma} \begin{proof} For every $f,g\in\Hom(X,FY)$, we define $f\appr g$ whenever for all $x\in X$, $f(x)\leq g(x)$. @@ -2360,19 +2360,19 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \qed \end{proof} \begin{remark}\label{rem:set-ord-str-co} - The exact same argument in~\autoref{lem:set-ord-str} is true for cogood order structures. + The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures. \end{remark} -\begin{lemma}\label{lem:good} - Assuming that a a functor $F$ has an order structure $\appr$ that is good, then for every $f\in\Hom(X,FY)$ we have: +\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} \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 good, 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$. + $(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:good-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$. + 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*} @@ -2381,17 +2381,17 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{gather*} So it follows directly from applying $\op$ on both sides of $(I)$.\qed \end{proof} -\begin{lemma}\label{lem:cogood} - Assuming that a a functor $F$ has an order structure $\appr$ that is cogood, then for every surjective $f\in\Hom(X,FY)$ we have: +\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 cogood, 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$. + $(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:cogood-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$. + 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*} @@ -2401,7 +2401,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i So it follows directly from applying $\op$ on both sides of $(I)$.\qed \end{proof} %\begin{prop} -% For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold: +% For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a coliftable order structure $\appr$, the following propositions hold: % \begin{enumerate} % \item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$ % \item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$ @@ -2416,7 +2416,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i % z \mathrel{\appr} z',\\ % z'\mathrel{(F\pi_j)} y. % \end{gather*} -% Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\ref{item:nat-ord:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$. +% Then from $z \mathrel{\appr} z'$ since $\appr$ is a coliftable order structure by~\ref{item:nat-ord:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$. % % Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that % \begin{gather*} @@ -2424,14 +2424,14 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i % z \mathrel{(F\pi_j)} y',\\ % y' \mathrel{\appr} y. % \end{gather*} -% Since $\appr$ is a cogood order structure by~\autoref{def:cogood-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 +% 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: \begin{enumerate} - \item If $\appr$ is good, 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 cogood, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op$ - \item If $\appr$ is both good and cogood, all the following are equal: + \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$ + \item If $\appr$ is both liftable and coliftable, all the following are equal: \begin{itemize} \item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad$ \item $F\pi_2\comp(F\pi_1)^\op\comp\appr$ @@ -2441,18 +2441,18 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{enumerate} \end{prop} \begin{proof} - They all follow in an obvious way from~\autoref{lem:good} and~\autoref{lem:cogood}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed + They all follow in an obvious way from~\autoref{lem:liftable} and~\autoref{lem:coliftable}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed \end{proof} \begin{example} - In the category of sets, subset over the powerset functor is an example of a good order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$. + In the category of sets, subset over the powerset functor is an example of a liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$. Assuming $z\in\powf g(k')$, then there exists $y'\in \{y\mid g(y)\in h\}$ that $z=g(y')$, so $z\in h$ and $\powf g(k')\subseteq h$. Assuming $z\in h$, since $h\subseteq \powf g(k)$, then $z\in\powf g(k)$. So, there exists $y'\in k$ such that $g(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means $z\in\powf g(k')$.\qed \end{example} -The following example justifies why the $g$ in~\autoref{def:cogood-ord} should be surjective: +The following example justifies why the $g$ in~\autoref{def:coliftable-ord} should be surjective: \begin{example} - If we take the surjectivity of $g$ out of~\autoref{def:cogood-ord}, subset relation over the powerset functor is NOT an example of a cogood order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$, + If we take the surjectivity of $g$ out of~\autoref{def:coliftable-ord}, subset relation over the powerset functor is NOT an example of a coliftable order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$, \begin{gather*} g(z)= \begin{cases} @@ -2473,7 +2473,7 @@ The following example justifies why the $g$ in~\autoref{def:cogood-ord} should b then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$. \end{example} \begin{example} - In the category of sets, subset over the powerset functor is an example of a cogood order structure if the $g$ in~\autoref{def:cogood-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$. + In the category of sets, subset over the powerset functor is an example of a coliftable order structure if the $g$ in~\autoref{def:coliftable-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$. Obviously, $\powf g(k')\subseteq h$. Now, assuming $z\in h$ we prove that $z\in \powf g(k')$. Since $g$ is surjective, then exists $A\subseteq Y$ such that $\powf g(A)=h$. By the definition of $k'$, $A\subseteq k'$. So from $z\in h$ we have $z\in \powf g(A)$ that means that exists $a\in A$, such that $g(a)=z$. Now, since $A\subseteq k'$, then $a\in k'$. So, we have $z\in \powf g(k')$.\qed \end{example} @@ -2491,19 +2491,19 @@ The following example justifies why the $g$ in~\autoref{def:cogood-ord} should b \end{prop} \begin{prop} - Assuming that a set-functor $F$ has a good order structure $\appr$, then the $F$-relator $\relar r=\appr\comp Fr$ is natural. + Assuming that a set-functor $F$ has a liftable order structure $\appr$, then the $F$-relator $\relar r=\appr\comp Fr$ is natural. \end{prop} \begin{proof} \begin{align*} \relar (g^\op\comp r\comp f)&\\ =&\appr\comp F(g^\op\comp r\comp f)\\ =&\appr\comp(Fg^\op)\comp Fr\comp Ff\\ - =&(Fg^\op)\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:good}}\\ + =&(Fg^\op)\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:liftable}}\\ =&(Fg^\op)\comp\relar r\comp Ff \end{align*}\qed \end{proof} \begin{remark} - One may wonder if the above proposition is true for $F$-relators $r\mapsto Fr\comp\appr$ or $r\mapsto \appr\comp Fr\comp\appr$, where the order structure $\appr$ over $F$ is cogood. But it may not be the case because the surjectivity condition on the $g$ in~\autoref{def:cogood-ord} prevents the same reasoning. + One may wonder if the above proposition is true for $F$-relators $r\mapsto Fr\comp\appr$ or $r\mapsto \appr\comp Fr\comp\appr$, where the order structure $\appr$ over $F$ is coliftable. But it may not be the case because the surjectivity condition on the $g$ in~\autoref{def:coliftable-ord} prevents the same reasoning. \end{remark} \begin{prop} Symmetrization of a natural relator, is natural. @@ -2547,14 +2547,14 @@ The following example justifies why the $g$ in~\autoref{def:cogood-ord} should b Since the symmetrization of left-lax Barr relator is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator. \end{cor} \begin{cor} - By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is good, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well. + By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is liftable, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well. \end{cor} -Perhaps if we can relax the definition of good by allowing $g$ to be a relation rather than a function, we can have a lax Barr relator that its symmetrization is a normal lax extension.\todo{Investigate!} +Perhaps if we can relax the definition of liftable by allowing $g$ to be a relation rather than a function, we can have a lax Barr relator that its symmetrization is a normal lax extension. Well, this idea actually does not work because if $g$ is supposed to be a relation, then $F$ can not be a set-functor, but it should be a functor on $\rel$, and it is already a big assumption. \begin{prop} - For a natural order structure $\appr$ on a set-functor $F$, if for every $f\in\Hom(X,FY)$ we have $Ff\comp\appr=\appr\comp Ff$, then $\appr$ is cogood. + For a natural order structure $\appr$ on a set-functor $F$, if for every $f\in\Hom(X,FY)$ we have $Ff\comp\appr=\appr\comp Ff$, then $\appr$ is coliftable. \end{prop} \begin{proof} - \todo{Investigate if it's true! If it is, is naturality necessary? It is really weird! If having a good order structure forces every witness for AM-simulation to have the left cell of the lax diagram as equality, and subset on powerset functor is a good order structure, then what is the counter-example number 4 that you have?!} + \todo{Investigate if it's true! If it is, is naturality necessary? It is really weird! If having a liftable order structure forces every witness for AM-simulation to have the left cell of the lax diagram as equality, and subset on powerset functor is a liftable order structure, then what is the counter-example number 4 that you have?!} \end{proof} \begin{prop} Assuming that $\relar$ is a difunctionally functorial relator, then the symmetrization of the relator that takes $r\c X\rto Y$ to $\relar r\comp\appr$ is a sound relator.