From 798ca20433d97297ae30e3a053dadded67ec4026 Mon Sep 17 00:00:00 2001 From: partowp Date: Mon, 28 Sep 2026 15:08:17 +0100 Subject: [PATCH] fail --- draft/draft.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 40362d2..957ff7d 100644 --- a/draft/draft.tex +++ b/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}