Skip to content
Snippets Groups Projects
Commit 888e33f5 authored by Philip Kaluđerčić's avatar Philip Kaluđerčić :u7121:
Browse files

Use a more consistent notation in the bisimulation sketch

parent 288a3dc9
Branches
Tags
No related merge requests found
......@@ -332,8 +332,8 @@
\((C, c) \xleftarrow{\outm{1}} (R, r) \xrightarrow{\outm{2}} (D,
d)\) we can construct a \de{pullback}
\(\mathsf{Pb}(\outm{1}, \outm{2}) = (P, p)\). In \(\Set\) this
exist necessarily, meaning that the \des{morphism}
\((C, c) \xrightarrow{q_1} (P, p) \xleftarrow{p_2} (D, d)\) provide
exist necessarily, meaning that the cone \des{morphism}
\((C, c) \xrightarrow{p_1} (P, p) \xleftarrow{p_2} (D, d)\) provide
the intended \defn{beheqiv}{behavioural equivalence}.
\end{proof}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment