diff --git a/draft/draft.tex b/draft/draft.tex
index 1336985..443c1d9 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -2311,6 +2311,16 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 %		y' \mathrel{\sqsubseteq} y.
 %	\end{gather*}
 %\end{proof}
+\begin{prop}
+	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ is either the maybe monad, the subdistribution monad or $FX=\powf(X\times A)$, where $A$ is a set of labels, then 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$
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\end{proof}
 \begin{definition}[Cogood Order Structure]\label{def:cogood}
 	A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
@@ -2344,6 +2354,39 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	\end{gather*}
 	Since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:II} 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}
+	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:
+	\begin{enumerate}
+		\item $F\pi_2\comp\sappr\comp(F\pi_1)^\op\quad=\quad F\pi_2\comp(F\pi_1)^\op\comp\appr$
+		\item $F\pi_1\comp\sappr\comp(F\pi_2)^\op\quad=\quad F\pi_1\comp(F\pi_2)^\op\comp\appr$
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\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:
+	\begin{enumerate}
+		\item $F\pi_2\comp\appr\comp\sappr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op\comp\appr$
+		\item $F\pi_1\comp\appr\comp\sappr\comp(F\pi_2)^\op\quad=\quad \appr\comp F\pi_1\comp(F\pi_2)^\op\comp\appr$
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\end{proof}
+\begin{prop}
+	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a good order structure $\appr$, the following propositions hold:
+	\begin{enumerate}
+		\item $F\pi_2\comp\sappr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
+		\item $F\pi_1\comp\sappr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\end{proof}
+\begin{prop}
+	Assuming that $\relar$ is a difunctionally functorial relator, then the symmetrization of the relator that take $r\c X\rto Y$ to $\relar r\comp\appr$ is a sound relator. 
+\end{prop}
 \begin{prop}
 	Assuming that $\relar$ is a relator over $F\c\Set\to\Set$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then the symmetrization of the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator.
 \end{prop}