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}

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?