pouya/coalgebraic-simulation
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

lemma

Browse Source
This commit is contained in:
partowp
2026-09-27 18:02:05 +01:00
parent 96194207bf
commit 0482ae66f5
1 changed files with 8 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+8 -7
View File
@@ -2298,18 +2298,19 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
\begin{lemma} \begin{lemma}
Given objects $A$, $X$, and $Y$ in a category $\BC$, then we have: Given objects $A$, $X$, and $Y$ in a category $\BC$, then we have:
\begin{gather*} \begin{gather*}
\Hom(X,Y)\iso \Hom(\Hom(A,X)\to\Hom(A,Y)) \Hom(X,Y)\iso \Hom(\Hom(A,X),\Hom(A,Y))
\end{gather*} \end{gather*}
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
It is entailed by the Yoneda lemma. \todo{Finish! You may need cartesian closedness!} It is entailed by the Yoneda lemma. The contravariant version of the Yoneda's lemma says that given a functor $G\c\BC^\op\to\Set$ the following correspondance holds:
\end{proof}
\begin{cor}
Given objects $X$ and $Y$ in a category $\BC$, then we have:
\begin{gather*} \begin{gather*}
\Hom(X,Y)\iso \Hom(\Hom(1,X)\to\Hom(1,Y)) GX\iso\Hom(\Hom(\argument,X),G)
\end{gather*} \end{gather*}
\end{cor} 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{proof}
% %
\begin{prop} \begin{prop}
Assuming the axiom of choice, given $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ iff there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$. Assuming the axiom of choice, given $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ iff there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$.