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

minor

Browse Source
This commit is contained in:
partowp
2026-06-11 13:16:53 +01:00
parent 3903cc0e30
commit 8f306095ee
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+1 -1
View File
@@ -2544,7 +2544,7 @@ The following example justifies why the $g$ in~\autoref{def:coliftable-ord} shou
\end{align*}\qed \end{align*}\qed
\end{proof} \end{proof}
\begin{cor} \begin{cor}
Since the symmetrization of left-lax Barr relator is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator. Since the symmetrization of left-lax Barr relator that is laxed with a lifatble order structure is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator.
\end{cor} \end{cor}
\begin{cor} \begin{cor}
By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is liftable, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well. By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is liftable, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well.