liftablity

ACV 2026/Feedback

@@ -0,0 +1,3 @@
+- You should first make a list of the things that you want to talk about before making the slides.
+- If you have a proposition about strong separated HO-GSOS, you should not present it as a proposition about separated HO-GSOS, but with the same result! You were thinking that you can do this because you will get simplicity, but no!
+- You panicked after Filipo said you only have 5 minutes! :)

ACV 2026/README.md

@@ -0,0 +1,93 @@
+# Asraneh and Oberseminar
+
+
+
+## Getting started
+
+To make it easy for you to get started with GitLab, here's a list of recommended next steps.
+
+Already a pro? Just edit this README.md and make it your own. Want to make it easy? [Use the template at the bottom](#editing-this-readme)!
+
+## Add your files
+
+- [ ] [Create](https://docs.gitlab.com/ee/user/project/repository/web_editor.html#create-a-file) or [upload](https://docs.gitlab.com/ee/user/project/repository/web_editor.html#upload-a-file) files
+- [ ] [Add files using the command line](https://docs.gitlab.com/ee/gitlab-basics/add-file.html#add-a-file-using-the-command-line) or push an existing Git repository with the following command:
+
+```
+cd existing_repo
+git remote add origin https://git8.cs.fau.de/le79nide/asraneh-and-oberseminar.git
+git branch -M main
+git push -uf origin main
+```
+
+## Integrate with your tools
+
+- [ ] [Set up project integrations](https://git8.cs.fau.de/le79nide/asraneh-and-oberseminar/-/settings/integrations)
+
+## Collaborate with your team
+
+- [ ] [Invite team members and collaborators](https://docs.gitlab.com/ee/user/project/members/)
+- [ ] [Create a new merge request](https://docs.gitlab.com/ee/user/project/merge_requests/creating_merge_requests.html)
+- [ ] [Automatically close issues from merge requests](https://docs.gitlab.com/ee/user/project/issues/managing_issues.html#closing-issues-automatically)
+- [ ] [Enable merge request approvals](https://docs.gitlab.com/ee/user/project/merge_requests/approvals/)
+- [ ] [Set auto-merge](https://docs.gitlab.com/ee/user/project/merge_requests/merge_when_pipeline_succeeds.html)
+
+## Test and Deploy
+
+Use the built-in continuous integration in GitLab.
+
+- [ ] [Get started with GitLab CI/CD](https://docs.gitlab.com/ee/ci/quick_start/index.html)
+- [ ] [Analyze your code for known vulnerabilities with Static Application Security Testing (SAST)](https://docs.gitlab.com/ee/user/application_security/sast/)
+- [ ] [Deploy to Kubernetes, Amazon EC2, or Amazon ECS using Auto Deploy](https://docs.gitlab.com/ee/topics/autodevops/requirements.html)
+- [ ] [Use pull-based deployments for improved Kubernetes management](https://docs.gitlab.com/ee/user/clusters/agent/)
+- [ ] [Set up protected environments](https://docs.gitlab.com/ee/ci/environments/protected_environments.html)
+
+***
+
+# Editing this README
+
+When you're ready to make this README your own, just edit this file and use the handy template below (or feel free to structure it however you want - this is just a starting point!). Thanks to [makeareadme.com](https://www.makeareadme.com/) for this template.
+
+## Suggestions for a good README
+
+Every project is different, so consider which of these sections apply to yours. The sections used in the template are suggestions for most open source projects. Also keep in mind that while a README can be too long and detailed, too long is better than too short. If you think your README is too long, consider utilizing another form of documentation rather than cutting out information.
+
+## Name
+Choose a self-explaining name for your project.
+
+## Description
+Let people know what your project can do specifically. Provide context and add a link to any reference visitors might be unfamiliar with. A list of Features or a Background subsection can also be added here. If there are alternatives to your project, this is a good place to list differentiating factors.
+
+## Badges
+On some READMEs, you may see small images that convey metadata, such as whether or not all the tests are passing for the project. You can use Shields to add some to your README. Many services also have instructions for adding a badge.
+
+## Visuals
+Depending on what you are making, it can be a good idea to include screenshots or even a video (you'll frequently see GIFs rather than actual videos). Tools like ttygif can help, but check out Asciinema for a more sophisticated method.
+
+## Installation
+Within a particular ecosystem, there may be a common way of installing things, such as using Yarn, NuGet, or Homebrew. However, consider the possibility that whoever is reading your README is a novice and would like more guidance. Listing specific steps helps remove ambiguity and gets people to using your project as quickly as possible. If it only runs in a specific context like a particular programming language version or operating system or has dependencies that have to be installed manually, also add a Requirements subsection.
+
+## Usage
+Use examples liberally, and show the expected output if you can. It's helpful to have inline the smallest example of usage that you can demonstrate, while providing links to more sophisticated examples if they are too long to reasonably include in the README.
+
+## Support
+Tell people where they can go to for help. It can be any combination of an issue tracker, a chat room, an email address, etc.
+
+## Roadmap
+If you have ideas for releases in the future, it is a good idea to list them in the README.
+
+## Contributing
+State if you are open to contributions and what your requirements are for accepting them.
+
+For people who want to make changes to your project, it's helpful to have some documentation on how to get started. Perhaps there is a script that they should run or some environment variables that they need to set. Make these steps explicit. These instructions could also be useful to your future self.
+
+You can also document commands to lint the code or run tests. These steps help to ensure high code quality and reduce the likelihood that the changes inadvertently break something. Having instructions for running tests is especially helpful if it requires external setup, such as starting a Selenium server for testing in a browser.
+
+## Authors and acknowledgment
+Show your appreciation to those who have contributed to the project.
+
+## License
+For open source projects, say how it is licensed.
+
+## Project status
+If you have run out of energy or time for your project, put a note at the top of the README saying that development has slowed down or stopped completely. Someone may choose to fork your project or volunteer to step in as a maintainer or owner, allowing your project to keep going. You can also make an explicit request for maintainers.

ACV 2026/beamercolorthemefocus.sty

@@ -0,0 +1,71 @@
+% Copyright (C) 2018 Pasquale Claudio Africa.
+%               2018 Sebastian Friedl.
+%
+% This file is part of beamerthemefocus.
+%
+% beamerthemefocus is free software: you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation, either version 3 of the License, or
+% (at your option) any later version.
+% 
+% beamerthemefocus is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+% 
+% You should have received a copy of the GNU General Public License
+% along with beamerthemefocus. If not, see <http://www.gnu.org/licenses/>.
+
+\mode<presentation>
+
+
+% DEFINE COLORS. ---------------------------------------------------------------
+\definecolor{main}{RGB}{64, 64, 64}
+\definecolor{background}{RGB}{239, 239, 239}
+
+\definecolor{alert}{RGB}{180, 0, 0}
+\definecolor{example}{RGB}{0, 110, 0}
+
+
+% SET COLORS. ------------------------------------------------------------------
+\setbeamercolor{normal text}{fg=text, bg=background}
+\setbeamercolor{alerted text}{fg=alert}
+\setbeamercolor{example text}{fg=example}
+
+\setbeamercolor{titlelike}{fg=background, bg=main}
+\setbeamercolor{frametitle}{parent={titlelike}}
+
+\setbeamercolor{footline}{fg=background, bg=main}
+
+\setbeamercolor{block title}{bg=main!80!background, fg=background}
+\setbeamercolor{block body}{bg=main!10!background, fg=text}
+
+\setbeamercolor{block title alerted}{bg=alert, fg=background}
+\setbeamercolor{block body alerted}{bg=alert!10!background, fg=text}
+
+\setbeamercolor{block title example}{bg=example, fg=background}
+\setbeamercolor{block body example}{bg=example!10!background, fg=text}
+
+\setbeamercolor{itemize item}{fg=text}
+\setbeamercolor{itemize subitem}{fg=text}
+
+\setbeamercolor{enumerate item}{fg=main!70!black}
+\setbeamercolor{enumerate subitem}{fg=main!70!black}
+
+\setbeamercolor{description item}{fg=main!70!black}
+\setbeamercolor{description subitem}{fg=main!70!black}
+
+\setbeamercolor{caption name}{fg=main}
+
+\setbeamercolor{section in toc}{fg=main}
+\setbeamercolor{subsection in toc}{fg=main}
+\setbeamercolor{section number projected}{bg=main}
+\setbeamercolor{subsection number projected}{bg=main}
+
+\setbeamercolor{bibliography item}{fg=main}
+\setbeamercolor{bibliography entry author}{fg=main!70!black}
+\setbeamercolor{bibliography entry title}{fg=main}
+\setbeamercolor{bibliography entry location}{fg=main}
+\setbeamercolor{bibliography entry note}{fg=main}
+
+\mode<all>

ACV 2026/beamerfontthemefocus.sty

@@ -0,0 +1,47 @@
+% Copyright (C) 2018 Pasquale Claudio Africa.
+%               2018 Sebastian Friedl.
+%
+% This file is part of beamerthemefocus.
+%
+% beamerthemefocus is free software: you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation, either version 3 of the License, or
+% (at your option) any later version.
+% 
+% beamerthemefocus is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+% 
+% You should have received a copy of the GNU General Public License
+% along with beamerthemefocus. If not, see <http://www.gnu.org/licenses/>.
+
+\mode<presentation>
+
+
+% SET FONTS. -------------------------------------------------------------------
+\setbeamerfont{title}{size=\huge, shape=\scshape\bfseries}
+\setbeamerfont{subtitle}{size=\Large, shape=\scshape, parent=structure}
+\setbeamerfont{author}{size=\large, shape=\upshape}
+
+\setbeamerfont{institute}{size=\normalsize, shape=\scshape}
+\setbeamerfont{date}{size=\small, shape=\scshape}
+
+\setbeamerfont{sectiontitle}{size=\huge, series=\scshape\bfseries}
+\setbeamerfont{frametitle}{size=\Large, shape=\scshape}
+
+\setbeamerfont{footline}{size=\scriptsize}
+
+\setbeamerfont{focusframe}{size=\huge, shape=\scshape}
+
+\setbeamerfont{description item}{shape=\bfseries}
+
+\setbeamerfont{caption name}{shape=\bfseries}
+
+\setbeamerfont{bibliography item}{size=\small, shape=\scshape}
+\setbeamerfont{bibliography entry author}{size=\small, shape=\scshape}
+\setbeamerfont{bibliography entry title}{size=\small, series=\scshape\bfseries}
+\setbeamerfont{bibliography entry location}{size=\small, shape=\scshape\normalfont}
+\setbeamerfont{bibliography entry note}{size=\small, shape=\scshape\normalfont}
+
+\mode<all>

ACV 2026/beamerinnerthemefocus.sty

@@ -0,0 +1,110 @@
+% Copyright (C) 2018 Pasquale Claudio Africa.
+%               2018 Sebastian Friedl.
+%
+% This file is part of beamerthemefocus.
+%
+% beamerthemefocus is free software: you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation, either version 3 of the License, or
+% (at your option) any later version.
+% 
+% beamerthemefocus is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+% 
+% You should have received a copy of the GNU General Public License
+% along with beamerthemefocus. If not, see <http://www.gnu.org/licenses/>.
+
+\mode<presentation>
+
+\RequirePackage{tikz}
+
+
+% CUSTOMIZE STRUCTURE ELEMENTS. ------------------------------------------------
+\setbeamertemplate{blocks}[default]
+
+\setbeamertemplate{section in toc}[square]
+\setbeamertemplate{subsection in toc}[square]
+
+\setbeamertemplate{itemize items}[square]
+\setbeamertemplate{itemize subitem}[triangle]
+
+
+% STRUCTURE FRAME TEMPLATE DEFINITIONS. ----------------------------------------
+% Title page.
+\defbeamertemplate*{title page}{focus}{%
+    {\usebeamercolor{frametitle}\colorlet{focus@@temp}{bg}%
+        \begin{tikzpicture}[overlay, remember picture]
+            \fill[color=focus@@temp] (current page.north west) rectangle ([shift = {(0, -0.45\paperheight)}] current page.north east);
+        \end{tikzpicture}}
+    
+    \vspace{-1.65\baselineskip}
+    \begin{minipage}[b][0.35\paperheight]{\textwidth}
+        \vspace{\baselineskip}
+        \usebeamerfont{title}
+        \usebeamercolor[fg]{frametitle}
+        \inserttitle
+    \end{minipage}
+    
+    \begin{minipage}[t][0.1\paperheight]{\textwidth}
+        \usebeamerfont{subtitle}
+        \usebeamercolor[fg]{frametitle}
+        \insertsubtitle
+    \end{minipage}
+    
+    % Set the title graphic in a zero-height box, so that
+    % the position of other elements is not affected.
+    {\vfuzz=9999pt\vbox to 0pt {
+        \raggedleft
+        \inserttitlegraphic
+    }}
+    
+    \begin{minipage}[t]{\textwidth}
+        \usebeamerfont{author}
+        \insertauthor
+    \end{minipage}
+    
+    \vspace*{\baselineskip}
+    \begin{minipage}[t]{\textwidth}
+        \usebeamerfont{institute}
+        \insertinstitute
+    \end{minipage}
+    
+    \vspace*{\baselineskip}
+    \begin{minipage}[t]{\textwidth}
+        \usebeamerfont{date}{\insertdate}
+    \end{minipage}
+    
+    \vspace*{5\baselineskip}
+    
+    \addtocounter{framenumber}{-1}
+}
+
+% Section page.
+\defbeamertemplate*{section page}{focus}{%
+    {%
+        \usebeamercolor{frametitle}\colorlet{focus@@temp}{bg}%
+        \begin{tikzpicture}[overlay, remember picture]
+            \fill[color=focus@@temp] (current page.north west) rectangle ([shift = {(0, -0.45\paperheight)}] current page.north east);
+        \end{tikzpicture}%
+    }
+    
+    \vspace{-2\baselineskip}
+    \begin{minipage}[b][0.45\paperheight]{\textwidth}
+        \usebeamerfont{sectiontitle}
+        \usebeamercolor[fg]{frametitle}
+        \let\hyperlink\@secondoftwo\insertsection
+    \end{minipage}
+    
+    \begin{minipage}[t][0.55\paperheight]{\textwidth}
+    \end{minipage}
+}
+
+\AtBeginSection{%
+    \begin{frame}[plain, noframenumbering]{}
+        \sectionpage
+    \end{frame}%
+}
+
+\mode<all>

ACV 2026/beamerouterthemefocus.sty

@@ -0,0 +1,255 @@
+% Copyright (C) 2018 Pasquale Claudio Africa.
+%               2018 Sebastian Friedl.
+%
+% This file is part of beamerthemefocus.
+%
+% beamerthemefocus is free software: you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation, either version 3 of the License, or
+% (at your option) any later version.
+% 
+% beamerthemefocus is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+% 
+% You should have received a copy of the GNU General Public License
+% along with beamerthemefocus. If not, see <http://www.gnu.org/licenses/>.
+
+\mode<presentation>
+
+\RequirePackage{appendixnumberbeamer}% Don't number appendix frames.
+\RequirePackage{etoolbox}% \BeforeBeginEnvironment
+\RequirePackage{tikz}
+
+
+% FRAMETITLE TEMPLATES. --------------------------------------------------------
+\defbeamertemplate*{frametitle}{focus}{%
+    % If not title page.
+    \ifnum\value{framenumber}>0%
+        \vspace{-1pt}%
+        \begin{beamercolorbox}[wd=\paperwidth,leftskip=0.55cm,rightskip=0.55cm,sep=0.2cm]{frametitle}%
+            \strut\insertframetitle\strut%
+        \end{beamercolorbox}%
+    \fi%
+}
+
+% Plain header.
+\defbeamertemplate{frametitle}{plain}{%
+    % If not title page.
+    \ifnum\value{framenumber}>0%
+        \vspace{-1pt}%
+        \begin{beamercolorbox}[wd=\paperwidth,leftskip=0.55cm,rightskip=0.55cm,sep=0.2cm,ignorebg]{frametitle}%
+            \strut%
+        \end{beamercolorbox}%
+    \fi%
+}
+
+
+% FOOTLINE TEMPLATES. ----------------------------------------------------------
+% Lenghts for the progress bar footline.
+\newlength{\focus@pbar@height}% Progress bar height.
+\newlength{\focus@pbar@leftoffset}
+\newlength{\focus@pbar@rightoffset}
+
+\defbeamertemplate*{footline}{progressbar}{%
+    % If not appendix.
+    \ifnum\mainend<0% From package appendixnumberbeamer.
+        %
+        \settowidth{\focus@pbar@leftoffset}{1}%
+        \addtolength{\focus@pbar@leftoffset}{1.5em}%
+        %
+        \settowidth{\focus@pbar@rightoffset}{\inserttotalframenumber}%
+        \addtolength{\focus@pbar@rightoffset}{1.5em}%
+        %
+        % If not title page.
+        \ifnum\c@framenumber>0%
+            \ifnum\c@framenumber<\inserttotalframenumber%
+                \begin{tikzpicture}[inner xsep=0.5em, inner ysep=0.5ex]\usebeamerfont{footline}
+                    \pgfmathsetmacro{\focus@pbar@progress}%
+                        {(\paperwidth-\focus@pbar@leftoffset-\focus@pbar@rightoffset)*(\insertframenumber/\inserttotalframenumber)}
+                
+                    \clip (0,0) rectangle ++(\paperwidth,\the\focus@pbar@height);
+                    \fill[footline.bg] (0,0) rectangle ++(\the\focus@pbar@leftoffset,\the\focus@pbar@height);
+                    
+                    \fill[footline.bg] (\the\focus@pbar@leftoffset,0) rectangle ++(\focus@pbar@progress pt,\the\focus@pbar@height)
+                                       ++(0,{-0.5*\the\focus@pbar@height}) node[anchor=east, text=footline.fg] {\strut\insertframenumber};
+                    
+                    \fill[footline.bg] (\paperwidth,0) rectangle ++(-\the\focus@pbar@rightoffset,\the\focus@pbar@height)
+                                       ++(0,{-0.5*\the\focus@pbar@height}) node[anchor=west, text=footline.fg] {\strut\inserttotalframenumber};
+                \end{tikzpicture}%
+            \else%
+                \begin{tikzpicture}[inner xsep=0.5em, inner ysep=0.5ex]
+                    \clip (0,0) rectangle ++(\paperwidth,\the\focus@pbar@height);
+                    \fill[footline.bg] (0,0) rectangle ++(\paperwidth,\the\focus@pbar@height);
+                    
+                    \node[anchor=east, footline.fg] at ({\paperwidth-\the\focus@pbar@rightoffset},{0.5*\focus@pbar@height}) {\strut\insertframenumber};
+                    \node[footline.fg] at ({\paperwidth-\the\focus@pbar@rightoffset},{0.5*\focus@pbar@height}) {\strut/};
+                    \node[anchor=west, footline.fg] at ({\paperwidth-\the\focus@pbar@rightoffset},{0.5*\focus@pbar@height}) {\strut\inserttotalframenumber};
+                \end{tikzpicture}%
+            \fi%
+        \fi%
+    \fi%
+}
+
+% Full bar footline.
+\defbeamertemplate{footline}{fullbar}{%
+    % If not appendix.
+    \ifnum\mainend<0% From package appendixnumberbeamer.
+        %
+        \settowidth{\focus@pbar@leftoffset}{1}%
+        \addtolength{\focus@pbar@leftoffset}{1.5em}%
+        %
+        \settowidth{\focus@pbar@rightoffset}{\inserttotalframenumber}%
+        \addtolength{\focus@pbar@rightoffset}{1.5em}%
+        %
+        % If not title page.
+        \ifnum\c@framenumber>0%
+            \begin{tikzpicture}[inner xsep=0.5em, inner ysep=0.5ex]
+                \clip (0,0) rectangle ++(\paperwidth,\the\focus@pbar@height);
+                \fill[footline.bg] (0,0) rectangle ++(\paperwidth,\the\focus@pbar@height);
+                
+                \node[anchor=east, footline.fg] at ({\paperwidth-\the\focus@pbar@rightoffset},{0.5*\focus@pbar@height}) {\strut\insertframenumber};
+                \node[footline.fg] at ({\paperwidth-\the\focus@pbar@rightoffset},{0.5*\focus@pbar@height}) {\strut/};
+                \node[anchor=west, footline.fg] at ({\paperwidth-\the\focus@pbar@rightoffset},{0.5*\focus@pbar@height}) {\strut\inserttotalframenumber};
+            \end{tikzpicture}%
+        \fi%
+    \fi%
+}
+
+% Empty footline.
+\defbeamertemplate{footline}{none}{}
+
+\DeclareOptionBeamer{numbering}{\def\beamer@focus@numbering{#1}}
+\ExecuteOptionsBeamer{numbering=progressbar}
+\ProcessOptionsBeamer
+
+\def\beamer@focus@numberingprogressbar{progressbar}
+\def\beamer@focus@numberingfullbar{fullbar}
+\def\beamer@focus@numberingnone{none}
+
+
+% BACKGROUND CANVAS TEMPLATES. -------------------------------------------------
+\defbeamertemplate*{background canvas}{focus}{%
+    \begin{tikzpicture}
+        \clip (0,0) rectangle ++(\paperwidth,\paperheight);
+        \fill[normal text.bg] (0,0) rectangle ++(\paperwidth,\paperheight);
+    \end{tikzpicture}%
+}
+
+\defbeamertemplate{background canvas}{focusplain}{%
+    \begin{tikzpicture}
+        \clip (0,0) rectangle ++(\paperwidth,\paperheight);
+        \fill[normal text.bg] (0,0) rectangle ++(\paperwidth,\paperheight);
+    \end{tikzpicture}%
+}
+
+\defbeamertemplate{background canvas}{focusframe}{%
+    \begin{tikzpicture}
+        \clip (0,0) rectangle ++(\paperwidth,\paperheight);
+        \fill[frametitle.bg] (0,0) rectangle ++(\paperwidth,\paperheight);        
+    \end{tikzpicture}%
+}
+
+
+% HOOKS FOR CREATING FRAMES. ---------------------------------------------------
+\BeforeBeginEnvironment{frame}{%
+    \setbeamertemplate{background canvas}[focus]%
+    \setbeamertemplate{frametitle}[focus]%
+    %
+    % Reset footline height and determine it for the current slide.
+    \setlength{\focus@pbar@height}{0cm}%
+    \focus@calculatefootheight%
+    %
+    % If not appendix.
+    \ifnum\mainend<0 % From package appendixnumberbeamer.
+        \settoheight{\focus@pbar@height}{\usebeamerfont{footline}1234567890/}%
+        \addtolength{\focus@pbar@height}{6pt}%
+        %
+        \ifx\beamer@focus@numbering\beamer@focus@numberingprogressbar%
+            \setbeamertemplate{footline}[progressbar]%
+        \else%
+            \ifx\beamer@focus@numbering\beamer@focus@numberingfullbar%
+                \setbeamertemplate{footline}[fullbar]%
+            \fi%
+        \fi%
+        %
+        \focus@calculatefootheight%
+    \fi%
+}
+
+% Enable noframenumbering option.
+\define@key{beamerframe}{noframenumbering}[true]{%
+    \setbeamertemplate{footline}[none]%
+    \setlength{\focus@pbar@height}{0cm}%
+    \focus@calculatefootheight%
+    %
+    \addtocounter{framenumber}{-1}%
+}
+
+
+% Enable plain option.
+\define@key{beamerframe}{plain}[true]{%
+    \setbeamertemplate{background canvas}[focusplain]%
+    \setbeamertemplate{frametitle}[plain]%
+    %
+    \setbeamertemplate{footline}[none]%
+}
+
+
+% Full vertical centering
+% (from https://tex.stackexchange.com/questions/247826/beamer-full-vertical-centering).
+\define@key{beamerframe}{c}[true]{%
+    \beamer@frametopskip=0pt plus 1fill\relax%
+    \beamer@framebottomskip=0pt plus 1fill\relax%
+    \beamer@frametopskipautobreak=0pt plus 0.4\paperheight\relax%
+    \beamer@framebottomskipautobreak=0pt plus 0.6\paperheight\relax%
+    \def\beamer@initfirstlineunskip{}%
+}
+
+
+% Enable focus option.
+\providebool{focus@standout}
+\define@key{beamerframe}{focus}[true]{%
+    \booltrue{focus@standout}%
+    \begingroup%
+        \setkeys{beamerframe}{noframenumbering}%
+        \setbeamertemplate{background canvas}[focusframe]%
+        \setbeamertemplate{frametitle}[plain]%
+        %
+        \setkeys{beamerframe}{c}%
+        \centering%
+        \usebeamerfont{focusframe}%
+        \usebeamercolor[fg]{frametitle}%
+}
+
+\apptocmd{\beamer@reseteecodes}
+{%
+    \ifbool{focus@standout}%
+    {%
+        \endgroup%
+        \boolfalse{focus@standout}%
+    }{}%
+}{}{}
+
+
+% Recalculate the footline's size and refresh other parameters.
+% Partially copied from the definition of \beamer@calculateheadfoot.
+\def\focus@calculatefootheight{%
+    \footheight=\focus@pbar@height%
+    \advance\footheight by 4pt%
+    \sidebarheight=\paperheight%
+    \advance\sidebarheight by-\headheight%
+    \advance\sidebarheight by\headdp%
+    \advance\sidebarheight by-\footheight%
+    \advance\sidebarheight by 4pt%
+    \footskip=\footheight%
+    \textheight=\paperheight%
+    \advance\textheight by-\footheight%
+    \advance\textheight by-\headheight%
+    \@colht\textheight%
+    \@colroom\textheight%
+    \vsize\textheight%
+}
+
+\mode<all>

ACV 2026/beamerthemefocus.sty

@@ -0,0 +1,60 @@
+% Copyright (C) 2018 Pasquale Claudio Africa.
+%               2018 Sebastian Friedl.
+%
+% This file is part of beamerthemefocus.
+%
+% beamerthemefocus is free software: you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation, either version 3 of the License, or
+% (at your option) any later version.
+% 
+% beamerthemefocus is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+% 
+% You should have received a copy of the GNU General Public License
+% along with beamerthemefocus. If not, see <http://www.gnu.org/licenses/>.
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{beamerthemefocus}[2018/07/15 v2.0 Focus Beamer theme]
+
+\mode<presentation>
+
+
+% THEME OPTIONS. ---------------------------------------------------------------
+\DeclareOptionBeamer{numbering}{%
+    \PassOptionsToPackage{numbering=#1}{beamerouterthemefocus}
+}
+
+\newif\if@focus@loadfirafonts
+\@focus@loadfirafontstrue
+
+\DeclareOptionBeamer{nofirafonts}{\@focus@loadfirafontsfalse}
+\ProcessOptionsBeamer
+
+
+% LOAD EXTERNAL PACKAGES. ------------------------------------------------------
+\if@focus@loadfirafonts
+    \RequirePackage[T1]{fontenc}
+    
+    \PassOptionsToPackage{type1}{FiraSans}
+    \PassOptionsToPackage{type1}{FiraMono}
+    
+     \RequirePackage{FiraSans}
+     \RequirePackage{FiraMono}
+\fi
+
+\usecolortheme{focus}
+\usefonttheme{focus}
+\useinnertheme{focus}
+\useoutertheme{focus}
+
+\setbeamertemplate{navigation symbols}{}
+
+
+% SET MARGINS. -----------------------------------------------------------------
+\setbeamersize{text margin left=0.75cm, text margin right=0.75cm}
+\setlength{\leftmargini}{0.75cm}
+
+\mode<all>

ACV 2026/references.bib

@@ -0,0 +1,110 @@
+@article{amir,
+  title     = {Implication via Spacetime},
+  author    = {Tabatabai, Amirhossein Akbar},
+  journal   = {Mathematics, Logic, and Their Philosophies: Essays in Honour of Mohammad Ardeshir},
+  volume    = {49},
+  pages     = {161},
+  year      = {2021},
+  publisher = {Springer Nature}
+}
+
+@phdthesis{ardeshir1995aspects,
+  title  = {Aspects of basic logic},
+  author = {Ardeshir, Mohammad},
+  year   = {1995},
+  school = {Marquette University}
+}
+
+@article{celani2001closer,
+  title     = {A closer look at some subintuitionistic logics},
+  author    = {Celani, Sergio and Jansana, Ramon},
+  journal   = {Notre Dame Journal of Formal Logic},
+  volume    = {42},
+  number    = {4},
+  pages     = {225--255},
+  year      = {2001},
+  publisher = {Duke University Press}
+}
+
+@incollection{DBLP:books/ox/07/Feferman07,
+  author    = {Solomon Feferman},
+  editor    = {Stewart Shapiro},
+  title     = {Predicativity},
+  booktitle = {The Oxford Handbook of Philosophy of Mathematics and Logic},
+  series    = {Oxford handbooks in philosophy},
+  pages     = {590--624},
+  publisher = {Oxford University Press},
+  year      = {2007},
+  timestamp = {Wed, 06 May 2020 15:26:14 +0200},
+  biburl    = {https://dblp.org/rec/books/ox/07/Feferman07.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@incollection{dovsen1993modal,
+  title     = {Modal translations in K and D},
+  author    = {Do{\v{s}}en, Kosta},
+  booktitle = {Diamonds and defaults},
+  pages     = {103--127},
+  year      = {1993},
+  publisher = {Springer}
+}
+
+@article{feferman2007predicativity,
+  title     = {Predicativity},
+  author    = {Feferman, Solomon},
+  year      = {2007},
+  publisher = {Citeseer}
+}
+
+@incollection{Kennedy2009-KENOGL,
+  editor    = {Dov Gabbay},
+  title     = {On {G}\"odel's Logic},
+  year      = {2009},
+  author    = {Juliette Kennedy and Mark van Atten},
+  booktitle = {The Handbook of the History of Logic},
+  publisher = {Elsevier}
+}
+
+@article{mckinsey1944algebra,
+  title     = {The algebra of topology},
+  author    = {McKinsey, John Charles Chenoweth and Tarski, Alfred},
+  journal   = {Annals of mathematics},
+  pages     = {141--191},
+  year      = {1944},
+  publisher = {JSTOR}
+}
+
+@article{tabatabai2017geometric,
+  title   = {Geometric modality and weak exponentials},
+  author  = {Tabatabai, Amirhossein Akbar},
+  journal = {arXiv preprint arXiv:1711.01736},
+  year    = {2017}
+}
+
+@article{van2001,
+  title     = {Intuitionistic Logic},
+  author    = {Dirk van Dalen},
+  journal   = {The Blackwell Guide to Philosophica Logic},
+  editor    = {L. Gobble. Blackwell},
+  publisher = {Blackwell},
+  year      = {2001},
+  pages     = {224–257}
+}
+
+@article{van2017predicativity,
+  title   = {Predicativity and parametric polymorphism of Brouwerian implication},
+  author  = {van Atten, Mark},
+  journal = {arXiv preprint arXiv:1710.07704},
+  year    = {2017}
+}
+
+@article{russell1908mathematical,
+  title={Mathematical logic as based on the theory of types},
+  author={Russell, Bertrand},
+  journal={American journal of mathematics},
+  volume={30},
+  number={3},
+  pages={222--262},
+  year={1908},
+  publisher={JSTOR}
+}

ACV 2026/slides.tex

@@ -0,0 +1,755 @@
+\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 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, for example:\vspace{-0.4cm}
+	\begin{itemize}
+		\setlength{\itemsep}{6pt}
+		\item[\faServer] \textbf{Hardware redesign.} A chip redesigned for a cheaper price 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 point}
+		``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}
+			
+			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.\\
+			Bisimilarity is defined similarly, where $R$ is a bisimulation, and it is shown with $\sim$.
+%			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 $T$.\\
+	-Then one should prove that the result is a simulation.\\
+	-The closure preserves symmetry, and symmetric simulation is a bisimulation in traditional definitions.\\
+	-We need to know how to generally derive bisimulation from simulation.\\
+	-And what is the impact of choosing specific notion of simulation (span-based, relation-based)?
+\end{frame}
+
+\begin{frame}{Relators and Simulations}
+	
+	\footnotesize
+	
+	\begin{columns}[T,onlytextwidth]
+		
+		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+		\column{.47\textwidth}
+		Relators unify simulation and bisimulation.
+		\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}
+\begin{block}{R-Similarity}
+	$\relar$-similarity is the greatest $\relar$-simulation.
+\end{block}
+		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+		\column{.47\textwidth}
+		\begin{alertblock}{Example: Trivial Relator}
+			For an arbitrary set endofunctor $F$, the relator $\mathbf{K}$ takes every relation $r:X\rto Y$ to $FX\times FY$.
+		\end{alertblock}\vspace{-0.2cm}
+%		\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}
+		\begin{block}{}
+			But it is a bad relator because every relation is a $\mathbf{K}$-bisimulation!
+		\end{block}
+		\begin{alertblock}{Example: Egli-Milner Relator}
+			The relator $\emre$ is a $\powf$-relator defined as:\vspace{-0.2cm}
+			\begin{gather*}
+				\emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}
+			\end{gather*}
+		\end{alertblock}\vspace{-0.2cm}
+		\begin{block}{}
+			It gives us the traditional definition for simulation on Kripke frames.
+		\end{block}
+	\end{columns}
+	
+\end{frame}
+
+\begin{frame}{Symmetric Relators}
+%	\footnotesize
+	
+%	\begin{columns}[T,onlytextwidth]
+		
+		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%		\column{.47\textwidth}
+		\begin{block}{$R$-bisimulation ($R$-bisimularity)}
+			An $\relar$-simulation (similarity) is a bisimulation (bisimilarity), if $\relar$ is \emph{symmetric}.
+		\end{block}
+				\begin{alertblock}{Symmetrization of a Relator}
+						Symmetrization of a relator $\relar$ is defined as:
+						\begin{gather*}
+								\hat{\relar}r=\relar r\cap (\relar r^{-1})^{-1}
+							\end{gather*}
+				\end{alertblock}
+						\begin{block}{Symmetric Relators}
+					A relator $\relar$ is symmetric if $\relar=\hat{\relar}$
+				\end{block}\vspace{-0.5cm}
+			Egli-Milner is not symmetric.
+		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%		\column{.47\textwidth}
+%	\end{columns}
+\end{frame}
+
+\begin{frame}{Barr 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}
+		\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}\vspace{-0.5cm}
+		Barr relators are nicely behaved relators.
+%		A trivial relator is a not a Barr relator.
+		\begin{block}{}
+			So, we always have bisimulations with Barr relators.
+		\end{block}
+%\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}{}
+			\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}\vspace{-0.2cm}
+		\begin{alertblock}{Liftability}
+			An ordering on a set endofunctor $F$ is called \emph{liftable}, if\vspace{-0.3cm}
+			\begin{gather*}
+				h\appr Fg\comp k\Rightarrow \exists k', h=Fg\comp k\;\&\;k'\appr k.
+			\end{gather*}
+		\end{alertblock}\vspace{-0.2cm}
+		An ordering and liftablity can be defined for an arbitrary category as well.
+	\end{columns}
+\end{frame}
+
+\begin{frame}{Symmetrization of Lax Barr relators}
+	\footnotesize
+	Having liftability allows us for an arbitrary function $g$ to have:\vspace{-0.2cm}
+\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			FX \& FX \\
+			FY \& FY
+			\arrow["{\appr_X}"{inner sep=.8ex}, "\shortmid"{marking}, tail, from=1-1, to=1-2]
+			\arrow["Fg"', from=1-1, to=2-1]
+			\arrow["Fg", from=1-2, to=2-2]
+			\arrow["{\appr_Y}"'{inner sep=.8ex}, "\shortmid"{marking}, tail, from=2-1, to=2-2]
+		\end{tikzcd}
+\end{equation*}\vspace{-0.3cm}
+%	\begin{gather*}
+%		Fg\comp\appr=\appr\comp Fg\\
+%		(Fg)^{-1}\comp\sappr=\sappr\comp(Fg)^{-1}
+%	\end{gather*}
+	\begin{alertblock}{Proposition}
+		Given a set endofunctor $F$, with a liftable ordering 
+		\begin{enumerate}
+			\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{enumerate}
+	\end{alertblock}
+	\vspace{-0.1cm}
+	\begin{block}{}
+		\begin{itemize}
+		\item Although, not every sound and complete relator is a Barr relator!\\
+		\item We do not know when Clause 3 does not produce a Barr relator.
+	\end{itemize}
+	\end{block}
+\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.2cm}
+		\begin{alertblock}{AM-Simulation}
+			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{alertblock}\vspace{-0.2cm}
+		\begin{block}{}
+			\begin{itemize}
+				\item Every AM-(bi)simulation is an HJ-(bi)simulation.
+				\item Assuming AoC every HJ-bisimulation is an AM-bisimulation.
+				\item Every HJ-bisimulation for a functor of form $\powf F$ in a topos is an AM-bisimulation.
+			\end{itemize}
+		\end{block}
+	\end{columns}
+\end{frame}
+
+\begin{frame}{Symmetric Simulation for Span-based Definitions}
+	\footnotesize
+	So far we have:
+	\begin{block}{}
+		\begin{itemize}
+			\item An example of an AM(HJ)-simulation that is not an AM(HJ)-bisimulation.
+			\item An example of an AM(HJ)-simulation that the witness for AM(HJ)-simulation does not serve as a witness for AM(HJ)-bisimulation for a $\powf$-coalgebra in $\Set$.
+		\end{itemize}
+	\end{block}
+	\begin{alertblock}{Proposition}
+		Given a symmetric span $(R,X)$, with the symmetry witness $s:R\to R$, assuming $R$ is an HJ-simulation on a coalgebra $(X,\alpha)$ with witness $\sigma$, then $R$ is an AM-bisimulation iff $s$ is a coalgebra endomorphism on $(R,\sigma)$.
+	\end{alertblock}
+	\begin{block}{}
+		\begin{itemize}
+			\item We have a proof that symmetric AM-simulations for coalgebras of $\powf$ and the maybe fucntor on $\Set$ are AM-bisimulation.
+			\item We want to know when exactly this proposition holds (perhaps liftability matters).
+		\end{itemize}
+	\end{block}
+\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}

ACV 2026/speech.tex

@@ -0,0 +1,33 @@
+\documentclass{paper}
+\pagestyle{empty}
+\begin{document}
+
+\setcounter{section}{-1}
+\section{Greetings}
+\section{Agenda}
+\begin{itemize}
+  \item Three parts:
+    \begin{enumerate}
+      \item What I know:
+        \begin{itemize}
+          \item Impredicativity
+          \item in logic: BHK
+        \end{itemize}
+      \item What has been done:
+        \begin{itemize}
+          \item An idea to avoid impredicative implication
+          \item Construct a logical system with this idea
+          \item There are well-behaved algebraic models for this system.
+        \end{itemize}
+      \item What we're going to do:
+        \begin{itemize}
+          \item Analiticity and the problem of $cut$
+          \item Introduce a new analytic system
+          \item what we hope to achive
+        \end{itemize}
+    \end{enumerate}
+\end{itemize}
+\part{Impredicativity}
+\section{What is impredicativity?}
+\textbullet We know impredicative definitions are 
+\end{document}

draft/draft.tex

@@ -292,7 +292,9 @@
 \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{\powf}{\mathcal{P}}
+\newcommand{\powfi}{\mathcal{P}_{\mathsf{inj}}}
 \newcommand{\sappr}{\sqsupseteq}
+\newcommand{\Dom}{\mathsf{Dom}}
 
 \newcommand{\simeet}{%
 	\mathbin{%
@@ -302,6 +304,7 @@
 		}%
 	}%
 }
+\newcommand{\sub}{\mathcal{S}}
 
 
 \newcommand{\bba}{
@@ -401,6 +404,130 @@ We want to say that a natural order structure entails an order over a functor de
 \begin{proof}
 	We take $\tilde{F}X=\Hom(1,FX)$. Assuming that $U$ takes every poset to its carrier set, then we have $U\comp\tilde{F}X=FX$ for every object $X$.\qed
 \end{proof}
+
+\begin{definition}[Liftable Order Structure]\label{def:liftable-ord}
+	A \emph{liftable 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}[Coliftable Order Structure]\label{def:coliftable-ord}
+	A \emph{coliftable 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)$, and $g$ is surjective, 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}\label{lem:set-ord-str}
+	In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a liftable order structure. 
+\end{lemma}
+\begin{proof}
+	For every $f,g\in\Hom(X,FY)$, we define $f\appr g$ whenever for all $x\in X$, $f(x)\leq g(x)$.
+	
+	Now, assuming $f\c X'\to X$, $\alpha,\beta\c X\to FY$, and $\alpha\appr\beta$, then for every $x'\in X'$, we have $\alpha(f(x'))\leq\beta(f(x'))$, so we have $\alpha\comp f\appr \beta\comp f$. Additionally, if we assume $g\c Y\to Y'$, then since $\leq$ satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, for every $x\in X$ we have $Fg\comp\alpha(x)\leq Fg\comp\beta(x)$.
+	
+	Furthermore, if we have $g\c Y\to Z$, $k\c X\to FY$, $h\c X\to FZ$, and $Fg\comp k\appr h$, then for every $x\in X$ we have $Fg\comp k(x)\leq h(x)$, thus by the assumption of the lemma, for every $x$, there exists a set that we call $k'(x)$, for which we have $Fg(k'(x))\leq h(x)$. So, we have a function $k'\c X\to FY$, such that for every $x$ we have $Fg\comp k'(x)\leq h(x)$ that means $Fg\comp k'\appr h$.
+	\qed
+\end{proof}
+\begin{remark}\label{rem:set-ord-str-co}
+	The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures.
+\end{remark}
+
+\begin{prop}\label{prop:lift-gen-func}
+	For a functor $F\c\Set\to\Set$, a functor of the form $\powf F$, where $\powf$ is the powerset functor, the set inclusion is a liftable order structure. 
+\end{prop}
+\begin{proof}
+	Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf FZ)$, $k\in\Hom(1,\powf FY)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf Fg(k)$, we define $k'\in\powf FY$ that that $k'=\{y\mid Fg(y)\in h\}$. We show that $k'\subseteq k$ and $\powf Fg(k')=h$.
+	
+	Assuming $y\in k'$ we have $Fg(y)\in h$. Since $h\subseteq \powf Fg(k)$ we have $Fg(y)\in\powf Fg(k)$, so we have $y\in k$ that means $k'\subseteq k$.
+	
+	Assuming $z\in\powf Fg(k')$, then there exists $y'\in k'$ that $z=Fg(y')$, so $z\in h$ and $\powf Fg(k')\subseteq h$.
+	
+	Assuming $z\in h$, since $h\subseteq \powf Fg(k)$, then $z\in\powf Fg(k)$. So, there exists $y'\in k$ such that $Fg(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means  $z\in\powf Fg(k')$.\qed
+\end{proof}
+
+\begin{example}
+	In the category of sets, subset over the powerset functor is an example of a coliftable order structure if the $g$ in~\autoref{def:coliftable-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$.
+	
+	Obviously, $\powf g(k')\subseteq h$. Now, assuming $z\in h$ we prove that $z\in \powf g(k')$. Since $g$ is surjective, then exists $A\subseteq Y$ such that $\powf g(A)=h$. By the definition of $k'$, $A\subseteq k'$. So from $z\in h$ we have $z\in \powf g(A)$ that means that exists $a\in A$, such that $g(a)=z$. Now, since $A\subseteq k'$, then $a\in k'$. So, we have $z\in \powf g(k')$.\qed
+\end{example}
+
+\begin{remark}
+	We give an example that justifies why the $g$ in~\autoref{def:coliftable-ord} should be surjective.
+	If we take the surjectivity of $g$ out of~\autoref{def:coliftable-ord}, subset relation over the powerset functor is not an example of a coliftable order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$, 
+	\begin{gather*}
+		g(z)=
+		\begin{cases} 
+			0 & z\in\mathbb{Z}^+ \\
+			1 & \mathsf{otherwise}  
+		\end{cases}
+	\end{gather*}
+	then 
+	\begin{gather*}
+		\powf g(A)=
+		\begin{cases} 
+			\emptyset & A=\emptyset \\
+			\{0\} & A\subseteq \mathbb{Z}^+,A\neq\emptyset\\  
+			\{1\} & A\subseteq \mathbb{Z}^-\cup\{0\},A\neq\emptyset\\
+			\{0,1\} & \mathsf{otherwise} 
+		\end{cases}
+	\end{gather*}
+	then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$.
+\end{remark}
+
+\begin{remark}
+	We could not prove a general statement like~\autoref{prop:lift-gen-func} for coliftability even if the surgectivity of $g$ remains in the definition. Perhaps more conditions on $F$ in~\autoref{prop:lift-gen-func} are needed. Conditions like preserving surjections and unions that make the statement extremely limited, and meaningless.
+\end{remark}
+
+\begin{example}
+	The subdistribution functor $\sub\c\Set\to\Set$ is defined as $\sub X=\{\mu\c X\to[0,1]\mid \sum_{x\in X}\mu(x)\}$ on objects, and for $\sub f\c \sub X\to\sub Y$, we have 
+	\begin{gather*}
+	\sub f(\mu)=y\mapsto\sum_{x\in f^{\mone}(y)}\mu(x),
+	\end{gather*}
+	on morphisms. We define the ordering on $\sub X$ for $\mu_1,\mu_2\in \sub X$ as
+	\begin{gather*}
+		\mu_1\appr \mu_2\iff \forall x\in X, \mu_1(x)\leq\mu_2(x).
+	\end{gather*} 
+	The definition derives the ordering on morphisms of each hom-set $\hom(X,\sub Y)$ as usual in $\Set$.\\
+	Assuming $\mu\in\sub X$, $g\c X\to Y$, $\nu\in\sub Y$, and $\nu\appr \sub g(\mu)$, we need to prove that there exists $\mu'\in \sub X$, that $\mu'\appr\mu$ and $\nu=\sub g(\mu')$.
+\end{example}
+
+\begin{lemma}\label{lem:liftable}
+	Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every $f\in\Hom(X,FY)$ we have:
+	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
+		\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
+		\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
+	\end{enumerate}
+\end{lemma}
+\begin{proof}
+	$(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$.
+	
+	Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
+	
+	$(II)$ Basically, by definition of $\op$ and relation composition we have
+	\begin{gather*}
+		(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
+		(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
+	\end{gather*}
+	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
+\end{proof}
+\begin{lemma}\label{lem:coliftable}
+	Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $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 coliftable, 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:coliftable-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)$ Basically, by definition of $\op$ and relation composition we have
+	\begin{gather*}
+		(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
+		(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
+	\end{gather*}
+	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
+\end{proof}
+
+
 \section{Coalgebraic Bisimulation}%\label{sec:}
 In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has
 products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\
@@ -1091,7 +1218,7 @@ A big concern with this approach is that Comma Objects are defined in a 2-catego
 
 \subsection{Choosing a suitable order for our setting}
 Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term.
-\section{Symmetric Simulation is Bisimulation}
+\section{Symmetric Simulation is a Bisimulation}
 \begin{definition}[Graph]
 	In a category $\BC$ a graph is a tuple $(R,X)$ of the following form:
 	\begin{equation*}
@@ -1336,6 +1463,35 @@ We show this relation with $F_\rel(R,X)$.
 	As the mentioned property is equivalent with $\sigma$ being a bisimulation, and bisimulation is unique, then $\sigma_1=\sigma_2$.
 \end{proof}
 %
+\begin{prop}
+	Assuming that the ordering on the functor $F$ is natural, and gives posets, given witness $\sigma$ for a symmetric object $R$ to be an HJ-simulation, if $(Fs)^\dagger\comp\sigma=\sigma\comp s$, then $\sigma$ is a witness for $R$ to be an $HJ$-bisimulation. 
+\end{prop}
+\begin{proof}
+	Since $\sigma$ is a witness that $R$ is an $HJ$-simulation we have
+	\begin{gather*}
+		\alpha\comp p_1\appr (Fp_1)^\dagger\comp\sigma,\\
+		(Fp_2)^\dagger\comp\sigma\appr\alpha\comp p_2.
+	\end{gather*}
+	So, we have:
+	\begin{align*}
+		\alpha\comp p_1\appr (Fp_1)^\dagger\comp\sigma&\\
+		\Rightarrow&\alpha\comp p_1\comp s\appr (Fp_1)^\dagger\comp\sigma\comp s&\by{naturality of $\appr$}\\
+		\Rightarrow&\alpha\comp p_1\comp s\appr (Fp_1)^\dagger\comp (Fs)^\dagger\comp\sigma&\by{\eqref{eq:diag-sym-rel}}\\
+		\Rightarrow&\alpha\comp p_2\appr (Fp_1)^\dagger\comp (Fs)^\dagger\comp\sigma&\by{assumption}\\
+		\Rightarrow&\alpha\comp p_2\appr (Fp_2)^\dagger\comp\sigma&\by{\eqref{eq:diag-sym-rel}}\\
+		\Rightarrow&\alpha\comp p_2= (Fp_2)^\dagger\comp\sigma&\by{anti symmetry of $\appr$}
+	\end{align*}
+	Similarly we have:
+	\begin{align*}
+		(Fp_2)^\dagger\comp\sigma\appr\alpha\comp p_2&\\
+		\Rightarrow&(Fp_2)^\dagger\comp\sigma\comp s\appr\alpha\comp p_2\comp s&\by{naturality of $\appr$}\\
+		\Rightarrow&(Fp_2)^\dagger\comp(Fs)^\dagger\comp\sigma\appr\alpha\comp p_2\comp s&\by{\eqref{eq:diag-sym-rel}}\\
+		\Rightarrow&(Fp_2)^\dagger\comp(Fs)^\dagger\comp\sigma\appr\alpha\comp p_1&\by{assumption}\\
+		\Rightarrow&(Fp_1)^\dagger\comp\sigma\appr\alpha\comp p_1&\by{\eqref{eq:diag-sym-rel}}\\
+		\Rightarrow&(Fp_1)^\dagger\comp\sigma=\alpha\comp p_1&\by{anti symmetry of $\appr$}
+	\end{align*}\qed
+\end{proof}
+%
 Now, we give a counter example of a symmetric relation on $\Set$ that is a simulation according to~\autoref{def:sim}, i.e, exists the morphism $\sigma$ that commutes laxly in~\eqref{eq:diag-lax-sim}, but $\sigma$ is not a coalgebraic bisimulation, although the relation that we give is clearly a bisimulation in the classic sense. 
 We set $R=\{(A,B),(B,A),(C_1,C_2),(C_2,C_1),(C'_2,C_2),(C_2,C'_2),(C_2,C_2)\}$, $F=\mathbf{Id}$, $\appr=\Delta\cup\{(C_1,C_2),(C_2,C'_2)\}$, and the coalgebra $\alpha$ is defined with the following set of reductions:
 \begin{gather*}
@@ -2049,6 +2205,58 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 %	\end{gather*}
 %	We have $(Fp_1)^\dagger\comp\sigma$.
 %\end{proof}
+\begin{example}\label{ex:sym-sim-bisim-count}
+Assuming that the functor is the powerset endofunctor over the category of sets and injective maps. Let us call this functor $\powfi$. For every $X$, we define the order on $\powfi X$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder. Then we define the order over every $\Hom(X,\powfi Y)$ pointwise. We have chosen the category of sets with injective maps because we could not define a functor from $\Set$ to $\preord$ with the mentioned ordering.\\
+We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
+\begin{gather*}
+	\alpha(x)=
+	\begin{cases} 
+		\{1,2\} & x=1  \\
+		\{2,3\} & x=2\\
+		\{3\} & x=3
+	\end{cases}\qquad
+\begin{tikzpicture}[scale=0.1]
+	\tikzstyle{every node}+=[inner sep=0pt]
+	\draw [black] (23.8,-25.2) circle (3);
+	\draw (23.8,-25.2) node {$1$};
+	\draw [black] (42.4,-25.2) circle (3);
+	\draw (42.4,-25.2) node {$2$};
+	\draw [black] (33,-34.6) circle (3);
+	\draw (33,-34.6) node {$3$};
+	\draw [black] (22.477,-22.52) arc (234:-54:2.25);
+	\fill [black] (25.12,-22.52) -- (26,-22.17) -- (25.19,-21.58);
+	\draw [black] (41.077,-22.52) arc (234:-54:2.25);
+	\fill [black] (43.72,-22.52) -- (44.6,-22.17) -- (43.79,-21.58);
+	\draw [black] (26.8,-25.2) -- (39.4,-25.2);
+	\fill [black] (39.4,-25.2) -- (38.6,-24.7) -- (38.6,-25.7);
+	\draw [black] (40.28,-27.32) -- (35.12,-32.48);
+	\fill [black] (35.12,-32.48) -- (36.04,-32.27) -- (35.33,-31.56);
+\end{tikzpicture}
+\end{gather*}
+$\sigma$ is defined as below:
+\begin{gather*}
+	\sigma(w)=\{(1,2),(2,1)\}
+\end{gather*}
+$R$ is symmetric, and $\sigma$ is a witness for $R$ to be an AM-simulation, but $R$ is not a bisimulation in the traditional sense because $(2,1)\in R$, and $2\to 3$, but $(3,1)$ or $(3,2)$ are not in $R$. It is easy to see that it is not an AM-bisimulation as well because we can not define a function that can serve as an evidence for it as $3$ does not appear in any pair in $R$, while it exists in $\alpha(2)$.
+
+This counter-example also works as a counter-example for Hughes-Jacobs definition of simulation. Actually, $\appr\comp(FR)^\dagger\comp\appr=\powf X\times \powf X$, so $R\subseteq( \appr\comp(FR)^\dagger\comp\appr)$ that means that $R$ is a simulation. Worth noting that they claim that their setting works for an arbitrary category. So, unlike their definition, in the context of the relator-based definitions that only work in $\Set$, this counter-example does not live.
+
+The mentioned ordering is not liftable. Assuming $h\in\Hom(\nats,\powfi \nats)$, $g\c \nats\to \nats$, and $k\in\Hom(\nats,\powfi \nats)$, and they are defined for every $n$ in $\nats$ as $h(n)=\{2\times n\}$, $g(n)=3\times n$, and $k(n)=\{n\}$, then $|h(n)|=|\powfi g(k(n))|=1$ that means $h\appr\powfi g\comp k$ is satisfied, but there is no $k'$ that $h=\powfi g\comp k$ because we can never have $h(1)=\powfi g\comp k'(1)$, as assuming $k'(1)=\{n\}$, and $n$ must be a natural number, then we should have $2=3\times n$ that is impossible.
+
+It is the same for HJ-simulation and HJ-bisimulation. We define $\sigma^\dagger\c R\to (\powf R)^\dagger$ as 
+\begin{gather*}
+	\sigma^\dagger(w)=\{(\{1,2\},\{1,2\})\}.
+\end{gather*}
+Indeed, $\sigma^\dagger$ is a witness for $R$ to be an HJ-simulation, but it is not a witness for $R$ to be an HJ-bisimulation. Similar to the case for AM-bisimulation, we can not have a witness for $R$ to be an HJ-bisimulation.
+\end{example}
+
+\begin{example}
+	In~\autoref{ex:sym-sim-bisim-count} we gave a counter-example with an ordering that gives preorders. Now, we slightly change the ordering so that it gives posets. We define $\appr$ as follows:
+	\begin{gather*}
+		A\appr B \iff
+	\end{gather*}
+\end{example}
+
 \subsection{The concrete proof}
 %\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}
 %	Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
@@ -2192,18 +2400,26 @@ Now, we prove our main statement.
 \end{cor}
 Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor.
 \subsection{Maybe Functor}
-We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_{X+1}\cup\{(\bot,x)\mid x\in X\}$.\\
-Now, we prove that the given order on the maybe functor is a liftable one.
+We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$, and for every $x\in\Dom(f)$ we have $f(x)=g(x)$ ($\Dom(f)$ is the domain of a function $f$). 
+Now, we prove that the given order on the maybe functor is liftable and coliftable.
 \begin{lemma}\label{lem:maybe-lif}
 	The order structure on the set-functor $FX=X+1$ is a liftable order.
 \end{lemma}
 \begin{proof}
-	By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
-	\begin{itemize}
-		\item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$.
-
-		\item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
-	\end{itemize}
+%	By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
+%	\begin{itemize}
+%		\item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$.
+%		\item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
+%	\end{itemize}
+Assuming that $h\in\Hom(X,Z+1)$, $g\c Y\to Z$, $k\in\Hom(X,Y+1)$, such that $h\appr (g+1)\comp k$. We define $k'\in\Hom(X,Y+1)$ as follows:
+\begin{gather*}
+	k'(x)=
+	\begin{cases}
+		\bot&x\notin\Dom(h)\\
+		k(x)&x\in\Dom(h)
+	\end{cases}
+\end{gather*}
+We have $\Dom((g+1)\comp k')=\Dom(k')$ and $\Dom(k')=\Dom(h)$, so we have $\Dom((g+1)\comp k')=\Dom(h)$. If $x\in\Dom(h)$, then $h(x)=(g+1)\comp k(x)$ and $(g+1)\comp k(x)=(g+1)\comp k'(x)$, so we have $h(x)=(g+1)\comp k'(x)$. So, we have $h=(g+1)\comp k'$. Additionally, $\Dom(k')\subseteq\Dom(k)$, and for every $x\in \Dom(k')$, we have $k'(x)=k(x)$, so we have $k'\appr k$. \qed
 \end{proof}
 \begin{lemma}\label{lem:maybe-colif}
 	The order structure on the set-functor $FX=X+1$ is a coliftable order.
@@ -2286,41 +2502,79 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph
 %	Now, we are left to prove that if $\alpha(x_1)\in X$ and $\alpha(x_2)\in X$ then $\beta(x_1,x_2)\in R$ that means that the codomain of $\beta$ is indeed $R+1$. We assume $\alpha(x_i)\in X$. Since $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$ we have $\beta(x_1,x_2)\in R$.
 %	\qed
 %\end{proof}
-
+%%%%%%Second proof:
 \begin{prop}\label{prop:sym-sim-bis-may}
 	For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation.
 \end{prop}
 \begin{proof}
 	We prove that $\sigma$ also is a witness for $R$ to be an AM-bisimulation. For every $(x_1,x_2)\in R$ we have
-	\begin{enumerate}
-		\item $\alpha(x_1)=p_1+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1},
-		\item $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\
-		%	\end{enumerate}
-	and since $R$ is symmetric, we have 
-	%		\begin{enumerate}
-		\item $\alpha(x_2)=p_1+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2},
-		\item $\alpha(x_1)\sappr p_2+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3},
-	\end{enumerate}
-	Followed by $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$ we have the following cases:
-	\begin{itemize}
-		\item $\alpha(x_2)=p_2+1\comp\sigma(x_1,x_2)$: In this case, we already have $\sigma$ as a witness for $R$ to be a bisimulation.
-		\item $Fp_2\comp\sigma(x_1,x_2)=\bot$: In this case, we have
-		\begin{align*}
-			p_2+1\comp\sigma(x_1,x_2)=\bot,&\\
-			\Rightarrow&\sigma(x_1,x_2)=\bot,\\
-			\Rightarrow&p_1+1\comp\sigma(x_1,x_2)=\bot,\\
-			\Rightarrow&\alpha(x_1)=\bot,&\eqref{eq:maybe-func-set-1}\\
-			\Rightarrow&p_2+1\comp\sigma(x_2,x_1)=\bot,&\eqref{eq:maybe-func-set-3}\\
-			\Rightarrow&\sigma(x_2,x_1)=\bot,\\
-			\Rightarrow&p_1+1\comp\sigma(x_2,x_1)=\bot,\\
-			\Rightarrow&\alpha(x_2)=\bot,&\eqref{eq:maybe-func-set-2}\\
-			\Rightarrow&\alpha(x_2)=p_1+1\comp\sigma(x_1,x_2).
-		\end{align*}
-	\end{itemize}\qed
+%	\begin{enumerate}
+%		\item $\alpha(x_1)=(p_1+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1},
+%		\item $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\
+%		%	\end{enumerate}
+%	and since $R$ is symmetric, we have 
+%	%		\begin{enumerate}
+%		\item $\alpha(x_2)=(p_1+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2},
+%		\item $\alpha(x_1)\sappr (p_2+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3},
+%	\end{enumerate}
+%	Followed by $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$ we have the following cases:
+%	\begin{itemize}
+%		\item $\alpha(x_2)=(p_2+1)\comp\sigma(x_1,x_2)$: In this case, we already have $\sigma$ as a witness for $R$ to be a bisimulation.
+%		\item $p_2+1\comp\sigma(x_1,x_2)=\bot$: In this case, we have
+%		\begin{align*}
+%			(p_2+1)\comp\sigma(x_1,x_2)=\bot,&\\
+%			\Rightarrow&\sigma(x_1,x_2)=\bot,\\
+%			\Rightarrow&(p_1+1)\comp\sigma(x_1,x_2)=\bot,\\
+%			\Rightarrow&\alpha(x_1)=\bot,&\eqref{eq:maybe-func-set-1}\\
+%			\Rightarrow&(p_2+1)\comp\sigma(x_2,x_1)=\bot,&\eqref{eq:maybe-func-set-3}\\
+%			\Rightarrow&\sigma(x_2,x_1)=\bot,\\
+%			\Rightarrow&(p_1+1)\comp\sigma(x_2,x_1)=\bot,\\
+%			\Rightarrow&\alpha(x_2)=\bot,&\eqref{eq:maybe-func-set-2}\\
+%			\Rightarrow&\alpha(x_2)=(p_1+1)\comp\sigma(x_1,x_2).
+%		\end{align*}
+%	\end{itemize}\qed
+\begin{enumerate}
+	\item $\alpha\comp p_1=(p_1+1)\comp\sigma$\label{eq:maybe-func-set-1},
+	\item $\alpha\comp p_2\sappr (p_2+1)\comp\sigma$\label{eq:maybe-func-set-2},\\
+and since $R$ is symmetric, we have 
+\end{enumerate}
+	Followed by~\eqref{eq:maybe-func-set-2} for every $(x_1,x_2)\in R$ we have $\alpha(x_2)=(p_2+1)\comp\sigma(x_1,x_2)$ and $\Dom((p_2+1)\comp\sigma)\subseteq\Dom(\alpha\comp p_2)$. We have
+	\begin{align*}
+		\Dom((p_2+1)\comp\sigma)&\\
+		=&\Dom(\sigma)\\
+		=&\Dom((p_1+1)\comp\sigma)\\
+		=&\Dom(\alpha\comp p_1)&\by{\eqref{eq:maybe-func-set-1}}\\
+		=&\Dom(\alpha\comp p_1\comp s)\\
+		=&\Dom(\alpha\comp p_2)
+	\end{align*}
+	So, we have $\alpha\comp p_2= (p_2+1)\comp\sigma$ as well that means that $\sigma$ also serves as a witness for $R$ to be a bisimulation.
 \end{proof}
 
-Now, we want to abstract the given proof for an extensive category that has terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. %For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$.\sgnote{This abstract order is coarser than (not the concretisation of) the pointwise Set order at \autoref{lem:set-ord-str}: here the \emph{whole} map must be $\bot$, whereas pointwise a map may be $\bot$ on some points and agree elsewhere. Please check the two agree on the hom-sets you actually use, or justify why the coarser order suffices.}
+Now, we want to abstract the given proof for an extensive category that has terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. We use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$.%For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$.\sgnote{This abstract order is coarser than (not the concretisation of) the pointwise Set order at \autoref{lem:set-ord-str}: here the \emph{whole} map must be $\bot$, whereas pointwise a map may be $\bot$ on some points and agree elsewhere. Please check the two agree on the hom-sets you actually use, or justify why the coarser order suffices.}
 %Although even in the context that we are at the moment, it does not seem plausible to prove that a symmetric simulation is a bisimulation without having an operator like $\join$ in~\autoref{prop:sym-sim-bis-maybe} that takes two morphisms of the same type and gives one.
+ The following lemma is an abstraction of saying that in $\Set$ assuming $f\c X\to Y+1$ and $g\c Y\to Z$, we have $\Dom((g+1)\comp f)=\Dom(f)$ that we have already used multiple times in the concrete proofs. 
+\begin{lemma}
+	Assuming that $(X_Y,f_Y,i)$ and $(X_Y,p,i)$ are pullbacks in the following diagram, then $p=g\comp f_Y$.
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			{X_Y} \& X \\
+			Y \& {Y+Q} \\
+			Z \& {Z+Q'}
+			\arrow["i", tail, from=1-1, to=1-2]
+			\arrow["{f_Y}"', from=1-1, to=2-1]
+			\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
+			\arrow["p"', bend right=50, from=1-1, to=3-1]
+			\arrow["f", from=1-2, to=2-2]
+			\arrow["{\inl_Y}"', tail, from=2-1, to=2-2]
+			\arrow["{g}"', from=2-1, to=3-1]
+			\arrow["g+q", from=2-2, to=3-2]
+			\arrow["{\inl_Z}"', tail, from=3-1, to=3-2]
+		\end{tikzcd}
+	\end{equation*}
+\end{lemma}
+\begin{proof}
+	IT simply relies on the fact that injections in an extensive category are assumed to be monic, and that the pullback of a monomorphism gives a monomorphism leg in the pullback's span.
+\end{proof}
 Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g\rightarrowtail X$, and $X_f$ and $X_g$ are pullbacks of $f$ and $\inl$, and $g$ and $\inl$ accordingly, then $f\appr g$ if there exists $h\c X_f\rightarrowtail X_g$ that commutes in the following diagram:
 \begin{equation*}
 	\begin{tikzcd}[ampersand replacement=\&]
@@ -2335,50 +2589,82 @@ Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g
 	The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order.
 \end{lemma}
 \begin{proof}
-	For morphisms $h\c X\to Z+1$, $g\c Y\to Z$, and $k\c X\to Y+1$, we assume $h\appr Fg\comp k$ that means we have two cases:
-	\begin{itemize}
-		\item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $Fg\comp k'=h$.
-		\item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $Fg\comp k'=h$.\qed
-	\end{itemize}
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			\& Z \& \\
+			{X_h} \&\& {Z+1} \\
+			{X_k} \& X \\
+			Y \& {Y+1} \\
+			Z \& {Z+1}
+			\arrow["{\inl_Z}", tail, from=1-2, to=2-3]
+			\arrow["q", from=2-1, to=1-2]
+			\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=2-1, to=2-3]
+			\arrow["e"', dashed, from=2-1, to=3-1]
+			\arrow["{h_d}", tail, from=2-1, to=3-2]
+			\arrow["{k_d}", tail, from=3-1, to=3-2]
+			\arrow["{k_Y}"', from=3-1, to=4-1]
+			\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-1, to=4-2]
+			\arrow["p"', bend right=50, from=3-1, to=5-1]
+			\arrow["h"', from=3-2, to=2-3]
+			\arrow["k"', from=3-2, to=4-2]
+			\arrow["{\inl_Y}"', tail, from=4-1, to=4-2]
+			\arrow["g"', from=4-1, to=5-1]
+			\arrow["{g+1}"', from=4-2, to=5-2]
+			\arrow["{\inl_Z}"', tail, from=5-1, to=5-2]
+		\end{tikzcd}
+	\end{equation*}
+	We define $k'=k\comp\mathsf{iso}\comp(k_d+1)\comp(e+1)\comp\mathsf{iso}$. We have:
+	\begin{align*}
+		(g+1)\comp k\comp\mathsf{iso}\comp(k_d+1)\comp(e+1)\comp\mathsf{iso}\\
+		(g+1)\comp k\comp\mathsf{iso}\comp(h_d+1)\comp\mathsf{iso}
+	\end{align*}
+	\todo{Finish! Perhaps, $k'=k\comp\mathsf{iso}\comp(k_d+1)\comp(e+1)\comp\mathsf{iso}$.}
 \end{proof}
-To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category is extensive, we use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$. We take $\brks{\alpha\comp p_1,\alpha\comp p_2}\c R\to (X+1)\times(X+1)$, where $(X+1)\times (X+1)\iso X^2+(2\times X)+1$, and we assume the following pullbacks exist:
-\begin{equation*}
-	\begin{tikzcd}[ampersand replacement=\&]
-		{R_{X^2}} \& R \& {R_{2\times X}} \& R \\
-		{X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\
-		\& {R_1} \& R \\
-		\& 1 \& {X^2+(2\times X)+1}
-		\arrow["{q_1}", from=1-1, to=1-2]
-		\arrow["{q_2}"', from=1-1, to=2-1]
-		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
-		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-2, to=2-2]
-		\arrow["{r_1}", from=1-3, to=1-4]
-		\arrow["{r_2}"', from=1-3, to=2-3]
-		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4]
-		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-4, to=2-4]
-		\arrow["{\mathsf{in}_1}"', from=2-1, to=2-2]
-		\arrow["{\mathsf{in}_2}"', from=2-3, to=2-4]
-		\arrow["{s_1}", from=3-2, to=3-3]
-		\arrow["{s_2}"', from=3-2, to=4-2]
-		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-2, to=4-3]
-		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=3-3, to=4-3]
-		\arrow["{\mathsf{in}_3}"', from=4-2, to=4-3]
-	\end{tikzcd}
-\end{equation*}
+%\begin{proof}
+%	For morphisms $h\c X\to Z+1$, $g\c Y\to Z$, and $k\c X\to Y+1$, we assume $h\appr Fg\comp k$ that means we have two cases:
+%	\begin{itemize}
+%		\item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $Fg\comp k'=h$.
+%		\item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $Fg\comp k'=h$.\qed
+%	\end{itemize}
+%\end{proof}
+%To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category is extensive, we use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$. We take $\brks{\alpha\comp p_1,\alpha\comp p_2}\c R\to (X+1)\times(X+1)$, where $(X+1)\times (X+1)\iso X^2+(2\times X)+1$, and we assume the following pullbacks exist:
 %\begin{equation*}
 %	\begin{tikzcd}[ampersand replacement=\&]
-%		R \& I \& {X^2+(2\times X)+1}
-%		\arrow["e", two heads, from=1-1, to=1-2]
-%		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}"', bend right=20, from=1-1, to=1-3]
-%		\arrow["m", tail, from=1-2, to=1-3]
+%		{R_{X^2}} \& R \& {R_{2\times X}} \& R \\
+%		{X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\
+%		\& {R_1} \& R \\
+%		\& 1 \& {X^2+(2\times X)+1}
+%		\arrow["{q_1}", from=1-1, to=1-2]
+%		\arrow["{q_2}"', from=1-1, to=2-1]
+%		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
+%		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-2, to=2-2]
+%		\arrow["{r_1}", from=1-3, to=1-4]
+%		\arrow["{r_2}"', from=1-3, to=2-3]
+%		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4]
+%		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-4, to=2-4]
+%		\arrow["{\mathsf{in}_1}"', from=2-1, to=2-2]
+%		\arrow["{\mathsf{in}_2}"', from=2-3, to=2-4]
+%		\arrow["{s_1}", from=3-2, to=3-3]
+%		\arrow["{s_2}"', from=3-2, to=4-2]
+%		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-2, to=4-3]
+%		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=3-3, to=4-3]
+%		\arrow["{\mathsf{in}_3}"', from=4-2, to=4-3]
 %	\end{tikzcd}
 %\end{equation*}
-So, we have the following:
-\begin{gather*}
-	R\iso R_{X^2}+R_{2\times X}+R_{1}
-\end{gather*}
-And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$.
-\sgnote{This abstraction is unfinished: the crux $R_{2\times X}\iso 0$ (the ``no mixed pairs'' content of \autoref{lem:maybe-func-set}) is stated but not proved, and the subsection ends here. Either complete the argument or mark it clearly as work in progress.}
+%%\begin{equation*}
+%%	\begin{tikzcd}[ampersand replacement=\&]
+%%		R \& I \& {X^2+(2\times X)+1}
+%%		\arrow["e", two heads, from=1-1, to=1-2]
+%%		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}"', bend right=20, from=1-1, to=1-3]
+%%		\arrow["m", tail, from=1-2, to=1-3]
+%%	\end{tikzcd}
+%%\end{equation*}
+%So, we have the following:
+%\begin{gather*}
+%	R\iso R_{X^2}+R_{2\times X}+R_{1}
+%\end{gather*}
+%And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$.
+%\sgnote{This abstraction is unfinished: the crux $R_{2\times X}\iso 0$ (the ``no mixed pairs'' content of \autoref{lem:maybe-func-set}) is stated but not proved, and the subsection ends here. Either complete the argument or mark it clearly as work in progress.}
 \section{Relators}
 \subsection{Two-way similarity in Hughes-Jacobs}
 Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is:
@@ -2765,6 +3051,12 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	$\hat{L}$ is a Barr relator.
 \end{prop}
 \begin{proof}
+	We have
+	\begin{gather*}
+		\hat{\emre}r=\emre r\cap (\emre r^\op)^\op,\\
+		\hat{\emre}r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}\cap\{(T,S)\mid x\in S\Rightarrow \exists y\in T, y\;r\;x\}.
+	\end{gather*}
+	Assuming that $r=\pi_2\comp(\pi_1)^\op$ we have to prove that $\hat{L}r=\powf\pi_2\comp(\powf\pi_1)^\op$.
 	\todo{Finish.}
 \end{proof}
 
@@ -2874,65 +3166,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 %	\end{enumerate}
 %\end{definition}
 
-\begin{definition}[Liftable Order Structure]\label{def:liftable-ord}
-	A \emph{liftable 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}[Coliftable Order Structure]\label{def:coliftable-ord}
-	A \emph{coliftable 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)$, and $g$ is surjective, 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}\label{lem:set-ord-str}
-	In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a liftable order structure. 
-\end{lemma}
-\begin{proof}
-	For every $f,g\in\Hom(X,FY)$, we define $f\appr g$ whenever for all $x\in X$, $f(x)\leq g(x)$.
-	
-	Now, assuming $f\c X'\to X$, $\alpha,\beta\c X\to FY$, and $\alpha\appr\beta$, then for every $x'\in X'$, we have $\alpha(f(x'))\leq\beta(f(x'))$, so we have $\alpha\comp f\appr \beta\comp f$. Additionally, if we assume $g\c Y\to Y'$, then since $\leq$ satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, for every $x\in X$ we have $Fg\comp\alpha(x)\leq Fg\comp\beta(x)$.
-	
-	Furthermore, if we have $g\c Y\to Z$, $k\c X\to FY$, $h\c X\to FZ$, and $Fg\comp k\appr h$, then for every $x\in X$ we have $Fg\comp k(x)\leq h(x)$, thus by the assumption of the lemma, for every $x$, there exists a set that we call $k'(x)$, for which we have $Fg(k'(x))\leq h(x)$. So, we have a function $k'\c X\to FY$, such that for every $x$ we have $Fg\comp k'(x)\leq h(x)$ that means $Fg\comp k'\appr h$.
-	\qed
-\end{proof}
-\begin{remark}\label{rem:set-ord-str-co}
-	The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures.
-\end{remark}
-\begin{lemma}\label{lem:liftable}
-	Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every $f\in\Hom(X,FY)$ we have:
-	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
-		\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
-		\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
-	\end{enumerate}
-\end{lemma}
-\begin{proof}
-	$(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$.
-	
-	Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
-	
-	$(II)$ Basically, by definition of $\op$ and relation composition we have
-	\begin{gather*}
-		(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
-		(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
-	\end{gather*}
-	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
-\end{proof}
-\begin{lemma}\label{lem:coliftable}
-	Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $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 coliftable, 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:coliftable-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)$ Basically, by definition of $\op$ and relation composition we have
-	\begin{gather*}
-		(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
-		(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
-	\end{gather*}
-	So it follows directly from applying $\op$ on both sides of $(I)$.\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 coliftable order structure $\appr$, the following propositions hold:
 %	\begin{enumerate}
@@ -2976,40 +3210,26 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \begin{proof}
 	They all follow in an obvious way from~\autoref{lem:liftable} and~\autoref{lem:coliftable}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed
 \end{proof}
-\begin{example}
-	In the category of sets, subset over the powerset functor is an example of a liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$.
-	
-	Assuming $z\in\powf g(k')$, then there exists $y'\in \{y\mid g(y)\in h\}$ that $z=g(y')$, so $z\in h$ and $\powf g(k')\subseteq h$.
-	
-	Assuming $z\in h$, since $h\subseteq \powf g(k)$, then $z\in\powf g(k)$. So, there exists $y'\in k$ such that $g(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means  $z\in\powf g(k')$.\qed
-\end{example}
-The following example justifies why the $g$ in~\autoref{def:coliftable-ord} should be surjective:
-\begin{example}
-	If we take the surjectivity of $g$ out of~\autoref{def:coliftable-ord}, subset relation over the powerset functor is NOT an example of a coliftable order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$, 
+\begin{prop}\label{prop:lax-relator-full-comm}
+	For a functor $F$ with a liftable order we have:
 	\begin{gather*}
-		g(z)=
-		\begin{cases} 
-			0 & z\in\mathbb{Z}^+ \\
-			1 & \mathsf{otherwise}  
-		\end{cases}
+		(\bar{F}r\comp\appr)\subseteq(\appr\comp\bar{F}r) 
 	\end{gather*}
-	then 
-	\begin{gather*}
-		\powf g(A)=
-		\begin{cases} 
-			\emptyset & A=\emptyset \\
-			\{0\} & A\subseteq \mathbb{Z}^+,A\neq\emptyset\\  
-			\{1\} & A\subseteq \mathbb{Z}^-\cup\{0\},A\neq\emptyset\\
-			\{0,1\} & \mathsf{otherwise} 
-		\end{cases}
-	\end{gather*}
-	then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$.
-\end{example}
-\begin{example}
-	In the category of sets, subset over the powerset functor is an example of a coliftable order structure if the $g$ in~\autoref{def:coliftable-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$.
-	
-	Obviously, $\powf g(k')\subseteq h$. Now, assuming $z\in h$ we prove that $z\in \powf g(k')$. Since $g$ is surjective, then exists $A\subseteq Y$ such that $\powf g(A)=h$. By the definition of $k'$, $A\subseteq k'$. So from $z\in h$ we have $z\in \powf g(A)$ that means that exists $a\in A$, such that $g(a)=z$. Now, since $A\subseteq k'$, then $a\in k'$. So, we have $z\in \powf g(k')$.\qed
-\end{example}
+\end{prop}
+\begin{proof}
+	Assuming $x \mathrel{(\bar{F}r\comp\appr)} y$ and $\bar{F}r=F\pi_2\comp(F\pi_1)^\op$, then there exist $x'$ and $p$ such that $x\appr x'$, $p\mathrel{F\pi_1}x'$, and $p\mathrel{F\pi_2}y$. So, we have $x\appr F\pi_1(p)$ then by liftability there exists $p'$ such that $p'\appr p$, and $F\pi_1(p')=x$. Then from $p'\appr p$ we get $F\pi_2(p')\appr y$ that is equivalent with $p' \mathrel{(\appr\comp F\pi_2)} y$, and then we have $x \mathrel{(\appr\comp F\pi_2\comp(F\pi_1)^\op)} y$.\qed
+\end{proof}
+\begin{cor}
+	Assuming that $r$ is an $(\bar{F}r\comp\appr)$-simulation, then it is an $(\appr\comp\bar{F}r)$-simulation as well.
+\end{cor}
+%\begin{example}
+%	In the category of sets, subset over the powerset functor is an example of a liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$.
+%	
+%	Assuming $z\in\powf g(k')$, then there exists $y'\in \{y\mid g(y)\in h\}$ that $z=g(y')$, so $z\in h$ and $\powf g(k')\subseteq h$.
+%	
+%	Assuming $z\in h$, since $h\subseteq \powf g(k)$, then $z\in\powf g(k)$. So, there exists $y'\in k$ such that $g(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means  $z\in\powf g(k')$.\qed
+%\end{example}
+
 \begin{definition}[Natural Relator]
 	An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $r\c X\rto Y$, and all functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp r\comp f)=(Fg)^\op\comp\relar r\comp Ff$.
 \end{definition}
@@ -3077,7 +3297,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.
@@ -3101,7 +3321,7 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
-\subsection{Symmetrization of a Barr relator}
+\subsection{Symmetrization of a lax Barr relator}
 \begin{prop}
 	Assuming $F$ is the maybe functor $FX=X+1$, then the syemmetrization of the left-lax Barr relator of $F$ is a Barr-relator.
 \end{prop}
@@ -3123,7 +3343,37 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 \begin{remark}
 	With a similar argument we can prove that the symmetrization of a right-lax Barr-relator of $F$ is a Barr-relator.
 \end{remark}
-\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion.}
+\begin{lemma}\label{lem:lax-relator-str}
+	For a relation $r$, for functions $k_s\c F\pi_1(\bar{F}r)\to\powf FX$ and $k_b\c F\pi_2(\bar{F}r)\to\powf FX$, defined as 
+	\begin{gather*}
+		k_s(x)=\{(x',y)\mid(x,y)\in\bar{F}r,x'\appr x, (x',y)\notin\bar{F}r\},\\
+		k_b(x)=\{(x',y)\mid(x,y)\in\bar{F}r,x\appr x', (x',y)\notin\bar{F}r\},
+	\end{gather*}
+	we have
+	\begin{gather*}
+		(\bar{F}r)\comp\appr=\bar{F}r\cup(\bigcup_{x\in F\pi_1(\bar{F}r)} k_s(x)),\\
+		(\bar{F}r)\comp\sappr=\bar{F}r\cup(\bigcup_{x\in F\pi_1(\bar{F}r)} k_b(x)).
+	\end{gather*}
+\end{lemma}
+\begin{proof}
+	\todo{Write it down. You have it in your notes.}
+\end{proof}
+\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion. See if~\autoref{prop:lax-relator-full-comm} or~\autoref{lem:lax-relator-str} can help!}
+\subsection{Symmetric relation}
+\begin{prop}
+Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a coalgebra $(X,\alpha)$, then $r$ is an $\hat{\relar}$-bisimulation.
+\end{prop}
+\begin{proof}
+	$r$ being an $\relar$-simulation means that $r\leq \alpha^\op\comp\relar r\comp\alpha$, and $r$ being symmetric means that $r^\op=r$. So, we need to prove that $r\leq\alpha^\op\comp\hat{\relar} r\comp\alpha$. We have:
+	\begin{align*}
+		x \mathrel{(\alpha^\op\comp\hat{\relar} r\comp\alpha)} y&\\
+		\iff &x\mathrel{(\alpha^\op\comp(\relar r\cap (\relar r)^\op)\comp\alpha)} y\\
+		\iff &\exists x',y',\quad x\mathrel{\alpha}x'\quad\&\quad y\mathrel{\alpha}y'\quad\&\quad x'\mathrel{(\relar r\cap (\relar r)^\op)}y'\\
+		\iff &\exists x',y',\quad x\mathrel{\alpha}x'\quad\&\quad y\mathrel{\alpha}y'\quad\&\quad x'\mathrel{\relar r}y'\quad\&\quad x'\mathrel{(\relar r)^\op}y'\\
+		\iff &\exists x',y',\quad x\mathrel{\alpha}x'\quad\&\quad y\mathrel{\alpha}y'\quad\&\quad x'\mathrel{\relar r}y'\quad\&\quad y'\mathrel{\relar r}x'
+	\end{align*}
+	Now, assuming $x\mathrel{r}y$ gives us $x\mathrel{(\alpha^\op\comp\relar r\comp \alpha)} y$ that is equivalent with saying that exist $x'$ and $y'$ such that $x\mathrel{\alpha}x'$, $y\mathrel{\alpha}y'$, and $x'\mathrel{\relar r}y'$. Since $r$ is symmetric, we have $y\mathrel{r} x$ that means that exist $x''$ and $y''$ such that $x\mathrel{\alpha}x''$, $y\mathrel{\alpha}y''$, and $y''\mathrel{\relar r}x''$. On the other hand since $\alpha$ is a function, we have $x''=x'$ and $y''=y'$, so we have $y'\mathrel{\relar r}x'$ that ultimately gives $x\mathrel{(\alpha^\op\comp\hat{\relar}r\comp\alpha)}y$. So, $r$ is an $\hat{\relar}$-bisimulation as well.\qed
+\end{proof}
 \end{document}
 
 

list

@@ -0,0 +1,7 @@
+Introduce HJ-simulation in relator-form, show uniqness of wittnesses.
+Prove a general theorem that symmetric simulation for symmetrized relator yields similarity that is sound and complete for behavioral equivalence (use "Relators and Notions of Simulation Revisited" soundness and compteleness criterion).
+Elaborate this for powerset
+When is symmetrized relator the Barr relator (definition is in "Relators and Notions of Simulation Revisited")?
+At least, try to prove it for the Jacobs-Hughes relator
+Introduce notions of simulation, diverging from HJ-simulation. Do we need two of them (with normalization and without)? How are all of them related?
+Can we separate Hughes-Jacobs relator from one-sided lax relator?