presentation

2026-07-22 13:04:41 +01:00
parent 944bd831b6
commit 5eef8a7955
18 changed files with 1437 additions and 0 deletions
@@ -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! :)
@@ -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.
@@ -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>
@@ -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>
@@ -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>
@@ -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>
@@ -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>
@@ -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}
 }
@@ -0,0 +1,655 @@
 \documentclass{beamer}
 \usetheme{focus}
 % Add option [numbering=none] to disable the footer progress bar
 % Add option [numbering=fullbar] to show the footer progress bar as always full with a slide countx
 \definecolor{main}{RGB}{29, 160, 196}
 \definecolor{text}{RGB}{15, 40, 60}
 \definecolor{background}{RGB}{255, 255, 255}
 \definecolor{catchgreen}{RGB}{0, 166, 147}
 \setbeamercolor{block title alerted}{fg=white, bg=catchgreen}
 \setbeamercolor{block body alerted}{fg=text, bg=catchgreen!10}
 \setbeamertemplate{block begin}
 {
  \par\vskip\medskipamount%
  \IfStrEq{\insertblocktitle}{}{}{
      \begin{beamercolorbox}[colsep*=.75ex]{block title}
        \usebeamerfont*{block title}\insertblocktitle%
      \end{beamercolorbox}%
  }
  {\parskip0pt\par}%
  \ifbeamercolorempty[bg]{block title}
  {}
  {\ifbeamercolorempty[bg]{block body}{}{\nointerlineskip\vskip-0.5pt}}%
  \usebeamerfont{block body}%
  \begin{beamercolorbox}[colsep*=.75ex,vmode]{block body}%
    \ifbeamercolorempty[bg]{block body}{\vskip-.25ex}{\vskip-.75ex}\vbox{}%
 }
 \setbeamercovered{invisible}
 %------------------------------------------------
 \usepackage{booktabs} % Required for better table rules
 \usepackage{xstring}
 %\usepackage{tikz}
 \renewcommand{\baselinestretch}{1.3}
 \usepackage[T1]{fontenc}
 \usepackage[sfdefault]{AlegreyaSans}
 \usepackage{bussproofs}
 \EnableBpAbbreviations
 \usepackage{multicol}
 \usepackage{transparent}
 \usepackage{lipsum}
 \usepackage{graphicx}
 \usepackage{eso-pic}
 \usepackage{proof}
 \usepackage{amsthm}
 \usepackage[T1]{fontenc}
 \usepackage[utf8]{inputenc}
 \usepackage{hyperref}
 \usepackage{amssymb}
 \usepackage{mathtools}
 \usepackage{minted}
 \usepackage{wasysym}
 \usepackage{fontawesome}
 \usepackage{tikz-cd}
 \usepackage{xcolor}
 \usepackage{multicol}
 \usepackage{abraces}
 \usepackage{accsupp}
 \usepackage{stmaryrd}
 \usepackage{multicol}
 \def\bs{{\;\Downarrow\;}}
 \def\la#1{\stackrel{#1}{\rightarrow}}
 \def\a{\rightarrow}
 \def\as{\rightarrow^{\star}}
 \def\sp{{\hspace{1cm}}}
 \def\mp{{\hspace{0.66cm}}}
 \newcommand{\Dar}{\Downarrow}
 \newcommand{\val}{\mathsf{v}}
 \newcommand{\com}{\mathsf{c}}
 \newcommand{\comp}{\cdot}
 \newcommand{\inl}{\mathsf{inl}}
 \newcommand{\inr}{\mathsf{inr}}
 \newcommand{\id}{\mathsf{id}}
 \renewcommand{\prod}{\mathbin{\text{\rotatebox[origin=c]{180}{$\amalg$}}}}
 \renewcommand{\coprod}{\mathbin{\text{{$\amalg$}}}}
 \newcommand{\lcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\LEFTcircle$}}}}
 \newcommand{\fcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\CIRCLE$}}}}
 \newcommand{\tcomp}{\textsf{comp}}
 \newcommand{\unt}{\mathsf{unit}}
 \newcommand{\true}{\mathsf{true}}
 \newcommand{\false}{\mathsf{false}}	
 \newcommand{\bool}{\mathsf{bool}}	
 \newcommand{\fpc}{\mathsf{fix}}	
 \newcommand{\casec}{\mathsf{if}}
 \newcommand{\ndet}{\oplus} %{\pmb{\klplus}}
 %\newcommand{\paral}{\parallel} 
 % {\ensuremath{\boldsymbol{\mid\mid}}}
 \newcommand{\paralv}{\pmb{\parallel_\val}}
 \newcommand{\hask}{\includegraphics[height=\fontcharht\font`\B]{res/haskell-logo.png}}
 \newcommand{\mS}{\mu\Sigma}
 \newcommand{\lbs}[1]{{\mathrel{\;\overset{\raisebox{4pt}{$\scriptstyle #1$\;}}{\smash{\xRightarrow{\hspace{.75em}}}}\;}}}
 \newcommand{\ubs}{{\mathrel{\;\overset{\raisebox{4pt}{\;}}{\smash{\xRightarrow{\hspace{.75em}}}}\;}}}
 \newcommand{\bba}{
 	\mathrel{%
 		\begin{tikzpicture}[baseline=-6pt]
 			\draw[double, double distance=.75pt, -{Stealth[inset=0pt, angle=75:4pt]}] (0,.02) -- (0,-.28);
 		\end{tikzpicture}%
 	}%
 }
 \newcommand{\relar}{\mathsf{R}}
 \newcommand{\powf}{\mathcal{P}}
 \newcommand{\eval}{\mathsf{eval}}
 \newcommand{\refl}{\mathsf{refl}}
 \newcommand{\trans}{\mathsf{trans}}
 \newcommand{\preord}{\mathbf{PreOrd}}
 \newcommand{\rel}{\mathbf{Rel}}
 \newcommand{\spa}{\mathbf{Span}}
 \newcommand{\gra}{\mathbf{Gra}}
 \newcommand{\obj}{\mathbf{Obj}}
 \newcommand{\emre}{\mathbf{L}}
 \newcommand{\spto}{\mathrel{\tikz{\draw[-{Stealth}] (0.0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
 \newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0.04,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);\draw (0.04,0) -- (0,-0.07);\draw (0.04,0) -- (0,0.07);}}}
 \newcommand{\powfi}{\mathcal{P}_{\mathsf{inj}}}
 \newcommand{\appr}{\sqsubseteq}
 \newcommand{\sappr}{\sqsupseteq}
 \newcommand{\Dom}{\mathsf{Dom}}
 \newcommand{\Set}{\mathbf{Set}}
 \newcommand{\simeet}{%
 	\mathbin{%
 		\ooalign{%
 			$\sqcap$\cr
 			\hidewidth\raisebox{0.2ex}{\scalebox{0.44}{$\otimes$}}\hidewidth\cr
 		}%
 	}%
 }
 \title{\Large  Coalgebraic Notions of Simulation, Bisimulation and Relators}
 \author{\small Pouya Partow\\
 \footnotesize Joint work with Sergey Goncharov}
 %\titlegraphic{\transparent{0.1}\includegraphics[width=\textwidth,height=\textheight]{res/ut-logo.png}}
 \titlegraphic{\transparent{1} \includegraphics[scale=0.1]{res/ut-logo.png}}
 \institute{\small  School of Computer Science\\ University of Birmingham}
 \date{ACV 2026\\ July 25th 2026\\ Lisbon}
 \begin{document}
 \begin{frame}
 	\maketitle
 \end{frame}
 \setlength{\parskip}{2ex}
 %
 \begin{frame}{Overview}
 	The content of the talk:
 	\begin{itemize}
 		\item Intuitive introduction to coalgebra and (bi)simulation
 		\item Reviewing basic definitions of coalgebra and (bi)simulation
 		\item Relator-based notions
 		\item Span-based notions
 		\item Motivation! Howe's method for categorical operational semantics
 	\end{itemize}
 \end{frame}
 \begin{frame}{Why Does Equivalence of Systems Matter?}
 	\begin{alertblock}{A basic but fundamental question}
 		When can we say that two systems \emph{behave the same}?
 	\end{alertblock}
 	\vspace{-0.4cm}
 	This question is everywhere, often silently assumed:\vspace{-0.4cm}
 	\begin{itemize}
 		\setlength{\itemsep}{6pt}
 		\item[\faServer] \textbf{Hardware redesign.} A chip redesigned for cheaper production must still compute exactly what the old one did.
 		\item[\faCode] \textbf{Software upgrades.} A bank replaces its backend --- from the customer's view (balances, transactions), nothing should change.
 	\end{itemize}
 	\vspace{0.2cm}
 	\begin{block}{The catch}
 		``Behaving the same'' is intuitive, but making it \emph{precise} and \emph{checkable} is surprisingly subtle.
 	\end{block}
 \end{frame}
 %\begin{frame}{From ``System'' to Mathematics}
 %	\begin{block}{The word ``system'' needs to be made precise}
 %		To reason formally about equivalence, we need a precise model of what a system \emph{is}.
 %	\end{block}
 %	\vspace{0.3cm}
 %	In this work, systems are modeled as \textbf{Kripke frames}.
 %	\begin{block}{Definition: Kripke frame}
 %		A pair $(W, R)$ where $W$ is a set of \emph{states}, and $R \subseteq W \times W$ is a \emph{transition relation}.
 %	\end{block}
 %\end{frame}
 \begin{frame}{From ``System'' to Mathematics}
 	The word ``system'' needs to be made precise.
 %	\vspace{-0.6cm}
 	\begin{block}{}
 	We model systems as mathematical notions like \textbf{labeled transition systems}: a set of states, together with a 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 coffee} (idle);
 					\draw[->] (brewing tea) -- node[above] {take tea} (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 tea} (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 tea} (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 coffee} (idle);
 					\draw[->] (brewing tea) -- node[above] {take tea} (idle);
 				\end{tikzpicture}
 			\end{center}
 			%		\end{columns}
 	\end{block}
 \end{frame}
 \begin{frame}{Mathematical Definitions}
 	\footnotesize
 	\begin{columns}[T,onlytextwidth]
 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 		\column{.48\textwidth}
 		\begin{alertblock}{Labelled Transition Systems}
 			A \emph{labelled transition system} is a triple	$(X,A,T)$, where $T\;\subseteq\;X\times A\times X$.	
 			We write $x\xrightarrow{a}x'$
 			for $(x,a,x')\in T$.
 		\end{alertblock}
 		\vspace{2mm}
 		\begin{block}{Simulation and Bisimulation}
 			A relation $R\subseteq X\times Y$ is a simulation from $(X,A,T)$ to $(Y,A,S)$ whenever
 			\[
 				x\mathrel{R}y,\;
 				x\xrightarrow{a}x'
 				\Rightarrow
 				\exists\,y'.\;
 				y\xrightarrow{a}y'
 				\;\land\;
 				x'Ry'.
 			\]
 			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{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.\\
 			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}{Relators, Simulations and Bisimulations}
 	\footnotesize
 	\begin{columns}[T,onlytextwidth]
 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 		\column{.47\textwidth}
 		\begin{alertblock}{Relator}
 		Assuming $F:\Set\to\Set$ is a functor, an $F$-relator a monotone map that sends a morphism of $\rel$ that is a relation $X\rto Y$ to a relation $FX\rto FY$. 
 		\end{alertblock}
 		\vspace{-0.3cm}
 		\begin{block}{R-Simulation}
 			For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if $r\subseteq \beta\comp\relar r\comp\alpha^{-1}$.
 		\end{block}
 		\vspace{-0.3cm}
 		\begin{alertblock}{Symmetrization of a Relator}
 			Symmetrization of a relator $\relar$ is defined as:
 			\begin{gather*}
 				\hat{\relar}=\relar r\cap (\relar r^{-1})^{-1}
 			\end{gather*}
 		\end{alertblock}
 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 		\column{.47\textwidth}
 		\begin{alertblock}{Symmetric Relator}
 			A relator $\relar$ is symmetric if $\relar=\hat{\relar}$
 		\end{alertblock}
 		\vspace{-0.2cm}
 		\begin{block}{R-Bisimulation}
 			For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-bisimulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is an $R$-simulation, and $R$ is a symmetric relator.
 		\end{block}
 		\vspace{-0.2cm}
 		\begin{block}{R-Similarity}
 			$\relar$-similarity is the greatest $\relar$-simulation.
 		\end{block}
 		\vspace{-0.3cm}
 		\begin{block}{R-Bisimilarity}
 			$\relar$-bisimilarity is the greatest $\relar$-bisimulation.
 		\end{block}
 	\end{columns}
 \end{frame}
 \begin{frame}{Some Examples of Relators}
 	\footnotesize
 	\begin{columns}[T,onlytextwidth]
 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 		\column{.47\textwidth}
 		\begin{alertblock}{Example: Trivial Relator}
 			For an arbitrary set endofunctor $F$, the relator $\mathbf{Q}$ takes every relation $r:X\rto Y$ to $FX\times FY$.
 		\end{alertblock}
 		It is a symmetric relator.
 		\begin{block}{}
 			But it is a bad relator because every relation is a $\mathbf{Q}$-bisimulation!
 		\end{block}
 		\begin{alertblock}{Example: Egli-Milner Relator}
 			The relator $\emre$ is a $\powf$-relator defined as:
 			\begin{gather*}
 				\emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}
 			\end{gather*}
 		\end{alertblock}
 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 		\column{.47\textwidth}
 		We give a family of examples:
 		\begin{alertblock}{Example: Barr Relators}
 			Given a set endofunctor $F$, and $r$ is a relation that $r=\pi_2\comp\pi_1^{-1}$ ($\pi_1$ and $\pi_2$ are functions) the Barr relator $\bar{F}$ is defined as
 			$\bar{F}r=\bar{F}\pi_2\comp(\bar{F}\pi_1)^{-1}$.
 		\end{alertblock}
 		\begin{block}{}
 			The symmetrization of the Egli-Milner relator is a Barr relator, i.e.,
 			\begin{gather*}
 				\hat{\emre}=\bar{\powf}
 			\end{gather*}
 		\end{block}
 		Barr relators are nicely behaved relators.\\ 
 		A trivial relator is a not a Barr relator.
 \end{columns}
 \end{frame}
 \begin{frame}{Lax Barr relators}
 		\footnotesize
 	\begin{columns}[T,onlytextwidth]
 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 		\column{.47\textwidth}
 		An ordering of a set endofunctor $F$ is a functor $G$ that commutes in the following diagram:
 		\begin{equation*}
 			\begin{tikzcd}[ampersand replacement=\&]
 				\& \mathbf{PoSet} \& \\
 				\Set \&\& \Set
 				\arrow["U", from=1-2, to=2-3]
 				\arrow["G", from=2-1, to=1-2]
 				\arrow["F"', from=2-1, to=2-3]
 			\end{tikzcd}
 		\end{equation*}
 		Meaning that for every $X$, there is a poset $(FX,\appr)$.
 		\begin{block}{}
 			For example $(\powf X,\subseteq)$ for every set $X$.
 		\end{block}
 		With orderings we define \emph{lax Barr relators}.\\
 		Lax Barr relators are different abstractions of the Egli-Milner relator.
 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 		\column{.47\textwidth}
 		\begin{block}{}
 			There are multiple of them:
 			\begin{itemize}
 				\item Left-lax: $\appr\comp\bar{F}r$
 				\item Right-lax: $\bar{F}\comp\appr$
 				\item Bi-lax: $\appr\comp\bar{F}r\comp\appr$
 				\item Mid-lax: $F\pi_1\comp\appr\comp(F\pi_2)^{-1}$
 			\end{itemize}
 		\end{block}
 		\begin{alertblock}{Liftability}
 			An ordering on a set endofunctor $F$ is called \emph{liftable}, if\vspace{-0.3cm}
 			\begin{gather*}
 				\alpha\appr\beta\Rightarrow\alpha\comp f\appr \beta\comp f,\\
 				\alpha\appr\beta\Rightarrow Ff'\comp\alpha\appr Ff'\comp \beta,\\
 				h\appr Fg\comp k\Rightarrow \exists k', h=Fg\comp k\;\&\;k'\appr k.
 			\end{gather*}
 		\end{alertblock}
 	\end{columns}
 \end{frame}
 \begin{frame}{Lax Barr relators (2)}
 	\begin{alertblock}{Proposition}
 		Given a set endofunctor $F$, with a liftable ordering 
 		\begin{itemize}
 			\item mid-lax and left-lax relators of $F$ are equal,
 			\item Assuming the axiom of choice, righ-lax and left-lax relators of $F$ are equal,
 			\item the symmetrizaion of the left-lax relator is \emph{sound} and \emph{complete} with respect to \emph{behavioural equivalence}.
 		\end{itemize}
 	\end{alertblock}
 \end{frame}
 \begin{frame}{Span-based definitions}
 	\footnotesize
 	\begin{columns}[T,onlytextwidth]
 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 		\column{.47\textwidth}
 		\begin{alertblock}{Aczel-Mendler Bisimulation}
 			For coalgebras $(X,\alpha)$, and $(Y,\beta)$ a span $(R,X,Y)$ is an \emph{AM-bisimulation}, if there is a \emph{witness} $\gamma$ that commutes in the following:
 			\begin{equation*}
 				\begin{tikzcd}[ampersand replacement=\&]
 					X \& R \& Y \\
 					FX \& FR \& FY
 					\arrow["\alpha"', from=1-1, to=2-1]
 					\arrow["{{p_1}}"', from=1-2, to=1-1]
 					\arrow["{{p_2}}", from=1-2, to=1-3]
 					\arrow["{{\gamma}}", from=1-2, to=2-2]
 					\arrow["\beta", from=1-3, to=2-3]
 					\arrow["{Fp_1}", from=2-2, to=2-1]
 					\arrow["{Fp_2}"', from=2-2, to=2-3]
 				\end{tikzcd}
 			\end{equation*}
 		\end{alertblock}\vspace{-0.2cm}
 		In a \emph{regular category}, if we change $FR$ with $\bar{F}R$ that shows the image of $<Fp_1,Fp_2>$, and the legs of $\bar{F}$ (Barr relator in $\Set$), we have an \emph{Hermida-Jacobs} bisimulation.
 		\begin{block}{}\vspace{-0.2cm}
 			Every AM-bisimulation is an HJ-bisimulation. 
 		\end{block}
 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 		\column{.47\textwidth}
 		\vspace{0.1cm}
 		Assuming the axiom of choice, every HJ-bisimulation is an AM-bisimulation.
 		\begin{block}{}
 			We have \emph{AM-simulation}, if we lax the diagram:\vspace{-0.4cm}
 		\begin{equation*}
 			\begin{tikzcd}[ampersand replacement=\&]
 				X \& R \& Y \\
 				FX \& FR \& FY
 				\arrow["\alpha"', from=1-1, to=2-1]
 				\arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
 				\arrow["{p_1}"', from=1-2, to=1-1]
 				\arrow["{p_2}", from=1-2, to=1-3]
 				\arrow["\sigma", from=1-2, to=2-2]
 				\arrow["\beta", from=1-3, to=2-3]
 				\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
 				\arrow["{{Fp_1}}", from=2-2, to=2-1]
 				\arrow["{{Fp_2}}"', from=2-2, to=2-3]
 			\end{tikzcd}
 		\end{equation*}
 		\end{block}\vspace{-0.3cm}
 		We have found a symmetric AM-simulation that is not a bisimulation!
 		\begin{alertblock}{Proposition}
 			Given a symmetric span $(R,X)$, with the symmetry evidence $s:R\to R$, assuming $R$ is an AM-simulation on a coalgebra $(X,\alpha)$ with evidence $\sigma$, then $R$ is an AM-bisimulation iff $s$ is a coalgebra endomorphism on $(R,\sigma)$.
 		\end{alertblock}
 	\end{columns}
 \end{frame}
 \begin{frame}{Motivation!}
 	\footnotesize
 	We have a coalgbera $(\mS,\gamma)$ in an arbitrary category $\mathbb{C}$.
 	\begin{block}{}
 		-$\mS$ is representing terms of a programming language,\\
 		-and $\gamma$ is giving their big-step reduction.
 	\end{block}
 	\begin{alertblock}{Main Goal}
 		We want to prove that for terms $t$ and $s$, and a context $C$:\vspace{-0.3cm}
 		\begin{gather*}
 			t\sim s\Rightarrow C[t]\sim C[s]
 		\end{gather*}
 	\end{alertblock}\vspace{-0.5cm}
 	-In the literature, this is often proved using \emph{Howe's method}. \\
 	-The method, applies a closure on the bisimilarity relation on $\mS$.\\
 	-Then one should prove that the result is a simulation.\\
 	-The closure preserves symmetry, and symmetric simulation is a bisimulation in traditional definitions.\\
 	-We have found out that it is not always the case.\\
 	-That is why we want to know when exactly a symmetric simulation is a bisimulation.
 \end{frame}
 \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}
@@ -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}