fail

draft/draft.tex

@@ -2295,7 +2295,7 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 	\end{gather*}
 \end{definition}
 %
-\begin{lemma}
+\begin{lemma}\label{lem:yoneda}
 	Given objects $A$, $X$, and $Y$ in a category $\BC$, then we have:
 	\begin{gather*}
 		\Hom(X,Y)\iso \Hom(\Hom(A,X),\Hom(A,Y))
@@ -2309,7 +2309,7 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 	If we substitute $G$ with $\Hom(\argument,Y)$ then we have the following:
 	\begin{gather*}
 		\Hom(\argument,Y)\iso\Hom(\Hom(\argument,X),\Hom(\argument,Y))
-	\end{gather*}
+	\end{gather*}\qed
 \end{proof}
 %
 \begin{prop}
@@ -2317,7 +2317,7 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 \end{prop}
 \begin{proof}
 	$(\Rightarrow):$ For every $u\in\Hom(1,R)$ we take $v\in\Hom(1,S)$ to be $w\comp u$.\\
-	$(\Leftarrow):$ \todo{Finish, using the concrete proof.}
+	$(\Leftarrow):$ Given that $(g_1,g_2)$ is a morphism in $\spa_a(\BC)$ then for every $u\in\Hom(1,R)$ there exists $v\in\Hom(1,S)$ such that $g_1\comp p_1\comp u=q_1\comp v$ and $g_2\comp p_2\comp u=q_2\comp v$. We define a function that takes $u\in\Hom(1,R)$ and gives $V_u\in\powf\Hom(1,S)$ such that for every $v\in V_u$ we have $g_1\comp p_1\comp u=q_1\comp v$ and $g_2\comp p_2\comp u=q_2\comp v$, and $V_u\neq\emptyset$. The axiom of choice gives us a function $s\c\im_h\to\Hom(1,S)$. So, we define a function $k\c\Hom(1,R)\to\Hom(1,S)$ such that $k=s\comp e_h$, where $e_h\c\Hom(1,R)\to\im_h$ is the epimorphism in the image factorization of $h$. By~\autoref{lem:yoneda}, there exists a bijection $\nu\c\Hom(\Hom(1,R),\Hom(1,S))\to\Hom(R,S)$.
 \end{proof}
 %
 \begin{definition}