bluh

draft/draft.tex

@@ -476,6 +476,16 @@ We want to say that a natural order structure entails an order over a functor de
 	$\appr$ being a liftable order structure on $F$ means that for morphisms $g\c Y\to Z$, $k\in\Hom(X,FY)$, and $h\in\Hom(X,FZ)$ that $g$ is epic, if $h\appr Fg\comp k$ then exists $k'\in\Hom(X,FY)$, such that $k\appr k'$ and $h=Fg\comp k'$. %Now, assuming $\alpha\c Y\to Z$, $\mu\in\Hom(X,FGY)$, and $\nu\in\Hom(X,FGZ)$ that $\alpha$ is epic, we need to prove that exists some $\mu'\in\Hom(X,FGY)$ such that $\mu'\appr\mu$ and $\nu=FG\alpha\comp\mu'$. Since $G$ preserves epimorphisms and $\alpha$ is epic, then $G\alpha$ is also epic. Furthermore, since $\appr$ is a liftable order structure on $F$, then the mentioned $\mu'$ exists.\qed  
 	Now, assuming $\alpha\c Y\to Z$, $\mu\in\Hom(X,FGY)$, and $\nu\in\Hom(X,FGZ)$ that $\alpha$ is epic. Since $G$ is assumed to preserve epimorphisms, $G\alpha$ is epic. Since $\appr$ is a liftable order structure on $F$, then there exists some $\mu'\in\Hom(X,FGY)$ such that $\mu'\appr\mu$ and $\nu=FG\alpha\comp\mu'$. So, $\appr$ is a liftable order structure for $FG$ as well.\qed
 \end{proof}
+\begin{rem}
+	For every regular category $\BC$ with the axiom of choice, every functor $G\c\BC\to\BC$ preserves epimorphisms. Assuming $e\c X\to Y$ is epic, then it has a section $s\c Y\to X$. Applying $G$ on both of them we have $Ge\c GX\to GY$ and $Gs\c GY\to GX$ that
+	\begin{align*}
+		Ge\comp Gs&\\
+		=&G(e\comp s)\\
+		=&G(\id_Y)\\
+		=&\id_{GY}
+	\end{align*}
+	that means that $Gs$ is a section for $Ge$ that entails that $Ge$ is epic.
+\end{rem}
 \todo{It seems too much, but perhaps you can study if you can derive an order structure from $F$ to $G$ and consequently $GF$, by the following rule:
 \begin{gather*}
 	\infer{Gh\appr GFg\comp Gk}{h\appr Fg\comp k}
@@ -3672,6 +3682,14 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 	\todo{Write it down. You have it in your notes.}
 \end{proof}
 \todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion. See if~\autoref{prop:lax-relator-full-comm} or~\autoref{lem:lax-relator-str} can help!}
+%
+%\begin{prop}
+%	For every functor $F\c\Set\to\Set$, assuming $\relar$ is the left-lax Barr relator for $F$, then for every relation $r\subseteq X\times Y$, we have $\hat{\relar}r\subseteq \bar{F}r$.
+%\end{prop}
+%\begin{proof}
+%	
+%\end{proof}
+%
 \subsection{Symmetric relation}
 \begin{prop}
 Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a coalgebra $(X,\alpha)$, then $r$ is an $\hat{\relar}$-bisimulation.
@@ -3687,6 +3705,9 @@ Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a
 	\end{align*}
 	Now, assuming $x\mathrel{r}y$ gives us $x\mathrel{(\alpha^\op\comp\relar r\comp \alpha)} y$ that is equivalent with saying that exist $x'$ and $y'$ such that $x\mathrel{\alpha}x'$, $y\mathrel{\alpha}y'$, and $x'\mathrel{\relar r}y'$. Since $r$ is symmetric, we have $y\mathrel{r} x$ that means that exist $x''$ and $y''$ such that $x\mathrel{\alpha}x''$, $y\mathrel{\alpha}y''$, and $y''\mathrel{\relar r}x''$. On the other hand since $\alpha$ is a function, we have $x''=x'$ and $y''=y'$, so we have $y'\mathrel{\relar r}x'$ that ultimately gives $x\mathrel{(\alpha^\op\comp\hat{\relar}r\comp\alpha)}y$. So, $r$ is an $\hat{\relar}$-bisimulation as well.\qed
 \end{proof}
+\begin{cor}
+	For a functor $F\c\Set\to\Set$, assuming that for a relation $r$ we have $\appr\comp\bar{F}r\leq\bar{F}r$, if $r$ is symmetric, and it is a $\appr\comp\bar{F}$-simulation, then it is a $\hat{\appr\comp\bar{F}}$-bisimulation.\ppnote{This is a bad notation for lax Barr-relators. Switch them with $F^\rightarrow$, $F^\leftarrow$, and $F^\leftrightarrow$.}
+\end{cor}
 \end{document}