\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

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

\begin{document}

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


\section*{bicategory of relations}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{relations}{}\paragraph*{{Relations}}\label{relations}

[[!include relations - contents]]

\hypertarget{2category_theory}{}\paragraph*{{2-Category theory}}\label{2category_theory}

[[!include 2-category theory - contents]]

\hypertarget{bicategories_of_relations}{}\section*{{Bicategories of relations}}\label{bicategories_of_relations}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{the_beckchevalley_condition}{The Beck-Chevalley condition}\dotfill \pageref*{the_beckchevalley_condition} \linebreak
\noindent\hyperlink{relation_to_allegories}{Relation to allegories}\dotfill \pageref*{relation_to_allegories} \linebreak
\noindent\hyperlink{see_also}{See also}\dotfill \pageref*{see_also} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A \emph{bicategory of relations} is a [[(1,2)-category]] which behaves like the 2-category of internal [[relations]] in a [[regular category]]. The notion is due to Carboni and Walters.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

Note: in this article, the direction of composition is diagrammatic (i.e., ``anti-Leibniz'').

A \textbf{bicategory of relations} is a [[cartesian bicategory]] which is [[locally posetal 2-category|locally posetal]] and moreover in which for every object $X$, the [[diagonal morphism|diagonal]] $\Delta\colon X\to X\otimes X$ and [[codiagonal]] $\nabla\colon X\otimes X\to X$ satisfy the [[Frobenius condition]]:

\begin{displaymath}
\nabla\Delta = (1\otimes \Delta)(\nabla \otimes 1).
\end{displaymath}
Of course, in the locally posetal case the definition of cartesian bicategory simplifies greatly: it amounts to a symmetric monoidal [[Pos]]-[[enriched category]] for which every object carries a commutative [[comonoid]] structure, for which the structure maps $\Delta_X: X \to X \otimes X$, $\varepsilon_X: X \to 1$ are [[left adjoint]] 1-morphisms, and for which every morphism $R: X \to Y$ is a colax morphism of comonoids in the sense that the following inequalities hold:

\begin{displaymath}
R \Delta_Y \leq \Delta_{X \otimes X} (R \otimes R), \qquad R \varepsilon_Y \leq \varepsilon_X.
\end{displaymath}
We remark that such structure is unique when it exists (being a cartesian bicategory is a property of, as opposed to structure on, a bicategory). The [[tensor product]] $\otimes$ behaves like the ordinary product of [[relation]]s. Note this is not a cartesian product in the sense of the usual universal property; nevertheless, it is customary to write it as a product $\times$, and we follow this custom below. It does become a cartesian product if one restricts to the subcategory of left adjoints (called \emph{maps}), which should be thought of as functional relations.

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

We record a few consequences of this notion.

\begin{prop}
\label{}\hypertarget{}{}
(Separability condition) $\Delta\nabla = 1$.

\end{prop}
\begin{proof}
In one direction, we have the 2-cell $1 \leq \Delta\nabla$ which is the unit of the adjunction $\Delta \dashv \Delta_* = \nabla$. In the other direction, there is an adjunction $\varepsilon \dashv \varepsilon_*$ between the counit and its dual, and the unit of this adjunction is a 2-cell $1 \leq \varepsilon\varepsilon_*$, from which we derive

\begin{displaymath}
\Delta\nabla = \Delta\Delta_* \leq \Delta (1 \times \varepsilon)(1 \times \varepsilon_*)\Delta_* = 1
\end{displaymath}
where the last equation follows from the equation $\Delta(1 \times \varepsilon) = 1$ and its dual $(1 \times \varepsilon_*)\Delta_* = 1$.

\end{proof}
\begin{prop}
\label{}\hypertarget{}{}
(Dual Frobenius condition) $\nabla \Delta = (\Delta \times 1)(1 \times \nabla)$.

\end{prop}
\begin{proof}
The locally full subcategory whose 1-cells are \emph{maps} (= left adjoints) has finite products, in particular a symmetry involution $\sigma$ for which

\begin{displaymath}
\Delta_X \sigma_{X X} = \Delta_X
\end{displaymath}
Additionally, the right adjoint $\sigma_{X Y *}$ is the inverse $\sigma_{X Y}^{-1} = \sigma_{Y X}$. Hence the equation above is mated to $\sigma_{X X} \nabla_X = \nabla_X$, and we calculate

\begin{displaymath}
\itexarray{
\nabla_X \Delta_X & = & \sigma_{X X}\nabla_X \Delta_X \sigma_{X X} \\
 & = & \sigma_{X X} (1 \times \Delta_X)(\nabla_X \times 1) \sigma_{X X} \\
 & = & (\Delta_X \times 1_X) \sigma_{X \times X, X} \sigma_{X \times X, X} (1_X \times \nabla_X) \\
 & = & (\Delta_X \times 1_X) (\sigma_{X X} \times 1) (1 \times \sigma_{X X}) (1 \times \nabla_X) \\
 & = & (\Delta_X \times 1_X)(1_X \times \nabla_X)
}
\end{displaymath}
which gives the dual equation.

