Let $A$, $B$, and $C$ be sets and let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ and $S\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}C$ be relations.
We have
\begin{align*} S_{1}\mathbin {\square }R_{1} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (a,c)\in A\times C\ \middle |\ \begin{aligned} & \text{for each $b\in B$, we have}\\ & \text{$a\sim _{R_{1}}b$ or $b\sim _{S_{1}}c$}\end{aligned} \right\} \\ & \subset \left\{ (a,c)\in A\times C\ \middle |\ \begin{aligned} & \text{for each $b\in B$, we have}\\ & \text{$a\sim _{R_{2}}b$ or $b\sim _{S_{2}}c$}\end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S_{2}\mathbin {\square }R_{2}. \end{align*}
This finishes the proof.
Indeed, we have
\begin{align*} (T\mathbin {\square }S)\mathbin {\square }R & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left(\int _{c\in C}T^{-_{2}}_{c}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}S^{c}_{-_{2}}\right)\mathbin {\square }R\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int _{b\in B}\left(\int _{c\in C}T^{-_{1}}_{c}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}S^{c}_{b}\right)\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}}\\ & = \int _{b\in B}\int _{c\in C}(T^{-_{1}}_{c}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}S^{c}_{b})\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}}\\ & = \int _{c\in C}\int _{b\in B}(T^{-_{1}}_{c}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}S^{c}_{b})\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}}\\ & = \int _{c\in C}\int _{b\in B}T^{-_{1}}_{c}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(S^{c}_{b}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}})\\ & = \int _{c\in C}T^{-_{1}}_{c}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\left(\int _{b\in B}S^{c}_{b}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}}\right)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int _{c\in C}T^{-_{1}}_{c}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(S\mathbin {\square }R)^{c}_{-_{2}}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}T\mathbin {\square }(S\mathbin {\square }R). \end{align*}
In the language of relations, given $a\in A$ and $d\in D$, the stated equality witnesses the equivalence of the following two statements:
-
•
We have $a\sim _{(T\mathbin {\square }S)\mathbin {\square }R}d$, i.e. there exists some $b\in B$ such that:
-
•
We have $a\sim _{R}b$;
-
•
We have $b\sim _{T\mathbin {\square }S}d$, i.e. there exists some $c\in C$ such that:
-
•
We have $b\sim _{S}c$;
-
•
We have $c\sim _{T}d$;
-
•
We have $a\sim _{T\mathbin {\square }(S\mathbin {\square }R)}d$, i.e. there exists some $c\in C$ such that:
-
•
We have $a\sim _{S\mathbin {\square }R}c$, i.e. there exists some $b\in B$ such that:
-
•
We have $a\sim _{R}b$;
-
•
We have $b\sim _{S}c$;
-
•
We have $c\sim _{T}d$;
both of which are equivalent to the statement
-
•
There exist $b\in B$ and $c\in C$ such that $a\sim _{R}b\sim _{S}c\sim _{T}d$.
Indeed, we have
\begin{align*} \nabla _{B}\mathbin {\square }R & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int _{b\in B}(\nabla _{B})^{-_{1}}_{b}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}}\\ & = \bigwedge _{b\in B}(\nabla _{B})^{-_{1}}_{b}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}}\\ & = (\bigwedge _{\substack {b\in B\\ \begin{bgroup} b=-_{1}
\end{bgroup}}}(\nabla _{B})^{-_{1}}_{b}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}})\wedge (\bigwedge _{\substack {b\in B\\ \begin{bgroup} b\neq -_{1}
\end{bgroup}}}(\nabla _{B})^{-_{1}}_{b}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}})\\ & = ((\nabla _{B})^{-_{1}}_{-_{1}}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{-_{1}}_{-_{2}})\wedge (\bigwedge _{\substack {b\in B\\ \begin{bgroup} b\neq -_{1}
\end{bgroup}}}\mathsf{t}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{b}_{-_{2}})\\ & = (\mathsf{f}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}R^{-_{1}}_{-_{2}})\wedge (\bigwedge _{\substack {b\in B\\ \begin{bgroup} b\neq -_{1}
\end{bgroup}}}\mathsf{t})\\ & = R^{-_{1}}_{-_{2}}\wedge \mathsf{t}\\ & = R^{-_{1}}_{-_{2}}, \end{align*}
and
\begin{align*} R\mathbin {\square }\nabla _{A} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int _{a\in A}R^{-_{1}}_{a}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(\nabla _{A})^{a}_{-_{2}}\\ & = \bigwedge _{a\in A}R^{-_{1}}_{a}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(\nabla _{A})^{a}_{-_{2}}\\ & = (\bigwedge _{\substack {a\in A\\ \begin{bgroup} a=-_{2}
\end{bgroup}}}R^{-_{1}}_{a}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(\nabla _{A})^{a}_{-_{2}})\wedge (\bigwedge _{\substack {a\in A\\ \begin{bgroup} a\neq -_{2}
\end{bgroup}}}R^{-_{1}}_{a}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(\nabla _{A})^{a}_{-_{2}})\\ & = (R^{-_{1}}_{-_{2}}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(\nabla _{A})^{-_{2}}_{-_{2}})\wedge (\bigwedge _{\substack {a\in A\\ \begin{bgroup} a\neq -_{2}
\end{bgroup}}}R^{-_{1}}_{a}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\mathsf{t})\\ & = (R^{-_{1}}_{-_{2}}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\mathsf{f})\wedge (\bigwedge _{\substack {a\in A\\ \begin{bgroup} a\neq -_{2}
\end{bgroup}}}\mathsf{t})\\ & = R^{-_{1}}_{-_{2}}\wedge \mathsf{t}\\ & = R^{-_{1}}_{-_{2}}, \end{align*}
This finishes the proof.
Item 4: Relation to Composition of Relations
We proceed in a few steps.
-
•
We have $a\sim _{(S\mathbin {\square }R)^{\textsf{c}}}b$ iff $a\nsim _{S\mathbin {\square }R}b$.
-
•
We have $a\nsim _{S\mathbin {\square }R}b$ iff the assertion “for each $b\in B$, we have $a\sim _{R}b$ or $b\sim _{S}c$” is false.
-
•
That happens iff there exists some $b\in B$ such that $a\nsim _{R}b$ and $b\nsim _{S}c$.
-
•
That happens iff there exists some $b\in B$ such that $a\sim _{R^{\textsf{c}}}b$ and $b\sim _{S^{\textsf{c}}}c$.
The second equality then follows from the first one by Chapter 4: Constructions With Sets, Item 3 of Proposition 4.3.11.1.2.
We have
\begin{align*} T\mathbin {\diamond }(S\mathbin {\square }R) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{there exists some $c\in C$ such}\\ & \text{that $a\sim _{S\mathbin {\square }R}c$ and $c\sim _{T}d$} \end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{there exists some $c\in C$ such that}\\ & \text{$c\sim _{T}d$ and, for each $b\in B$,}\\ & \text{we have $a\sim _{R}b$ or $b\sim _{S}c$}\end{aligned} \right\} \\ & = \left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{the following conditions are satisfied:}\\ & \mkern 20mu\text{1. For each $b\in B$, we have $a\sim _{R}b$ or $b\sim _{S}c$.}\\ & \mkern 20mu\text{2. There exists $c\in C$ such that $c\sim _{T}d$.} \end{aligned} \right\} \\ & \subset \left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{for each $b\in B$, at least one of the}\\ & \text{following conditions is satisfied:}\\ & \mkern 20mu\text{1. We have $a\sim _{R}b$.}\\ & \mkern 20mu\text{2. There exists $c\in C$ such that $b\sim _{S}c$}\\ & \mkern 20mu\phantom{\text{2. }}\text{and $c\sim _{T}d$.} \end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{for each $b\in B$, we have}\\ & \text{$a\sim _{R}b$ or there exists some $c\in C$}\\ & \text{such that $b\sim _{S}c$ and $c\sim _{T}d$}\\ \end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{for each $b\in B$, we have}\\ & \text{$a\sim _{R}b$ or $b\sim _{T\mathbin {\diamond }S}d$}\\ \end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(T\mathbin {\diamond }S)\mathbin {\square }R\end{align*}
and
\begin{align*} (T\mathbin {\square }S)\mathbin {\diamond }R & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$ such}\\ & \text{that $a\sim _{R}b$ and $b\sim _{T\mathbin {\square }S}d$} \end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$ such}\\ & \text{that $a\sim _{R}b$ and, for each $c\in C$,}\\ & \text{we have $b\sim _{S}c$ or $c\sim _{T}d$}\end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$ satisfying}\\ & \text{the following conditions:}\\ & \mkern 20mu\text{1. We have $a\sim _{R}b$.}\\ & \mkern 20mu\text{2. For each $c\in C$, we have $b\sim _{S}c$}\\ & \mkern 20mu\phantom{\text{2. }}\text{or $c\sim _{T}d$.} \end{aligned} \right\} \\ & \subset \left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{for each $c\in C$, at least one of the}\\ & \text{following conditions is satisfied:}\\ & \mkern 20mu\text{1. We have $c\sim _{T}d$.}\\ & \mkern 20mu\text{2. There exists some $b\in B$ such that}\\ & \mkern 20mu\phantom{\text{2. }}\text{we have $a\sim _{R}b$ and $b\sim _{S}c$} \end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{for each $c\in C$, we have $c\sim _{T}d$}\\ & \text{or there exists some $b\in B$, such that}\\ & \text{we have $a\sim _{R}b$ and $b\sim _{S}c$} \end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (d,a)\in D\times A\ \middle |\ \begin{aligned} & \text{for each $c\in C$, we have}\\ & \text{$a\sim _{S\mathbin {\diamond }R}c$ or $c\sim _{T}d$}\end{aligned} \right\} \\ & \subset T\mathbin {\square }(S\mathbin {\diamond }R). \end{align*}
This finishes the proof.
Item 6: Interaction With Converses
This is a repetition of Item 4 of Proposition 8.1.5.1.3 and is proved there.
