minor

draft/draft.tex

@@ -2537,7 +2537,7 @@ The following example justifies why the $g$ in~\autoref{def:cogood-ord} should b
 \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.
 \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 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. 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.
 \end{prop}