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

pc sync

Browse Source
This commit is contained in:
Sergey Goncharov
2026-07-20 14:05:33 +01:00
parent 81da58d639
commit 3d36dc3293
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
@@ -3077,7 +3077,7 @@ The following example justifies why the $g$ in~\autoref{def:coliftable-ord} shou
\end{align*}\qed
\end{proof}
\begin{cor}
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.
Since the symmetrization of left-lax Barr relator 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}
\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.