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

good

Browse Source
This commit is contained in:
partowp 2026-05-23 18:03:20 +01:00
parent ac7303d14a
commit 48728470f3
1 changed files with 26 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
draft/draft.tex
View File

@ -2321,13 +2321,33 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
\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{definition}[Natural Order Structure]\label{def:nat-ord}
A \emph{natural order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X\to X'$, $g\c Y\to Y'$, then:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item If $\alpha\appr\beta$ in $\Hom(X,FY)$, $g\c Y\to Y'$, then $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,Y')$.\label{item:cogood:I}
\item If $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.\label{item:cogood:II}
\item $\alpha\comp f\appr\beta\comp f$ in $\Hom(X',Y)$. \label{item:nat-ord:I}
\item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,Y')$. \label{item:nat-ord:II}
\end{enumerate}
\end{definition}
\begin{definition}[Good Order Structure]\label{def:good-ord}
A \emph{good order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr Fg\comp k$ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
\end{definition}
\begin{definition}[Cogood Order Structure]\label{def:cogood-ord}
A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
\end{definition}
\begin{lemma}
Assuming that a a functor $F$ has an order structure $\appr$ that is cogood, then for every $f\in\Hom(X,FY)$ we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item $Ff\comp\appr\quad=\quad\appr\comp Ff$
\item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$
\end{enumerate}
\end{lemma}
\begin{proof}
$(I)$Assuming $t\mathrel{Ff\comp\appr} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is good, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{\appr\comp Ff} x$.
Assuming $t\mathrel{\appr\comp Ff} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:cogood-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{Ff\comp\appr}s$.
$(II)$\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}
@ -2344,7 +2364,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
z \mathrel{\appr} z',\\
z'\mathrel{(F\pi_j)} y.
\end{gather*}
Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$.
Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\ref{item:nat-ord:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$.
Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
\begin{gather*}
@ -2352,7 +2372,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
z \mathrel{(F\pi_j)} y',\\
y' \mathrel{\appr} y.
\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
Since $\appr$ is a cogood order structure by~\autoref{def:cogood-ord} 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: