We have
\begin{align*} S_{1}\mathbin {\diamond }R_{1} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (a,c)\in A\times C\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$, such}\\ & \text{that $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{there exists some $b\in B$, such}\\ & \text{that $a\sim _{R_{2}}b$ or $b\sim _{S_{2}}c$}\end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S_{2}\mathbin {\diamond }R_{2}. \end{align*}
This finishes the proof.
Item 2: Associativity, Proof I
Indeed, we have
\begin{align*} (T\mathbin {\diamond }S)\mathbin {\diamond }R & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(\int ^{c\in C}T^{-_{1}}_{c}\times S^{c}_{-_{2}})\mathbin {\diamond }R\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int ^{b\in B}(\int ^{c\in C}T^{-_{1}}_{c}\times S^{c}_{b})\times R^{b}_{-_{2}}\\ & = \int ^{b\in B}\int ^{c\in C}(T^{-_{1}}_{c}\times S^{c}_{b})\times R^{b}_{-_{2}}\\ & = \int ^{c\in C}\int ^{b\in B}(T^{-_{1}}_{c}\times S^{c}_{b})\times R^{b}_{-_{2}}\\ & = \int ^{c\in C}\int ^{b\in B}T^{-_{1}}_{c}\times (S^{c}_{b}\times R^{b}_{-_{2}})\\ & = \int ^{c\in C}T^{-_{1}}_{c}\times (\int ^{b\in B}S^{c}_{b}\times R^{b}_{-_{2}})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int ^{c\in C}T^{-_{1}}_{c}\times (S\mathbin {\diamond }R)^{c}_{-_{2}}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}T\mathbin {\diamond }(S\mathbin {\diamond }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:
-
1.
We have $a\sim _{(T\mathbin {\diamond }S)\mathbin {\diamond }R}d$, i.e. there exists some $b\in B$ such that:
-
•
We have $a\sim _{R}b$;
-
•
We have $b\sim _{T\mathbin {\diamond }S}d$, i.e. there exists some $c\in C$ such that:
-
•
We have $b\sim _{S}c$;
-
•
We have $c\sim _{T}d$;
-
2.
We have $a\sim _{T\mathbin {\diamond }(S\mathbin {\diamond }R)}d$, i.e. there exists some $c\in C$ such that:
-
•
We have $a\sim _{S\mathbin {\diamond }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$.
Item 2: Associativity, Proof II
Using Item 3 of Definition 8.1.3.1.1, we have
\begin{align*} [(T\mathbin {\diamond }S)\mathbin {\diamond }R](a) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{b\in R(a)}(T\mathbin {\diamond }S)(b)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{b\in R(a)}\bigcup _{c\in S(b)}T(c) \end{align*}
on the one hand and
\begin{align*} [T\mathbin {\diamond }(S\mathbin {\diamond }R)](a) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{c\in [S\mathbin {\diamond }R](a)}T(c)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{c\in \bigcup _{b\in R(a)}S(b)}T(c) \end{align*}
on the other, so we want to prove an equality of the form
\[ \bigcup _{b\in R(a)}\bigcup _{c\in S(b)}T(c)=\bigcup _{c\in \bigcup _{b\in R(a)}S(b)}T(c). \]
This then follows from an application of Chapter 4: Constructions With Sets, Item 2 of Proposition 4.3.6.1.2 in which we consider $X=D$, consider $\mathcal{P}(\mathcal{P}(\mathcal{P}(D)))$, take $U=U_{c}=T(c)$, take $A$ to be
\[ A_{b}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ T(c)\in \mathcal{P}(D)\ \middle |\ c\in S(b)\right\} , \]
and then finally take
\begin{align*} \mathcal{A} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ A_{b}\in \mathcal{P}(\mathcal{P}(D))\ \middle |\ b\in R(a)\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \left\{ T(c)\in \mathcal{P}(D)\ \middle |\ c\in S(b)\right\} \ \middle |\ b\in R(a)\right\} . \end{align*}
Indeed, we have
\begin{align*} \bigcup _{A\in \mathcal{A}}(\bigcup _{U\in A}U) & = \bigcup _{A_{b}\in \mathcal{A}}(\bigcup _{c\in S(b)}T(c))\\ & = \bigcup _{b\in R(a)}(\bigcup _{c\in S(b)}T(c)) \end{align*}
and
\begin{align*} \bigcup _{U\in \bigcup _{A\in \mathcal{A}}A}U & = \bigcup _{U_{c}\in \bigcup _{b\in R(a)}A_{b}}U_{c}\\ & = \bigcup _{T(c)\in \bigcup _{b\in R(a)}A_{b}}T(c)\\ & = \bigcup _{c\in \bigcup _{b\in R(a)}S(b)}T(c).\end{align*}
This finishes the proof.
Indeed, we have
\begin{align*} \Delta _{B}\mathbin {\diamond }R & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int ^{b\in B}(\Delta _{B})^{-_{1}}_{b}\times R^{b}_{-_{2}}\\ & = \bigvee _{b\in B}(\Delta _{B})^{-_{1}}_{b}\times R^{b}_{-_{2}}\\ & = \bigvee _{\substack {b\in B\\ \begin{bgroup} b=-_{1}
\end{bgroup}}}R^{b}_{-_{2}}\\ & = R^{-_{1}}_{-_{2}}, \end{align*}
and
\begin{align*} R\mathbin {\diamond }\Delta _{A} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int ^{a\in A}R^{-_{1}}_{a}\times (\Delta _{A})^{a}_{-_{2}}\\ & = \bigvee _{a\in B}R^{-_{1}}_{a}\times (\Delta _{A})^{a}_{-_{2}}\\ & = \bigvee _{\substack {a\in B\\ \begin{bgroup} a=-_{2}
\end{bgroup}}}R^{-_{1}}_{a}\\ & = R^{-_{1}}_{-_{2}}. \end{align*}
In the language of relations, given $a\in A$ and $b\in B$:
-
•
The equality
\[ \Delta _{B}\mathbin {\diamond }R=R \]
witnesses the equivalence of the following two statements:
-
•
We have $a\sim _{b}B$.
-
•
There exists some $b'\in B$ such that:
-
•
We have $a\sim _{R}b'$
-
•
We have $b'\sim _{\Delta _{B}}b$, i.e. $b'=b$.
-
•
The equality
\[ R\mathbin {\diamond }\Delta _{A}=R \]
witnesses the equivalence of the following two statements:
-
•
There exists some $a'\in A$ such that:
-
•
We have $a\sim _{\Delta _{B}}a'$, i.e. $a=a'$.
-
•
We have $a'\sim _{R}b$
-
•
We have $a\sim _{b}B$.
Item 4: Relation to Apartness Composition of Relations
This is a repetition of Item 4 of Proposition 8.1.4.1.3 and is proved there.
This is a repetition of Item 5 of Proposition 8.1.4.1.3 and is proved there.
Item 6: Interaction With Converses
This is a repetition of Item 3 of Proposition 8.1.5.1.3 and is proved there.
Item 7: Interaction With Ranges and Domains
We have
\begin{align*} \operatorname {Dom}(S\mathbin {\diamond }R) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ a\in A\ \middle |\ a\sim _{S\mathbin {\diamond }R}c\text{ for some $c\in C$}\right\} ,\\ & = \left\{ a\in A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$ and $c\in C$}\\ & \text{such that $a\sim _{R}b$ and $b\sim _{R}c$} \end{aligned} \right\} ,\\ & \subset \left\{ a\in A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$}\\ & \text{such that $a\sim _{R}b$} \end{aligned} \right\} ,\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {Dom}(R) \end{align*}
and
\begin{align*} \mathrm{Im}(S\mathbin {\diamond }R) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ c\in C\ \middle |\ a\sim _{S\mathbin {\diamond }R}c\text{ for some $a\in A$}\right\} ,\\ & = \left\{ c\in C\ \middle |\ \begin{aligned} & \text{there exists some $a\in A$ and $b\in B$}\\ & \text{such that $a\sim _{R}b$ and $b\sim _{R}c$} \end{aligned} \right\} ,\\ & \subset \left\{ c\in C\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$}\\ & \text{such that $b\sim _{S}c$} \end{aligned} \right\} ,\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Im}(S). \end{align*}
This finishes the proof.
\begin{align*} [\operatorname {\mathrm{Lan}}_{\chi _{B}}(S)](V) & \cong \int ^{b\in B}\chi _{\mathcal{P}(B)}(\chi _{b},V)\odot S(b)\\ & \cong \int ^{b\in B}\chi _{V}(b)\odot S(b)\\ & \cong \bigcup _{b\in B}\chi _{V}(b)\odot S(b)\\ & \cong \bigcup _{b\in V}S(b) \end{align*}