\end{proof}
\begin{theorem}
\label{}\hypertarget{}{}
In a bicategory of relations, each object is dual to itself, making the bicategory a compact closed bicategory.

\end{theorem}
\begin{proof}
Both the unit and counit of the desired adjunction $X \dashv X$ are given by equality predicates:

\begin{displaymath}
\eta_X = (1 \stackrel{\varepsilon_*}{\to} X \stackrel{\Delta}{\to} X \times X) \qquad \theta_X = (X \times X \stackrel{\nabla}{\to} X \stackrel{\varepsilon}{\to} 1)
\end{displaymath}
One of the triangular equations follows from the commutative diagram

\begin{displaymath}
\itexarray{
X & \stackrel{1 \times \varepsilon_*}{\to} & X \times X & \stackrel{1 \times \Delta}{\to} & X \times X \times X \\
 & {}_1\searrow & \downarrow \mathrlap{\nabla} & & \downarrow \mathrlap{\nabla \times 1} \\
 & & X & \overset{\Delta}{\to} & X \times X \\
 & &  & {}_{1}\searrow & \downarrow \mathrlap{\varepsilon \times 1} \\
 & & & & X
}
\end{displaymath}
where the square expresses a Frobenius equation. The other triangular equation uses the dual Frobenius equation.

\end{proof}
The compact closure allows us to define the opposite of a relation $R: X \to Y$ as the 1-morphism mate:

\begin{displaymath}
R^{op} = (Y \stackrel{1_Y \times \eta_X}{\to} Y \times X \times X \stackrel{1_Y \times R \times 1_X}{\to} Y \times Y \times X \stackrel{\theta_Y \times 1_X}{\to} X)
\end{displaymath}
In this way, a bicategory of relations becomes a [[dagger-compact category|†-compact]] $Pos$-enriched category.

Recall (again) that a \textbf{map} in the bicategory of relations is the same as a 1-cell that has a right adjoint.

\begin{prop}
\label{strict}\hypertarget{strict}{}
If $f \colon X \to Y$ is a map, then $f$ is a strict morphism of comonoids.

\end{prop}
\begin{proof}
If $g$ is the right adjoint of $f$, we have $\Delta_X g \leq (g \times g)\Delta_Y$ since $g$, like any morphism, is a lax comonoid morphism. But this 2-cell is mated to a 2-cell $(f \times f)\Delta_X \to \Delta_Y f$, inverse to the 2-cell $\Delta_Y f \to (f \times f)\Delta_X$ that comes for free. So $f$ preserves comultiplication strictly. A similar argument shows $f$ preserves the counit strictly.

\end{proof}
\begin{prop}
\label{}\hypertarget{}{}
If $f \colon X \to Y$ is a map, then $f^{op}: Y \to X$ equals the right adjoint $f_\ast$.

\end{prop}
\begin{proof}
The proof is much more perspicuous if we use [[string diagram|string diagrams]]. But the key steps are given in two strings of equalities and inequalities. The first gives a counit for $f \dashv f^{op}$, and the second gives a unit. We have

\begin{displaymath}
\itexarray{
f f^{op} & \stackrel{0}{=} & f \circ (\varepsilon_Y \times 1)(\nabla_Y\times 1)(1 \times f \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\
& \stackrel{1}{=} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times f \times f)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ 
 & \stackrel{2}{=} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times \Delta_Y)(1 \times f)(1 \times \varepsilon_X_\ast)\\ 
 & \stackrel{3}{\leq} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times \Delta_Y)(1 \times \varepsilon_Y_\ast) \\
 & \stackrel{4}{=} & (\varepsilon_Y \times 1)\Delta_Y \nabla_Y(1 \times \varepsilon_Y_\ast) \\
 & \stackrel{5}{=} & 1_Y
}
\end{displaymath}
where (0) uses the definition of $f^{op}$, (1) uses properties of monoidal categories, (2) uses the fact that $f$ strictly preserves comultiplication, (3) is mated to the fact that $f$ laxly preserves the counit, (4) is a Frobenius condition, and (5) uses comonoid and dual monoid laws. We can also ``almost'' run the same calculation backwards to get the unit:

