\documentclass{beamer}

\usetheme{focus}
% Add option [numbering=none] to disable the footer progress bar
% Add option [numbering=fullbar] to show the footer progress bar as always full with a slide countx


\definecolor{main}{RGB}{29, 160, 196}
\definecolor{text}{RGB}{15, 40, 60}
\definecolor{background}{RGB}{255, 255, 255}
\definecolor{catchgreen}{RGB}{0, 166, 147}
\setbeamercolor{block title alerted}{fg=white, bg=catchgreen}
\setbeamercolor{block body alerted}{fg=text, bg=catchgreen!10}

\setbeamertemplate{block begin}
{
  \par\vskip\medskipamount%
  \IfStrEq{\insertblocktitle}{}{}{
      \begin{beamercolorbox}[colsep*=.75ex]{block title}
        \usebeamerfont*{block title}\insertblocktitle%
      \end{beamercolorbox}%
  }
  {\parskip0pt\par}%
  \ifbeamercolorempty[bg]{block title}
  {}
  {\ifbeamercolorempty[bg]{block body}{}{\nointerlineskip\vskip-0.5pt}}%
  \usebeamerfont{block body}%
  \begin{beamercolorbox}[colsep*=.75ex,vmode]{block body}%
    \ifbeamercolorempty[bg]{block body}{\vskip-.25ex}{\vskip-.75ex}\vbox{}%
}


\setbeamercovered{invisible}

%------------------------------------------------




\usepackage{booktabs} % Required for better table rules
\usepackage{xstring}
%\usepackage{tikz}
\renewcommand{\baselinestretch}{1.3}
\usepackage[T1]{fontenc}
\usepackage[sfdefault]{AlegreyaSans}
\usepackage{bussproofs}
\EnableBpAbbreviations
\usepackage{multicol}
\usepackage{transparent}
\usepackage{lipsum}
\usepackage{graphicx}
\usepackage{eso-pic}
\usepackage{proof}
\usepackage{amsthm}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{hyperref}
\usepackage{amssymb}
\usepackage{mathtools}
\usepackage{minted}
\usepackage{wasysym}
\usepackage{fontawesome}
\usepackage{tikz-cd}
\usepackage{xcolor}
\usepackage{multicol}
\usepackage{abraces}
\usepackage{accsupp}
\usepackage{stmaryrd}
\usepackage{multicol}




\def\bs{{\;\Downarrow\;}}
\def\la#1{\stackrel{#1}{\rightarrow}}
\def\a{\rightarrow}
\def\as{\rightarrow^{\star}}
\def\sp{{\hspace{1cm}}}
\def\mp{{\hspace{0.66cm}}}
\newcommand{\Dar}{\Downarrow}
\newcommand{\val}{\mathsf{v}}
\newcommand{\com}{\mathsf{c}}
\newcommand{\comp}{\cdot}
\newcommand{\inl}{\mathsf{inl}}
\newcommand{\inr}{\mathsf{inr}}
\newcommand{\id}{\mathsf{id}}
\renewcommand{\prod}{\mathbin{\text{\rotatebox[origin=c]{180}{$\amalg$}}}}
\renewcommand{\coprod}{\mathbin{\text{{$\amalg$}}}}
\newcommand{\lcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\LEFTcircle$}}}}
\newcommand{\fcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\CIRCLE$}}}}
\newcommand{\tcomp}{\textsf{comp}}
\newcommand{\unt}{\mathsf{unit}}
\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}	
\newcommand{\bool}{\mathsf{bool}}	
\newcommand{\fpc}{\mathsf{fix}}	
\newcommand{\casec}{\mathsf{if}}
\newcommand{\ndet}{\oplus} %{\pmb{\klplus}}
%\newcommand{\paral}{\parallel} 
% {\ensuremath{\boldsymbol{\mid\mid}}}
\newcommand{\paralv}{\pmb{\parallel_\val}}
\newcommand{\hask}{\includegraphics[height=\fontcharht\font`\B]{res/haskell-logo.png}}
\newcommand{\mS}{\mu\Sigma}
\newcommand{\lbs}[1]{{\mathrel{\;\overset{\raisebox{4pt}{$\scriptstyle #1$\;}}{\smash{\xRightarrow{\hspace{.75em}}}}\;}}}
\newcommand{\ubs}{{\mathrel{\;\overset{\raisebox{4pt}{\;}}{\smash{\xRightarrow{\hspace{.75em}}}}\;}}}
\newcommand{\bba}{
	\mathrel{%
		\begin{tikzpicture}[baseline=-6pt]
			\draw[double, double distance=.75pt, -{Stealth[inset=0pt, angle=75:4pt]}] (0,.02) -- (0,-.28);
		\end{tikzpicture}%
	}%
}
\newcommand{\relar}{\mathsf{R}}
\newcommand{\powf}{\mathcal{P}}
\newcommand{\eval}{\mathsf{eval}}
\newcommand{\refl}{\mathsf{refl}}
\newcommand{\trans}{\mathsf{trans}}
\newcommand{\preord}{\mathbf{PreOrd}}
\newcommand{\rel}{\mathbf{Rel}}
\newcommand{\spa}{\mathbf{Span}}
\newcommand{\gra}{\mathbf{Gra}}
\newcommand{\obj}{\mathbf{Obj}}
\newcommand{\emre}{\mathbf{L}}
\newcommand{\spto}{\mathrel{\tikz{\draw[-{Stealth}] (0.0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
\newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0.04,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);\draw (0.04,0) -- (0,-0.07);\draw (0.04,0) -- (0,0.07);}}}
\newcommand{\powfi}{\mathcal{P}_{\mathsf{inj}}}
\newcommand{\appr}{\sqsubseteq}
\newcommand{\sappr}{\sqsupseteq}
\newcommand{\Dom}{\mathsf{Dom}}
\newcommand{\Set}{\mathbf{Set}}

\newcommand{\simeet}{%
	\mathbin{%
		\ooalign{%
			$\sqcap$\cr
			\hidewidth\raisebox{0.2ex}{\scalebox{0.44}{$\otimes$}}\hidewidth\cr
		}%
	}%
}

\title{\Large  Coalgebraic Notions of Simulation, Bisimulation and Relators}

\author{\small Pouya Partow\\
\footnotesize Joint work with Sergey Goncharov}

%\titlegraphic{\transparent{0.1}\includegraphics[width=\textwidth,height=\textheight]{res/ut-logo.png}}

\titlegraphic{\transparent{1} \includegraphics[scale=0.1]{res/ut-logo.png}}

\institute{\small  School of Computer Science\\ University of Birmingham}

\date{ACV 2026\\ July 25th 2026\\ Lisbon}


\begin{document}


\begin{frame}
	\maketitle
\end{frame}

\setlength{\parskip}{2ex}
%
\begin{frame}{Overview}
	The content of the talk:
	\begin{itemize}
		\item Intuitive introduction to coalgebra and (bi)simulation
		\item Reviewing basic definitions of coalgebra and (bi)simulation
		\item Our motivation: To ease proving program equivalence
		\item Relator-based notions
		\item Span-based notions
	\end{itemize}
\end{frame}

\begin{frame}{Why Does Equivalence of Systems Matter?}
	\begin{alertblock}{A basic but fundamental question}
		When can we say that two systems \emph{behave the same}?
	\end{alertblock}
	\vspace{-0.4cm}
	This question is everywhere, often silently assumed:\vspace{-0.4cm}
	\begin{itemize}
		\setlength{\itemsep}{6pt}
		\item[\faServer] \textbf{Hardware redesign.} A chip redesigned for cheaper production must still compute exactly what the old one did.
		\item[\faCode] \textbf{Software upgrades.} A bank replaces its backend --- from the customer's view (balances, transactions), nothing should change.
	\end{itemize}
	\vspace{0.2cm}
	\begin{block}{The catch}
		``Behaving the same'' is intuitive, but making it \emph{precise} and \emph{checkable} is surprisingly subtle.
	\end{block}
\end{frame}
%\begin{frame}{From ``System'' to Mathematics}
%	\begin{block}{The word ``system'' needs to be made precise}
%		To reason formally about equivalence, we need a precise model of what a system \emph{is}.
%	\end{block}
%	\vspace{0.3cm}
%	In this work, systems are modeled as \textbf{Kripke frames}.
%	\begin{block}{Definition: Kripke frame}
%		A pair $(W, R)$ where $W$ is a set of \emph{states}, and $R \subseteq W \times W$ is a \emph{transition relation}.
%	\end{block}
%\end{frame}

\begin{frame}{From ``System'' to Mathematics}
%	\vspace{-0.6cm}
	\begin{block}{}
	We model systems as mathematical notions like \textbf{labeled transition systems}: a set of states, together with a labeled transition relation between them.
	\end{block}
	\begin{alertblock}{Example: a vending machine}
%		\begin{columns}
%			\column{0.5\textwidth}
%			After inserting a coin, the machine may nondeterministically dispense \emph{coffee} or \emph{tea} --- then return to its idle state.
%			\column{0.5\textwidth}
			\begin{center}
				\begin{tikzpicture}[>=stealth, thick]
					\node[circle, draw, minimum size=1cm] (brewing tea)    at (0,1.8)   {$\mathsf{brewing\;tea}$};
					\node[circle, draw, minimum size=1cm] (idle)   at (4,1.8)     {$\mathsf{idle}$};
					\node[circle, draw, minimum size=1cm] (active)   at (4,0)   {$\mathsf{active}$};
					\node[circle, draw, minimum size=1cm] (brewing coffee) at (8,1.8)   {$\mathsf{brewing\;coffee}$};
					
					\draw[->] (idle) -- node[left] {insert coin} (active);
					\draw[->] (active) to[bend right=20] node[below] {select coffee} (brewing coffee);
					\draw[->] (active) to[bend left=20] node[below] {select tea} (brewing tea);

					\draw[->] (brewing coffee) -- node[above] {take drink} (idle);
					\draw[->] (brewing tea) -- node[above] {take drink} (idle);
				\end{tikzpicture}
			\end{center}
%		\end{columns}
	\end{alertblock}
\end{frame}

\begin{frame}{Simulation and Bisimulation}
	
	\begin{columns}[T]
		
		\column{0.47\textwidth}
		
		\begin{alertblock}{Similar to}
			\centering
			\begin{tikzpicture}[>=stealth, thick, scale=1, every node/.style={transform shape}]
				\node[circle, draw, minimum size=.9cm] (tea)    at (0,1.8)   {\scriptsize brewing tea};
				\node[circle, draw, minimum size=.9cm] (idle)   at (4,1.8)   {\scriptsize idle};
				\node[circle, draw, minimum size=.9cm] (active) at (4,0)     {\scriptsize active};
				
				\draw[->] (idle) -- node[left,font=\tiny] {insert coin} (active);
				\draw[->] (active) to[bend left=20]
				node[below,font=\tiny] {select tea} (tea);
				
				\draw[->] (tea) -- node[above,font=\tiny] {take drink} (idle);
			\end{tikzpicture}
		\end{alertblock}
		
		\column{0.47\textwidth}
		
		\begin{alertblock}{Bisimilar with}
			
			\centering
			
			\begin{tikzpicture}[>=stealth, thick, scale=.9, every node/.style={transform shape}]
				\node[circle, draw, minimum size=1cm] (tea)    at (0,1.8)   {\scriptsize brewing tea/coffee};
				\node[circle, draw, minimum size=1cm] (idle)   at (4,1.8)   {\scriptsize idle};
				\node[circle, draw, minimum size=1cm] (active) at (4,0)     {\scriptsize active};
				
				\draw[->] (idle) -- node[left,font=\tiny] {insert coin} (active);
				\draw[->] (active) to[bend left=20]
				node[below,font=\tiny] {select tea} (tea);
				\draw[->] (active) to[bend left=10]	node[above,font=\tiny,yshift=2mm] {select coffee} (tea);
				
				\draw[->] (tea) -- node[above,font=\tiny] {take drink} (idle);
			\end{tikzpicture}
			
		\end{alertblock}
		
	\end{columns}
%	
%	\vspace{-2mm}
%	
	\begin{block}{}
			\begin{center}
				\begin{tikzpicture}[>=stealth, thick, scale=.7, every node/.style={transform shape}]
					\node[circle, draw, minimum size=1cm] (brewing tea)    at (0,1.8)   {$\mathsf{brewing\;tea}$};
					\node[circle, draw, minimum size=1cm] (idle)   at (4,1.8)     {$\mathsf{idle}$};
					\node[circle, draw, minimum size=1cm] (active)   at (4,0)   {$\mathsf{active}$};
					\node[circle, draw, minimum size=1cm] (brewing coffee) at (8,1.8)   {$\mathsf{brewing\;coffee}$};
					
					\draw[->] (idle) -- node[left] {insert coin} (active);
					\draw[->] (active) to[bend right=20] node[below] {select coffee} (brewing coffee);
					\draw[->] (active) to[bend left=20] node[below] {select tea} (brewing tea);
					
					\draw[->] (brewing coffee) -- node[above] {take drink} (idle);
					\draw[->] (brewing tea) -- node[above] {take drink} (idle);
				\end{tikzpicture}
			\end{center}
			%		\end{columns}
	\end{block}
	
\end{frame}

\begin{frame}{Mathematical Definitions}
	
	\footnotesize
	
	\begin{columns}[T,onlytextwidth]
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.48\textwidth}
		
		\begin{alertblock}{Labelled Transition Systems}
			A \emph{labelled transition system} is a triple	$(X,A,T)$, where $T\;\subseteq\;X\times A\times X$.	
			We write $x\xrightarrow{a}x'$
			for $(x,a,x')\in T$.
		\end{alertblock}
		
		\vspace{2mm}
		
		\begin{block}{Simulation and Bisimulation}
			
			A relation $R\subseteq X\times Y$ is a simulation from $(X,A,T)$ to $(Y,A,S)$ whenever
			\[
				\begin{tikzcd}[ampersand replacement=\&]
					x \& y \\
					{x'} \& {y'}
					\arrow["R"{description}, no head, from=1-1, to=1-2]
					\arrow["a"', from=1-1, to=2-1]
					\arrow["a", dashed, from=1-2, to=2-2]
					\arrow["R"{description}, dashed, no head, from=2-1, to=2-2]
				\end{tikzcd}
			\]
%			A simulation relation like $R$ is a bisimulation whenever
%			\[
%			x\mathrel{R}y,\;
%			y\xrightarrow{a}y'
%			\Rightarrow
%			\exists\,x'.\;
%			x\xrightarrow{a}x'
%			\;\land\;
%			x'Ry'.
%			\]
		\end{block}
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.48\textwidth}
		\begin{block}{Bisimulation}
			A simulation relation like $R$ is a bisimulation whenever:\vspace{-0.5cm}
			\[
			\begin{tikzcd}[ampersand replacement=\&]
				x \& y \\
				{x'} \& {y'}
				\arrow["R"{description}, no head, from=1-1, to=1-2]
				\arrow["a", dashed, from=1-1, to=2-1]
				\arrow["a"', from=1-2, to=2-2]
				\arrow["R"{description}, dashed, no head, from=2-1, to=2-2]
			\end{tikzcd}
			\]
		\end{block}
		\vspace{-0.2cm}
		\begin{alertblock}{Similarity and Bisimilaritiy}
			The \emph{similarity relation} $\precsim\subseteq X\times Y$ is the greatest simulation relation. Equivalently 
			\vspace{-0.3cm}
			\[
			x\precsim y
			\iff
			\exists\,R.\;
			xRy,
			\]
			where $R$ is a simulation.\\
			Similarity is defined similarly, where $R$ is a simulation, and it is shown with $\precsim$.
%			Similarly, the \emph{bisimilarity relation} $\sim\subseteq X\times Y$ is the greatest bisimulation relation. Equivalently\vspace{-0.3cm}
%			\[
%			x\sim y
%			\iff
%			\exists\,R.\;
%			xRy,
%			\]
%			where $R$ is a bisimulation.
		\end{alertblock}
%		\vspace{-0.2cm}
%			Ultimately, people care about similarity and bisimilarity, but simulation and bisimulation should be defined first.
	\end{columns}
	
\end{frame}

\begin{frame}{Coalgebras: A Uniform View of Transition Systems}
	
	\small
	
	\begin{columns}[T]
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{0.48\textwidth}
		\begin{alertblock}{Coalgebras}
			\vspace{-2mm}
			Fix an endofunctor
			\vspace{-2mm}
			\[
			F:\mathbf{C}\rightarrow\mathbf{C}.
			\]
			\vspace{-2mm}
			An $F$-coalgebra is a pair $(X,\gamma)$, consisting of an object $X$, and a map
			\vspace{-2mm}
			\[
			\gamma:X\rightarrow FX.
			\]
			\vspace{-2mm}
			Different choices of $F$ describe
			different transition systems.
			\vspace{-1mm}
		\end{alertblock}
		
		\vspace{-1mm}
		
		\begin{block}{Our Goal}
			\centering
			Develop
			\textbf{simulation, bisimulation}
			once, for all coalgebras.
		\end{block}
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{0.48\textwidth}
		
		
		\begin{alertblock}{Different kinds of systems}
			\vspace{-2mm}
			\begin{itemize}
				\setlength{\itemsep}{2pt}
				\item Labeled Transition Systems ($FX=\powf(A\times X)$)
				\item Kripke frames ($FX=\powf X$)
				\item \textcolor{red}{Operational Semantics of Programming Languages (\emph{Abstract HO-GSOS, and Big-step SOS!})}
				\item Markov Chains ($FX=(\mathcal{D}X)^A$)
				\item Mealy Machines ($FX=(O\times X)^I$)
				\item[$\vdots$]
			\end{itemize}
			\vspace{-1mm}
		\end{alertblock}
		
	\end{columns}
	
\end{frame}

\begin{frame}{Towards Program Equivalence}
	\footnotesize
	We have developed a coalgbera $(T,\gamma)$ that gives the big-step semantics for an arbitrary programming language in a specified family of them, called \emph{abstract HO-GSOS}.
%	\begin{block}{}
%		-$\mS$ is representing terms of a programming language,\\
%		-and $\gamma$ is giving their big-step reduction.
%	\end{block}
	\begin{alertblock}{Main Motivation}
		We want to prove that for terms $t$ and $s$, and a context $C$:\vspace{-0.3cm}
		\begin{gather*}
			t\sim s\Rightarrow C[t]\sim C[s]
		\end{gather*}
	\end{alertblock}\vspace{-0.5cm}
	-In the literature, this is often proved using \emph{Howe's method}. \\
	-The method, applies a closure on the bisimilarity relation on $\mS$.\\
	-Then one should prove that the result is a simulation.\\
	-The closure preserves symmetry, and symmetric simulation is a bisimulation in traditional definitions.\\
	-We have found out that it is not always the case.\\
	-That is why we want to know when exactly a symmetric simulation is a bisimulation.
\end{frame}

\begin{frame}{Relators, Simulations and Bisimulations}
	
	\footnotesize
	
	\begin{columns}[T,onlytextwidth]
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.47\textwidth}
		
		\begin{alertblock}{Relator}
		Assuming $F:\Set\to\Set$ is a functor, an $F$-relator a monotone map that sends a morphism of $\rel$ that is a relation $X\rto Y$ to a relation $FX\rto FY$. 
		\end{alertblock}
		\vspace{-0.3cm}
		\begin{block}{R-Simulation}
			For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if $r\subseteq \beta\comp\relar r\comp\alpha^{-1}$.
		\end{block}
		\vspace{-0.3cm}
		
		\begin{alertblock}{Symmetrization of a Relator}
			Symmetrization of a relator $\relar$ is defined as:
			\begin{gather*}
				\hat{\relar}=\relar r\cap (\relar r^{-1})^{-1}
			\end{gather*}
		\end{alertblock}
		
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.47\textwidth}
		\begin{alertblock}{Symmetric Relator}
			A relator $\relar$ is symmetric if $\relar=\hat{\relar}$
		\end{alertblock}
		\vspace{-0.2cm}
		\begin{block}{R-Bisimulation}
			For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-bisimulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is an $R$-simulation, and $R$ is a symmetric relator.
		\end{block}
		\vspace{-0.2cm}
		\begin{block}{R-Similarity}
			$\relar$-similarity is the greatest $\relar$-simulation.
		\end{block}
		\vspace{-0.3cm}
		\begin{block}{R-Bisimilarity}
			$\relar$-bisimilarity is the greatest $\relar$-bisimulation.
		\end{block}
		
	\end{columns}
	
\end{frame}

\begin{frame}{Some Examples of Relators}
	\footnotesize
	\begin{columns}[T,onlytextwidth]
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.47\textwidth}
		\begin{alertblock}{Example: Trivial Relator}
			For an arbitrary set endofunctor $F$, the relator $\mathbf{Q}$ takes every relation $r:X\rto Y$ to $FX\times FY$.
		\end{alertblock}
		It is a symmetric relator.
		\begin{block}{}
			But it is a bad relator because every relation is a $\mathbf{Q}$-bisimulation!
		\end{block}
		\begin{alertblock}{Example: Egli-Milner Relator}
			The relator $\emre$ is a $\powf$-relator defined as:
			\begin{gather*}
				\emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}
			\end{gather*}
		\end{alertblock}
	
	
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.47\textwidth}
		We give a family of examples:
		\begin{alertblock}{Example: Barr Relators}
			Given a set endofunctor $F$, and $r$ is a relation that $r=\pi_2\comp\pi_1^{-1}$ ($\pi_1$ and $\pi_2$ are functions) the Barr relator $\bar{F}$ is defined as
			$\bar{F}r=\bar{F}\pi_2\comp(\bar{F}\pi_1)^{-1}$.
		\end{alertblock}
		\begin{block}{}
			The symmetrization of the Egli-Milner relator is a Barr relator, i.e.,
			\begin{gather*}
				\hat{\emre}=\bar{\powf}
			\end{gather*}
		\end{block}
		Barr relators are nicely behaved relators.\\ 
		A trivial relator is a not a Barr relator.
\end{columns}
\end{frame}

\begin{frame}{Lax Barr relators}
		\footnotesize
	\begin{columns}[T,onlytextwidth]
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.47\textwidth}
		An ordering of a set endofunctor $F$ is a functor $G$ that commutes in the following diagram:
		\begin{equation*}
			\begin{tikzcd}[ampersand replacement=\&]
				\& \mathbf{PoSet} \& \\
				\Set \&\& \Set
				\arrow["U", from=1-2, to=2-3]
				\arrow["G", from=2-1, to=1-2]
				\arrow["F"', from=2-1, to=2-3]
			\end{tikzcd}
		\end{equation*}
		Meaning that for every $X$, there is a poset $(FX,\appr)$.
		\begin{block}{}
			For example $(\powf X,\subseteq)$ for every set $X$.
		\end{block}
		With orderings we define \emph{lax Barr relators}.\\
		Lax Barr relators are different abstractions of the Egli-Milner relator.
			
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.47\textwidth}
		\begin{block}{}
			There are multiple of them:
			\begin{itemize}
				\item Left-lax: $\appr\comp\bar{F}r$
				\item Right-lax: $\bar{F}\comp\appr$
				\item Bi-lax: $\appr\comp\bar{F}r\comp\appr$
				\item Mid-lax: $F\pi_1\comp\appr\comp(F\pi_2)^{-1}$
			\end{itemize}
		\end{block}
		\begin{alertblock}{Liftability}
			An ordering on a set endofunctor $F$ is called \emph{liftable}, if\vspace{-0.3cm}
			\begin{gather*}
				\alpha\appr\beta\Rightarrow\alpha\comp f\appr \beta\comp f,\\
				\alpha\appr\beta\Rightarrow Ff'\comp\alpha\appr Ff'\comp \beta,\\
				h\appr Fg\comp k\Rightarrow \exists k', h=Fg\comp k\;\&\;k'\appr k.
			\end{gather*}
		\end{alertblock}
	\end{columns}
\end{frame}

\begin{frame}{Lax Barr relators (2)}
	\begin{alertblock}{Proposition}
		Given a set endofunctor $F$, with a liftable ordering 
		\begin{itemize}
			\item mid-lax and left-lax relators of $F$ are equal,
			\item Assuming the axiom of choice, righ-lax and left-lax relators of $F$ are equal,
			\item the symmetrizaion of the left-lax relator is \emph{sound} and \emph{complete} with respect to \emph{behavioural equivalence}.
		\end{itemize}
	\end{alertblock}
\end{frame}

\begin{frame}{Span-based definitions}
	\footnotesize
	\begin{columns}[T,onlytextwidth]
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.47\textwidth}
		\begin{alertblock}{Aczel-Mendler Bisimulation}
			For coalgebras $(X,\alpha)$, and $(Y,\beta)$ a span $(R,X,Y)$ is an \emph{AM-bisimulation}, if there is a \emph{witness} $\gamma$ that commutes in the following:
			\begin{equation*}
				\begin{tikzcd}[ampersand replacement=\&]
					X \& R \& Y \\
					FX \& FR \& FY
					\arrow["\alpha"', from=1-1, to=2-1]
					\arrow["{{p_1}}"', from=1-2, to=1-1]
					\arrow["{{p_2}}", from=1-2, to=1-3]
					\arrow["{{\gamma}}", from=1-2, to=2-2]
					\arrow["\beta", from=1-3, to=2-3]
					\arrow["{Fp_1}", from=2-2, to=2-1]
					\arrow["{Fp_2}"', from=2-2, to=2-3]
				\end{tikzcd}
			\end{equation*}
		\end{alertblock}\vspace{-0.2cm}
		In a \emph{regular category}, if we change $FR$ with $\bar{F}R$ that shows the image of $<Fp_1,Fp_2>$, and the legs of $\bar{F}$ (Barr relator in $\Set$), we have an \emph{Hermida-Jacobs} bisimulation.
		\begin{block}{}\vspace{-0.2cm}
			Every AM-bisimulation is an HJ-bisimulation. 
		\end{block}
		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		\column{.47\textwidth}
		\vspace{0.1cm}
		Assuming the axiom of choice, every HJ-bisimulation is an AM-bisimulation.
		\begin{block}{}
			We have \emph{AM-simulation}, if we lax the diagram:\vspace{-0.4cm}
		\begin{equation*}
			\begin{tikzcd}[ampersand replacement=\&]
				X \& R \& Y \\
				FX \& FR \& FY
				\arrow["\alpha"', from=1-1, to=2-1]
				\arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
				\arrow["{p_1}"', from=1-2, to=1-1]
				\arrow["{p_2}", from=1-2, to=1-3]
				\arrow["\sigma", from=1-2, to=2-2]
				\arrow["\beta", from=1-3, to=2-3]
				\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
				\arrow["{{Fp_1}}", from=2-2, to=2-1]
				\arrow["{{Fp_2}}"', from=2-2, to=2-3]
			\end{tikzcd}
		\end{equation*}
		\end{block}\vspace{-0.3cm}
		We have found a symmetric AM-simulation that is not a bisimulation!
		\begin{alertblock}{Proposition}
			Given a symmetric span $(R,X)$, with the symmetry evidence $s:R\to R$, assuming $R$ is an AM-simulation on a coalgebra $(X,\alpha)$ with evidence $\sigma$, then $R$ is an AM-bisimulation iff $s$ is a coalgebra endomorphism on $(R,\sigma)$.
		\end{alertblock}
	\end{columns}
\end{frame}

\bibliographystyle{apalike}
\bibliography{references}
\addtocounter{framenumber}{-1}
\begin{frame}{\quad}
%	\vspace{-1cm}
	\begin{center}
	\textcolor[rgb]{0.384, 0.384, 0}{\Huge Thank you for your attention! :-)}
	\end{center}
\end{frame}

\end{document}