\begin{displaymath}
\itexarray{
1_X & \stackrel{0}{=} & (\varepsilon_X \times 1)\Delta_X \nabla_X(1 \times \varepsilon_X_\ast) \\ 
 & \stackrel{1}{=} & (\varepsilon_X \times 1)(\nabla_X \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\
 & \stackrel{2}{=} & (\varepsilon_Y \times 1)(f \times 1)(\nabla_X\times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ 
 & \stackrel{3}{\leq} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(f \times f \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ 
 & \stackrel{4}{=} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times f \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \circ f \\
 & \stackrel{5}{=} & f^{op} f
}
\end{displaymath}
where (0) uses comonoid and dual monoid laws, (1) uses a Frobenius condition, (2) uses the fact that $f$ preserves the counit, (3) is mated to the fact that $f$ laxly preserves comultiplication, (4) uses properties of monoidal categories, and (5) uses the definition of $f^{op}$.

\end{proof}
In fact, what this proof really proves is a converse of the earlier \hyperlink{strict}{proposition}:

\begin{prop}
\label{}\hypertarget{}{}
If $f$ is a strict comonoid morphism, then $f$ has a right adjoint: $f \dashv f^{op}$.

\end{prop}
\begin{prop}
\label{}\hypertarget{}{}
If $f, g: X \to Y$ are maps and $f \leq g$, then $f = g$. Thus, the locally full subcategory whose morphisms are maps is locally discrete (the hom-posets are discrete).

\end{prop}
\begin{proof}
A 2-cell inequality $\alpha: f \leq g$ is mated to a inequality $\alpha_*: g_* \leq f_*$. On the other hand, whiskering $1_Y \times \alpha \times 1_X$ with $1_Y \times \eta_X$ and $\theta_Y \times 1_X$, as in the construction of opposites above, gives $\alpha^{op}: f^{op} \leq g^{op}$. Since $f^{op} = f_*$ and $g^{op} = g_*$, we obtain $f^{op} = g^{op}$, and because $f^{op op} = f$, we obtain $f = g$.

\end{proof}
\hypertarget{the_beckchevalley_condition}{}\subsection*{{The Beck-Chevalley condition}}\label{the_beckchevalley_condition}

Bicategories of relations $\mathbf{B}$ satisfy a Beck-Chevalley condition, as follows. Let $Prod(B_0)$ denote the free category with finite products generated by the set of objects of $\mathbf{B}$. According to the results at [[free cartesian category]], $Prod(B_0)$ is finitely complete.

Since $Map(\mathbf{B})$ has finite products, there is a product-preserving functor $\pi: Prod(B_0) \to \Map(\mathbf{B})$ which is the identity on objects. Again, according to the results of [[free cartesian category]], we have the following result.

\begin{lemma}
\label{}\hypertarget{}{}
If a diagram in $Prod(B_0)$ is a pullback square, then application of $\pi$ to that diagram is a pullback square in $Map(\mathbf{B})$.

\end{lemma}
Let us call pullback squares of this form in $Map(\mathbf{B})$ \emph{product-based} pullback squares.

\begin{prop}
\label{}\hypertarget{}{}
Given a product-based pullback square

\begin{displaymath}
\itexarray{
W & \stackrel{h}{\to} & X \\
k \downarrow & & \downarrow f \\
Y & \underset{g}{\to} & Z
}
\end{displaymath}
in $Map(\mathbf{B})$, the Beck-Chevalley condition holds: $h_* k = f g_*$.

\end{prop}
See Brady-Trimble for further details. The critical case to consider is the pullback square

\begin{displaymath}
\itexarray{
X & \overset{\Delta}{\to} & X \times X \\
\mathllap{\Delta} \downarrow & & \downarrow \mathrlap{\Delta \times 1} \\
X \times X & \underset{1 \times \Delta}{\to} & X \times X \times X
}
\end{displaymath}
where the Beck-Chevalley condition is exactly the Frobenius condition.

One way of interpreting this result is by viewing $\mathbf{B}$ as a hyperdoctrine or monoidal fibration over $Prod(B_0)$, where the fiber over an object $B$ is the local hom-poset $\hom(B, 1)$. Each $f: A \to B$ in the base induces a pullback functor, by precomposing $R: B \to 1$ with $\pi(f): A \to B$ in $Map(\mathbf{B})$. Existential quantification is interpreted by precomposing with right adjoints $\pi(f)_*$. The Beck-Chevalley condition exerts compatibility between quantification and pullback/substitution functors.

\hypertarget{relation_to_allegories}{}\subsection*{{Relation to allegories}}\label{relation_to_allegories}

Any bicategory of relations is an [[allegory]]. Recall that an allegory is a $Pos$-enriched $\dagger$-category whose local homs are meet-semilattices, satisfying Freyd's modular law:

\begin{displaymath}
R S \cap T \leq (R \cap T S^{op})S
\end{displaymath}
A proof of the modular law is given in the blog post by R.F.C. (``Bob'') Walters referenced below.

In fact, we may prove a little more:

\begin{theorem}
\label{}\hypertarget{}{}
The notion of bicategory of relations is equivalent to the notion of unitary pretabular allegory.

\end{theorem}
\begin{proof}
A bicategory of relations has a unit $1$ in the sense of allegories:

\begin{itemize}%
\item $1$ is a partial unit: we have $\varepsilon_1 = id_1: 1 \to 1$, and for any $R: 1 \to 1$ we have $R = R\varepsilon_1 \leq \varepsilon_1 = id_1$.


\item Any object $X$ is the source of a map $\varepsilon_X: X \to 1$, which being a map is entire. Thus $1$ is a unit.



\end{itemize}
A bicategory of relations is also pretabular, for the maximal element in $\hom(X, Y)$ is tabulated as $(\pi_X)_* \pi_Y$, where $\pi_X$, $\pi_Y$ are the product projections for $X \times Y$.

In the other direction, suppose $\mathbf{A}$ is a unitary pretabular allegory. There is a faithful embedding, which preserves the unit, of $\mathbf{A}$ into its coreflexive splitting, which is unitary and tabular, and hence equivalent to $Rel$ of the regular category $Map(\mathbf{A})$. By the proposition below, then, $\mathbf{A}$ is a full sub-2-category of a bicategory of relations. Because the product of two Frobenius objects is again Frobenius, it suffices to show that $\mathbf{A}$ is closed under products in its coreflexive splitting. The inclusion of $\mathbf{A}$ into the latter preserves the unit and the property of being a map, and hence preserves top elements of hom sets, while any allegory functor must preserve tabulations. So the tabulation $(\pi^{X Y}_X, \pi^{X Y}_Y)$ of $\top_{X Y}$ in $\mathbf{A}$ is a tabulation of $\top_{1_X 1_Y}$ in the coreflexive splitting, and hence $1_{X \times Y} \cong 1_X \times 1_Y$.

\end{proof}
\begin{prop}
\label{}\hypertarget{}{}
If $C$ is a [[regular category]], then the bicategory $Rel C$ of [[Rel|relations]] in $C$ is a bicategory of relations.

\end{prop}
\begin{proof}
By theorem 1.6 of Carboni--Walters, $\mathbf{A}$ is a [[Cartesian bicategory]] if:

\begin{itemize}%
\item $Map(\mathbf{A})$ has finite products.


\item $\mathbf{A}$ has local finite products, and $id_1$ is the top element of $\mathbf{A}(1,1)$.


\item The tensor product defined as

\begin{displaymath}
R \otimes S =  (p R p_*) \cap (p' S p'_*)
\end{displaymath}
is functorial, where $p$ and $p'$ are the appropriate product projections.



\end{itemize}
The first two are obvious, and for the third we may reason in the [[internal language]] of $C$. Clearly

\begin{displaymath}
1 \otimes 1 = [x = x \wedge x' = x'] = 1
\end{displaymath}
The formula whose meaning is by $R S \otimes R' S'$ is

\begin{displaymath}
(\exists y. R x y \wedge S y z) \wedge (\exists y'. R' x' y' \wedge S' y' z')
\end{displaymath}
and we may use [[Frobenius reciprocity]] to get

\begin{displaymath}
\begin{aligned}
  & \exists y. (R x y \wedge S y z \wedge y^* \exists y'. R' x' y' \wedge S' y' z') \\
  & \equiv \exists y. (R x y \wedge S y z \wedge  \exists y'. y^* (R' x' y'   \wedge S' y' z')) \\
  & \equiv \exists y, y'. R x y \wedge S y z \wedge R' x' y' \wedge S' y' z' \\
\end{aligned}
\end{displaymath}
which is the meaning of $(R \otimes R')(S \otimes S')$. Finally, the Frobenius law is

\begin{displaymath}
[\exists x'. (x_1, x_2) = (x', x') = (x_3, x_4)]
= [\exists x'. (x_1, x') = (x_3, x_3) \wedge (x_2, x_2) = (x_4, x')]
\end{displaymath}
which follows from transitivity and symmetry of equality.

\end{proof}
\hypertarget{see_also}{}\subsection*{{See also}}\label{see_also}

Other attempted axiomatizations of the same idea ``something that acts like the category of relations in a regular category'' include:

\begin{itemize}%
\item [[allegories]]


\item [[1-category equipped with relations]]



\end{itemize}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[category of correspondences]]


\item [[(infinity,n)-category of correspondences]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item Carboni and Walters, ``Cartesian Bicategories, I''


\item \href{http://rfcwalters.blogspot.com/2009/10/categorical-algebras-of-relations.html}{blog post} showing that any bicategory of relations is an [[allegory]]. Indeed, a bicategory of relations is equivalent to a unitary pretabular allegory.



\end{itemize}
[[!redirects bicategories of relations]]



\end{document}