A Categorical Approach to L-Convexity

• [(i)\implies(ii) ] The adjointness relation implies the following:

  Prooftree.

  (\bigvee x_i)\otimes y\ \geq\ z \bigvee x_i\ \geq\ [y,z] x_i\ \geq\ [y,z]\quad (\forall i) x_i\otimes y\ \geq\ z\phantom{[y,]}\quad (\forall i)

  Thus (\bigvee x_i)\otimes y=\bigvee (x_i\otimes y), as required.

• [(ii)\implies(i) ] First we claim that in order to make the adjointness relation

  Prooftree.

  x\otimes y\ \geq\ z x\ \geq\ [y,z]

  hold for some binary operation [-,-], the value of [y,z] must be the supremum of x’s satisfying x\otimes y\sqsubseteq z, namely,

  \begin{aligned} [y,z]=\bigvee\{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\}. \end{aligned}

  Note that the supremum certainly exists since \mathcal{V}_0 is assumed to be a complete lattice. Suppose [-,-] is a binary operation on \mathcal{V}_0 satisfying the adjointness relation:

  • [\bigvee\{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\}\sqsubseteq[y,z] ] For every x\in \{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\}, x\sqsubseteq [y,z] holds by the adjointness relation, so

    \bigvee\{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\}\sqsubseteq[y,z].

  • [[y,z]\sqsubseteq\bigvee\{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\} ] [y,z]\sqsubseteq [y,z] implies by the adjointness relation that [y,z]\otimes y \sqsubseteq z and hence [y,z]\in \{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\}, thus

    [y,z]\sqsubseteq \bigvee\{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\}.

  Therefore (Proof) is the only possible definition for the operation [-,-]. Conversely, (Proof) implies the adjointness relation:

  • [x\otimes y\sqsubseteq z\implies x\sqsubseteq [y,z] ] Since x\otimes y\sqsubseteq z implies x \in\{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\},

    x\sqsubseteq \bigvee\{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\}=[y,z].

  • [x\sqsubseteq [y,z] \implies x\otimes y\sqsubseteq z ] We first show that [y,z]\otimes y\sqsubseteq z:

    \begin{aligned} [y,z]\otimes y &= \bigvee\{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\}\otimes y \\ &= \bigvee\{x\otimes y\mid x\otimes y\sqsubseteq z\}\\ &\sqsubseteq z. \end{aligned}

    We used the assumption that (-\otimes y) preserves suprema. Using this fact and the monotonicity of \otimes, we conclude

    x\otimes y\sqsubseteq [y,z]\otimes y\sqsubseteq z.

  We now check that the operation [-,-] defined by (Proof) satisfies the axioms required for SC-Ps.

  • [Monotonicity of [-,-] ] Suppose y\sqsupseteq y^\prime and z\sqsubseteq z^\prime hold. Then,

    \{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\} \subseteq \{x\in \mathcal{V}_0\mid x\otimes y^\prime\sqsubseteq z^\prime\}

    because x\otimes y\sqsubseteq z implies x\otimes y^\prime\sqsubseteq x\otimes y \sqsubseteq z\sqsubseteq z^\prime. Therefore

    [y,z]= \bigvee\{x\in \mathcal{V}_0\mid x\otimes y\sqsubseteq z\} \sqsubseteq \bigvee\{x\in \mathcal{V}_0\mid x\otimes y^\prime\sqsubseteq z^\prime\} =[y^\prime,z^\prime],

    as required.

  • [Composition law ] The claim is [y,z]\sqsubseteq [[x,y],[x,z]], namely,

    \bigvee\{w\in \mathcal{V}_0\mid w\otimes y\sqsubseteq z\} \sqsubseteq \bigvee\{w\in \mathcal{V}_0\mid w\otimes [x,y]\sqsubseteq [x,z]\}.

    Thus it suffices to show

    \begin{aligned} \{w\in \mathcal{V}_0\mid w\otimes y\sqsubseteq z\} &\subseteq \{w\in \mathcal{V}_0\mid w\otimes [x,y]\sqsubseteq [x,z]\}\\ &= \big\{w\mid w\otimes \bigvee\{v\mid v\otimes x\sqsubseteq y\}\sqsubseteq\bigvee\{v\mid v\otimes x\sqsubseteq z\}\big\}\\ &= \big\{w\mid \bigvee\{w\otimes v\mid v\otimes x\sqsubseteq y\}\sqsubseteq\bigvee\{v\mid v\otimes x\sqsubseteq z\}\big\} \end{aligned}

    (here we used the assumption that (w\otimes -)=(-\otimes w) preserves suprema). So let us suppose w\otimes y\sqsubseteq z and aim to show that

    \{w\otimes v\mid v\otimes x\sqsubseteq y\}\subseteq\{v\mid v\otimes x\sqsubseteq z\}.

    This holds because for v with v\otimes x\sqsubseteq y,

    (w\otimes v)\otimes x=w\otimes(v\otimes x) \sqsubseteq w\otimes y\sqsubseteq z

    holds.

  • [Unit law for [-,-] ] The claim is z=[e,z]. This reduces to

    \begin{aligned} z&=\bigvee\{x\in \mathcal{V}_0\mid x\otimes e\sqsubseteq z\}\\ &=\bigvee\{x\in \mathcal{V}_0\mid x\sqsubseteq z\}, \end{aligned}

    a trivial equality.

  • [Commutative law for [-,-] ] The claim is x\sqsubseteq[y,z]\iff y\sqsubseteq[x,z], which follows from the following proof tree:

    Prooftree.

    x\ \geq\ [y,z] x\otimes y\ \geq\ z y\otimes x\ \geq\ z y\ \geq\ [x,z]

• [(i)\implies(iii) ] The adjointness relation implies the following:

  Prooftree.

  x\ \geq\ [y,\bigwedge z_i] x\otimes y\ \geq\ \bigwedge z_i x\otimes y\ \geq\ z_i \phantom{[y,]}\quad (\forall i) x\ \geq\ [y,z_i]\quad (\forall i)

  Thus [y,\bigwedge z_i]=\bigwedge [y,z_i], as required.

• [(iii)\implies(i) ] First we claim that in order to make the adjointness relation

  Prooftree.

  x\otimes y\ \geq\ z x\ \geq\ [y,z]

  hold for some binary operation \otimes, the value of x\otimes y must be the infimum of z’s satisfying x\sqsubseteq [y,z], namely,

  \begin{aligned} x\otimes y=\bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\}. \end{aligned}

  Note that the infimum certainly exists since \mathcal{V}_0 is assumed to be a complete lattice. Suppose \otimes is a binary operation on \mathcal{V}_0 satisfying the adjointness relation:

  • [x\otimes y\sqsubseteq \bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\} ] For every z\in \{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\}, x\otimes y\sqsubseteq z holds by the adjointness relation, so

    x\otimes y\sqsubseteq \bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\}.

  • [\bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\}\sqsubseteq x\otimes y ] x\otimes y\sqsubseteq x\otimes y implies by the adjointness relation that x\sqsubseteq [y,x\otimes y] and hence x\otimes y\in \{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\}, thus

    \bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\}\sqsubseteq x\otimes y.

  Therefore (Proof) is the only possible definition for the operation \otimes. Conversely, (Proof) implies the adjointness relation:

  • [x\sqsubseteq [y,z] \implies x\otimes y\sqsubseteq z ] Since x\sqsubseteq [y,z] implies z \in\{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\},

    x\otimes y=\bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\} \sqsubseteq z.

  • [x\otimes y\sqsubseteq z\implies x\sqsubseteq [y,z] ] We first show that x\sqsubseteq [y,x\otimes y]:

    \begin{aligned} [y,x\otimes y] &= [y,\bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\}] \\ &= \bigwedge\{[y,z]\mid x\sqsubseteq [y,z]\}\\ &\sqsupseteq x. \end{aligned}

    We used the assumption that [y,-] preserves infima. Using this fact and the monotonicity of [-,-], we conclude

    x\sqsubseteq [y,x\otimes y]\sqsubseteq [y,z].

  We now check that the operation \otimes defined by (Proof) satisfies the axioms required for SM-Ps.

  • [Monotonicity of \otimes ] Suppose x\sqsubseteq x^\prime and y\sqsubseteq y^\prime hold. Then,

    \{z\in \mathcal{V}_0\mid x^\prime\sqsubseteq [y^\prime,z]\}\subseteq \{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\}

    because x^\prime\sqsubseteq [y^\prime,z] implies x\sqsubseteq x^\prime\sqsubseteq [y^\prime,z]\sqsubseteq [y,z]. Therefore

    x\otimes y= \bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq [y,z]\} \sqsubseteq \bigwedge\{z\in \mathcal{V}_0\mid x^\prime\sqsubseteq [y^\prime,z]\} =x^\prime\otimes y^\prime,

    as required.

  • [Associative law ] The claim is x\otimes(y\otimes z)=(x\otimes y)\otimes z, namely,

    \bigwedge\{w\in \mathcal{V}_0\mid x\sqsubseteq [y\otimes z,w]\} =\bigwedge\{w\in \mathcal{V}_0\mid x\otimes y\sqsubseteq [z,w]\}.

    We prove this by showing \{w\in \mathcal{V}_0\mid x\sqsubseteq [y\otimes z,w]\}=\{w\in \mathcal{V}_0\mid x\otimes y\sqsubseteq [z,w]\}, or more explicitly,

    \begin{aligned} \big\{w\mid x\sqsubseteq [\bigwedge\{v\mid y\sqsubseteq [z,v]\},w]\big\}=\big\{w\mid \bigwedge\{v\mid x\sqsubseteq [y,v]\}\sqsubseteq [z,w]\big\}. \end{aligned}

    Note that by the commutative law for [-,-], (Proof) is equivalent to

    \begin{aligned} \big\{w\mid \bigwedge\{v\mid y\sqsubseteq [z,v]\}\sqsubseteq [x,w]\big\}=\big\{w\mid z\sqsubseteq [\bigwedge\{v\mid x\sqsubseteq [y,v]\},w]\big\}. \end{aligned}

    • [(LHS)\subseteq(RHS) ] We show this in the form of (Proof). It suffices to show

      \begin{aligned} x\sqsubseteq [\bigwedge\{v\mid y\sqsubseteq [z,v]\},w]\implies& [z,w]\in \{v\mid x\sqsubseteq [y,v]\}\\ \big(\iff& x\sqsubseteq [y,[z,w]]\;\,\big) \end{aligned}

      and this follows from

      \begin{aligned} [\bigwedge\{v\mid y\sqsubseteq [z,v]\},w] &\sqsubseteq [[z,\bigwedge\{v\mid y\sqsubseteq [z,v]\}],[z,w]]\\ &= [\bigwedge\{[z,v]\mid y\sqsubseteq [z,v]\},[z,w]]\\ &\sqsubseteq [y,[z,w]], \end{aligned}

      where the first inequality is an instance of the composition law, the equality follows from the inf-preserving property of [z,-], and the last inequality from \bigwedge\{[z,v]\mid y\sqsubseteq [z,v]\}\sqsupseteq y and the monotonicity of [-,-].

    • [(LHS)\supseteq(RHS) ] In this case, we refer to the form (Proof). Now, a sufficient condition is

      \begin{aligned} z\sqsubseteq [\bigwedge\{v\mid x\sqsubseteq [y,v]\},w]\implies& [x,w]\in \{v\mid y\sqsubseteq [z,v]\}\\ \big(\iff& y\sqsubseteq [z,[x,w]]\\ \iff& z\sqsubseteq [y,[x,w]]\;\,\big) \end{aligned}

      and this follows from

      \begin{aligned} [\bigwedge\{v\mid x\sqsubseteq [y,v]\},w] &\sqsubseteq [[x,\bigwedge\{v\mid x\sqsubseteq [y,v]\}],[x,w]]\\ &= [\bigwedge\{[x,v]\mid x\sqsubseteq [y,v]\},[x,w]]\\ &= [\bigwedge\{[x,v]\mid y\sqsubseteq [x,v]\},[x,w]]\\ &\sqsubseteq [y,[x,w]], \end{aligned}

      where the first inequality is an instance of the composition law, the first equality follows from the inf-preserving property of [z,-], and the last inequality from \bigwedge\{[x,v]\mid y\sqsubseteq [x,v]\}\sqsupseteq y and the monotonicity of [-,-].

  • [Unit law for \otimes ] The claim is e\otimes x=x=x\otimes e. Assuming the commutative law for \otimes proved below, it suffices to show x=x\otimes e, namely,

    \begin{aligned} x&=\bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq [e,z]\}\\ &=\bigwedge\{z\in \mathcal{V}_0\mid x\sqsubseteq z\}, \end{aligned}

    which obviously holds.

  • [Commutative law for \otimes ] The claim is x\otimes y=y\otimes x, which follows from the following proof tree:

    Prooftree.

    x\otimes y\ \geq\ z x\ \geq\ [y,z] y\ \geq\ [x,z] y\otimes x\ \geq\ z

    where z is an arbitrary element of \mathcal{V}_0.

• [(i) ] The commutativity of \otimes and sup-preserving property of (-\otimes x) imply the following:

  Prooftree.

  x\otimes(\bigvee y_i)\ \geq\ z (\bigvee y_i)\otimes x\ \geq\ z y_i\otimes x\ \geq\ z\quad\;\; (\forall i) x\otimes y_i\ \geq\ z\quad\;\; (\forall i)

  Thus x\otimes(\bigvee y_i)=\bigvee (x\otimes y_i), as required.

• [(ii) ] The commutativity of [-,-] implies the following:

  Prooftree.

  x\ \geq\ [(\bigvee y_i),z] \bigvee y_i\ \geq\ [x,z] y_i\ \geq\ [x,z]\phantom{y_i}\quad (\forall i) x\ \geq\ [y_i,z]\phantom{x}\quad (\forall i)

  Thus [(\bigvee y_i),z]=\bigwedge [y_i,z], as required.

For all a,a^\prime\in \textup{Ob}(\mathcal{A}), we have

If F is an isomorphism, let G be its inverse. Then for each pair a,a^\prime\in \textup{Ob}(\mathcal{A}),

holds and F is fully faithful. Also, \textup{Ob}(G) witnesses that \textup{Ob}(F) is a bijection as a map.

Suppose then, that F is fully faithful and \textup{Ob}(F) is a bijection. Let \textup{Ob}(G)\colon \textup{Ob}(\mathcal{B})\longrightarrow\textup{Ob}(\mathcal{A}) be the inverse of \textup{Ob}(F) (as a map). Then, for each pair b,b^\prime\in \textup{Ob}(\mathcal{B}),

holds, thus G is also a (fully faithful) \mathcal{V}-functor. By construction, it is clear that G\circ F=1_\mathcal{A} and F\circ G=1_\mathcal{B} hold.

• [Reflexivity ] We wish to prove e\sqsubseteq \textup{Hom}_\mathcal{B}\big(F(a),F(a)\big), but this is an instance of the identity law for \mathcal{B}.

• [Transitivity ] Suppose F\Rightarrow G and G\Rightarrow H for F,G,H\colon \mathcal{A}\longrightarrow \mathcal{B}. Then an application of the composition law for \mathcal{B} yields

  \begin{aligned} e&=e\otimes e\\ &\sqsubseteq \textup{Hom}_\mathcal{B}\big(F(a),G(a)\big)\otimes \textup{Hom}_\mathcal{B}\big(G(a),H(a)\big)\\ &\sqsubseteq \textup{Hom}_\mathcal{B}\big(F(a),H(a)\big). \end{aligned}

• [Composition law ] The claim is

  \textup{Hom}_{\mathcal{A}^\textup{op}}(a,b)\otimes \textup{Hom}_{\mathcal{A}^\textup{op}}(b,c)\sqsubseteq \textup{Hom}_{\mathcal{A}^\textup{op}}(a,c).

  It is proved as follows:

  \begin{aligned} \textup{Hom}_{\mathcal{A}^\textup{op}}(a,b)\otimes \textup{Hom}_{\mathcal{A}^\textup{op}}(b,c) &=\textup{Hom}_{\mathcal{A}}(b,a)\otimes \textup{Hom}_{\mathcal{A}}(c,b)\\ &=\textup{Hom}_{\mathcal{A}}(c,b)\otimes \textup{Hom}_{\mathcal{A}}(b,a)\\ &\sqsubseteq \textup{Hom}_{\mathcal{A}}(c,a)\\ &=\textup{Hom}_{\mathcal{A}^\textup{op}}(a,c). \end{aligned}

• [Identity law ] The claim is e \sqsubseteq\textup{Hom}_{\mathcal{A}^\textup{op}}(a,a), an obvious formula.

• [Composition law ] The claim is [x,y]\otimes[y,z]\sqsubseteq [x,z] for all x,y,z\in \mathcal{V}_0, but this is equivalent to the composition law for SC-Ps, which we know to hold:

  Prooftree.

  [x,y]\otimes[y,z]\ \geq\ [x,z] [y,z]\otimes[x,y]\ \geq\ [x,z] [y,z]\ \geq\ [[x,y],[x,z]]

  Incidentally, this proof tree explains the duplication of the name “composition law.”

• [Identity law ] The claim is e\sqsubseteq [z,z] for all z\in \mathcal{V}_0. Using the commutative law for [-,-], it suffices to show z\sqsubseteq [e,z]. But the unit law for [-,-] states z=[e,z], so the proof is done.

• [Composition law ] The claim is

  \textup{Hom}_{\textup{Fun}(\mathcal{A},\mathcal{B})}(F,G)\otimes \textup{Hom}_{\textup{Fun}(\mathcal{A},\mathcal{B})}(G,H)\sqsubseteq \textup{Hom}_{\textup{Fun}(\mathcal{A},\mathcal{B})}(F,H).

  For each a\in \textup{Ob}(\mathcal{A}), we have

  \begin{aligned} &\textup{Hom}_{\textup{Fun}(\mathcal{A},\mathcal{B})}(F,G)\otimes \textup{Hom}_{\textup{Fun}(\mathcal{A},\mathcal{B})}(G,H)\\ &\qquad= \bigwedge_{a^\prime\in \textup{Ob}(\mathcal{A})} \left\{\textup{Hom}_\mathcal{B}\big(F(a^\prime),G(a^\prime)\big)\right\}\otimes \bigwedge_{a^\prime\in \textup{Ob}(\mathcal{A})} \left\{\textup{Hom}_\mathcal{B}\big(G(a^\prime),H(a^\prime)\big)\right\}\\ &\qquad\sqsubseteq \textup{Hom}_\mathcal{B}\big(F(a),G(a)\big) \otimes \textup{Hom}_\mathcal{B}\big(G(a),H(a)\big)\\ &\qquad\sqsubseteq \textup{Hom}_\mathcal{B}\big(F(a),H(a)\big). \end{aligned}

  Taking the infimum with respect to a, we obtain the required result.

• [Identity law ] The claim is e\sqsubseteq \textup{Hom}_{\textup{Fun}(\mathcal{A},\mathcal{B})}(F,F). The identity law for \mathcal{B} assures

  e\sqsubseteq \textup{Hom}_\mathcal{B}\big(F(a),F(a)\big),

  and the inequality is preserved after we take the infimum with respect to a.

We first show that the values Y(b) and \overline{Y}(a) are indeed a presheaf or a copresheaf, respectively.

• [Y(b) is a presheaf on \mathcal{A}\!\!\! ] The claim is

  \begin{aligned} \textup{Hom}_{\mathcal{A}}(a,a^\prime) &\sqsubseteq [Y(b)(a^\prime),Y(b)(a)] \\ &= [\textup{Hom}_\mathcal{A}(a^\prime,b),\textup{Hom}_\mathcal{A}(a,b)], \end{aligned}

  and this is equivalent to an instance of the composition law for \mathcal{A}:

  Prooftree.

  \textup{Hom}_{\mathcal{A}}(a,a^\prime)\ \geq\ [\textup{Hom}_\mathcal{A}(a^\prime,b),\textup{Hom}_\mathcal{A}(a,b)] \textup{Hom}_{\mathcal{A}}(a,a^\prime)\otimes \textup{Hom}_\mathcal{A}(a^\prime,b)\ \geq\ \textup{Hom}_\mathcal{A}(a,b)

• [\overline{Y}(a) is a copresheaf on \mathcal{A}\!\!\! ] The claim is

  \begin{aligned} \textup{Hom}_{\mathcal{A}}(b,b^\prime) &\sqsubseteq [\overline{Y}(a)(b),\overline{Y}(a)(b^\prime)] \\ &= [\textup{Hom}_\mathcal{A}(a,b),\textup{Hom}_\mathcal{A}(a,b^\prime)], \end{aligned}

  and this is equivalent to an instance of the composition law for \mathcal{A}:

  Prooftree.

  \textup{Hom}_{\mathcal{A}}(b,b^\prime)\ \geq\ [\textup{Hom}_\mathcal{A}(a,b),\textup{Hom}_\mathcal{A}(a,b^\prime)] \textup{Hom}_{\mathcal{A}}(b,b^\prime)\otimes \textup{Hom}_\mathcal{A}(a,b)\ \geq\ \textup{Hom}_\mathcal{A}(a,b^\prime) \textup{Hom}_{\mathcal{A}}(a,b)\otimes \textup{Hom}_\mathcal{A}(b,b^\prime)\ \geq\ \textup{Hom}_\mathcal{A}(a,b^\prime)

Next we show that Y and \overline{Y} are fully faithful \mathcal{V}-functors:

• [Y is a fully faithful \mathcal{V}-functor ] The claim is

  \begin{aligned} \textup{Hom}_{\mathcal{A}}(b,b^\prime) &= \textup{Hom}_{\textup{Fun}(\mathcal{A}^\textup{op},\mathcal{V})}(Y(b),Y(b^\prime)) \\ &= \bigwedge_{a\in \textup{Ob}(\mathcal{A})} \left\{[Y(b)(a),Y(b^\prime)(a)]\right\} \\ &= \bigwedge_{a\in \textup{Ob}(\mathcal{A})} \left\{[\textup{Hom}_\mathcal{A}(a,b),\textup{Hom}_\mathcal{A}(a,b^\prime)]\right\}. \end{aligned}

  We prove this by showing the two inequalities:

  • [\textup{Hom}_{\mathcal{A}}(b,b^\prime) \sqsubseteq \bigwedge_{a\in \textup{Ob}(\mathcal{A})} \left\{[\textup{Hom}_\mathcal{A}(a,b),\textup{Hom}_\mathcal{A}(a,b^\prime)]\right\} ] It is equivalent to

    \textup{Hom}_{\mathcal{A}}(b,b^\prime) \sqsubseteq [\textup{Hom}_\mathcal{A}(a,b),\textup{Hom}_\mathcal{A}(a,b^\prime)]\quad(\forall a\in \textup{Ob}(\mathcal{A}))

    and its proof for some fixed a\in \textup{Ob}(\mathcal{A}) is already given above when we prove that \overline{Y}(a) is a copresheaf on \mathcal{A}.

  • [\bigwedge_{a\in \textup{Ob}(\mathcal{A})} \left\{[\textup{Hom}_\mathcal{A}(a,b),\textup{Hom}_\mathcal{A}(a,b^\prime)]\right\} \sqsubseteq \textup{Hom}_{\mathcal{A}}(b,b^\prime) ] First note that

    \bigwedge_{a\in \textup{Ob}(\mathcal{A})} \left\{[\textup{Hom}_\mathcal{A}(a,b),\textup{Hom}_\mathcal{A}(a,b^\prime)]\right\}\sqsubseteq [\textup{Hom}_\mathcal{A}(b,b),\textup{Hom}_\mathcal{A}(b,b^\prime)]

    holds. Using an instance of the identity law for \mathcal{A}, e\sqsubseteq \textup{Hom}_\mathcal{A}(b,b), we have the following:

    \begin{aligned} [\textup{Hom}_\mathcal{A}(b,b),\textup{Hom}_\mathcal{A}(b,b^\prime)] &\sqsubseteq [e,\textup{Hom}_\mathcal{A}(b,b^\prime)]\\ &= \textup{Hom}_\mathcal{A}(b,b^\prime). \end{aligned}

    Therefore the claim follows.

• [\overline{Y} is a fully faithful \mathcal{V}-functor ] The claim is

  \begin{aligned} \textup{Hom}_{\mathcal{A}}(a,a^\prime) &= \textup{Hom}_{\textup{Fun}(\mathcal{A},\mathcal{V})}(\overline{Y}(a^\prime),\overline{Y}(a)) \\ &= \bigwedge_{b\in \textup{Ob}(\mathcal{A})} \left\{[\overline{Y}(a^\prime)(b),\overline{Y}(a)(b)]\right\} \\ &= \bigwedge_{b\in \textup{Ob}(\mathcal{A})} \left\{[\textup{Hom}_\mathcal{A}(a^\prime,b),\textup{Hom}_\mathcal{A}(a,b)]\right\}. \end{aligned}

  We prove this by showing the two inequalities:

  • [\textup{Hom}_{\mathcal{A}}(a,a^\prime) \sqsubseteq \bigwedge_{b\in \textup{Ob}(\mathcal{A})} \left\{[\textup{Hom}_\mathcal{A}(a^\prime,b),\textup{Hom}_\mathcal{A}(a,b)]\right\} ] It is equivalent to

    \textup{Hom}_{\mathcal{A}}(a,a^\prime) \sqsubseteq [\textup{Hom}_\mathcal{A}(a^\prime,b),\textup{Hom}_\mathcal{A}(a,b)]\quad(\forall b\in \textup{Ob}(\mathcal{A}))

    and its proof for some fixed b\in \textup{Ob}(\mathcal{A}) is already given above when we prove that Y(b) is a presheaf on \mathcal{A}.

  • [\bigwedge_{b\in \textup{Ob}(\mathcal{A})} \left\{[\textup{Hom}_\mathcal{A}(a^\prime,b),\textup{Hom}_\mathcal{A}(a,b)]\right\} \sqsubseteq \textup{Hom}_{\mathcal{A}}(a,a^\prime) ] First note that

    \bigwedge_{b\in \textup{Ob}(\mathcal{A})} \left\{[\textup{Hom}_\mathcal{A}(a^\prime,b),\textup{Hom}_\mathcal{A}(a,b)]\right\}\sqsubseteq [\textup{Hom}_\mathcal{A}(a^\prime,a^\prime),\textup{Hom}_\mathcal{A}(a,a^\prime)]

    holds. Using an instance of the identity law for \mathcal{A}, e\sqsubseteq \textup{Hom}_\mathcal{A}(a^\prime,a^\prime), we have the following:

    \begin{aligned} [\textup{Hom}_\mathcal{A}(a^\prime,a^\prime),\textup{Hom}_\mathcal{A}(a,a^\prime)] &\sqsubseteq [e,\textup{Hom}_\mathcal{A}(a,a^\prime)]\\ &= \textup{Hom}_\mathcal{A}(a,a^\prime). \end{aligned}

    Therefore the claim follows.

When \alpha \in \mathbb{K}, then clearly

If \alpha =-\infty, then

and this is realized as

Finally, if \alpha =\infty, then

and this is written as

Hence, in either case (p-\alpha\cdot\mathbf{1})\in\mathbf{D}_0 by the order and weight completeness of \mathbf{D}.

• [(i) ] Since [\mathcal{A},\overline{\mathbb{K}}]=(\textup{Ob}(\mathcal{A}),[\mathcal{A},\overline{\mathbb{K}}]_0), {\llbracket [\mathcal{A},\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}_0=\{\pi_a\}_{a\in \textup{Ob}(\mathcal{A})}. We claim that

  {\eta_{\mathcal{A}}}\colon\mathcal{A}\longrightarrow{\llbracket [\mathcal{A},\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}

  given by

  \textup{Ob}({\eta_{\mathcal{A}}})\colon\textup{Ob}(\mathcal{A})\longrightarrow{\llbracket [\mathcal{A},\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}_0,\qquad \textup{Ob}({\eta_{\mathcal{A}}})(a)={\eta_{\mathcal{A}}}(a)=\pi_a \quad (\forall a\in \textup{Ob}(\mathcal{A}))

  as a map between the sets of points, is an isomorphism (note that \textup{Ob}({\eta_{\mathcal{A}}})=\pi_{[\mathcal{A},\overline{\mathbb{K}}]}, where \pi_{[\mathcal{A},\overline{\mathbb{K}}]} is the bijection defined in Lemma 3.11). By Proposition 2.20, it suffices to show that {\eta_{\mathcal{A}}} is a fully faithful \overline{\mathbb{K}}-functor (because \textup{Ob}({\eta_{\mathcal{A}}}) is certainly bijective). Therefore, we aim to show

  \begin{aligned} d_\mathcal{A}(a,b) &=d_{{\llbracket [\mathcal{A},\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}}(\pi_a,\pi_b), \end{aligned}

  or equivalently,

  \begin{aligned} d_\mathcal{A}(a,b) &=\sup_{p\in [\mathcal{A},\overline{\mathbb{K}}]_0}\{p(b)-p(a)\}. \end{aligned}

  • [d_\mathcal{A}(a,b) \leq \sup_{p\in [\mathcal{A},\overline{\mathbb{K}}]_0}\{p(b)-p(a)\}\!\!\! ] Recall that \overline{Y}(a) defined by

    \textup{Ob}(\overline{Y}(a))=\lambda b\in \textup{Ob}(\mathcal{A}).\,\textup{Hom}_\mathcal{A}(a,b)

    is an element of [\mathcal{A},\overline{\mathbb{K}}]_0. Therefore,

    d_\mathcal{A}(a,b)-d_\mathcal{A}(a,a)= \overline{Y}(a)(b)-\overline{Y}(a)(a)\leq \sup_{p\in [\mathcal{A},\overline{\mathbb{K}}]_0}\{p(b)-p(a)\}

    and it suffices to show

    d_\mathcal{A}(a,b)\geq d_\mathcal{A}(a,b)-d_\mathcal{A}(a,a),

    but this follows from the identity law 0\geq d_\mathcal{A}(a,a) for \mathcal{A} and the unit law and the monotonicity of -.

  • [d_\mathcal{A}(a,b) \geq \sup_{p\in [\mathcal{A},\overline{\mathbb{K}}]_0}\{p(b)-p(a)\}\!\!\! ] It suffices to show

    d_\mathcal{A}(a,b)\geq p(b)-p(a)

    for each p\in [\mathcal{A},\overline{\mathbb{K}}]_0; but this is nothing but the increasing condition for p.

• [(ii) ] Recall that {\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}=(\{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}},d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}), where

  d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_v,\pi_w) =\sup_{p\in \mathbf{D}_0}\{p(w)-p(v)\}.

  Now, the \overline{\mathbb{K}}-extended L-convex set [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]= (\{\pi_v\}_{v\in{\textup{Ind}(\mathbf{D})}},[{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0) is defined as follows: for all q\in \overline{\mathbb{K}}^{\{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}},

  q\in [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0 \iff d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_v,\pi_w)\geq q(\pi_w)-q(\pi_v)\quad (\forall \pi_v,\pi_w\in \{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}).

  We prove that bijections

  \begin{aligned} {\textup{Ind}({\varepsilon_{\mathbf{D}}})}\colon {\textup{Ind}(\mathbf{D})}\longrightarrow \{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}},\qquad & {\textup{Ind}({\varepsilon_{\mathbf{D}}})}(v)=\pi_v \quad (\forall v\in {\textup{Ind}(\mathbf{D})}),\\ {\textup{Ind}({\varepsilon_{\mathbf{D}}^\prime})}\colon \{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}\longrightarrow {\textup{Ind}(\mathbf{D})},\qquad & {\textup{Ind}({\varepsilon_{\mathbf{D}}^\prime})}(\pi_v)=v\quad (\forall \pi_v\in \{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}) \end{aligned}

  define homomorphisms (note that {\textup{Ind}({\varepsilon_{\mathbf{D}}})}=\pi_\mathbf{D}, where \pi_\mathbf{D} is the bijection defined in the proof of Lemma 3.11); in other words, there are maps

  \begin{aligned} ({\varepsilon_{\mathbf{D}}})_0\colon [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0\longrightarrow \mathbf{D}_0,\quad& ({\varepsilon_{\mathbf{D}}})_0(q)=\lambda v\in {\textup{Ind}(\mathbf{D})}.\, q(\pi_v) \quad (\forall q\in [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0),\\ ({\varepsilon_{\mathbf{D}}^\prime})_0\colon\mathbf{D}_0\longrightarrow [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0,\quad & ({\varepsilon_{\mathbf{D}}^\prime})_0(p)=\lambda \pi_v\in \{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}.\,p(v)\quad (\forall p\in \mathbf{D}_0). \end{aligned}

  To be more specific about the point, we have to verify that the images of the above maps are contained in the codomains.

  • [({\varepsilon_{\mathbf{D}}})_0([{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}, \overline{\mathbb{K}}]_0)\subseteq \mathbf{D}_0\!\!\! ] First we prove that for all images \overline{Y}(\pi_v)\in [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}, \overline{\mathbb{K}}]_0 of the co-Yoneda embedding, ({\varepsilon_{\mathbf{D}}})_0\big(\textup{Ob}(\overline{Y}(\pi_v))\big), abbreviated as ({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big), is an element of \mathbf{D}_0. To see this, observe that

    \begin{aligned} ({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big) &=\lambda w\in {\textup{Ind}(\mathbf{D})}.\,d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_v,\pi_w)\\ &=\lambda w\in {\textup{Ind}(\mathbf{D})}.\,\sup_{p\in \mathbf{D}_0}\{p(w)-p(v)\}, \end{aligned}

    in other words,

    \begin{aligned} ({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big) &=\sup_{p\in \mathbf{D}_0}\{p-p(v)\cdot\textbf{1}\}\\ &=\bigwedge_{p\in \mathbf{D}_0}\{p-p(v)\cdot\textbf{1}\} \end{aligned}

    holds. So the weight and order completeness conditions for \mathbf{D} assure ({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big)\in\mathbf{D}_0.

    Now take arbitrary q\in [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}, \overline{\mathbb{K}}]_0. We have

    d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_v,\pi_w)\geq q(\pi_w)-q(\pi_v)\quad (\forall \pi_v,\pi_w\in \{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}).

    The adjointness relation (for the SMC-CL \overline{\mathbb{K}}) yields

    d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_v,\pi_w) +q(\pi_v)\geq q(\pi_w)\quad (\forall \pi_v,\pi_w\in \{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}),

    so, with respect to the coordinate-wise order on \overline{\mathbb{K}}^{\textup{Ind}(\mathbf{D})} (also denoted by \geq), we obtain

    \begin{aligned} ({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big) +q(\pi_v)\cdot \textbf{1}\geq ({\varepsilon_{\mathbf{D}}})_0(q)\quad (\forall v\in {\textup{Ind}(\mathbf{D})}). \end{aligned}

    Since by the weight completeness ({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big)+q(\pi_v)\cdot \textbf{1} is an element of \mathbf{D}_0, so is

    q^\prime=\inf_{v\in {\textup{Ind}(\mathbf{D})}}\left\{({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big)+q(\pi_v)\cdot \textbf{1}\right\}= \bigvee_{v\in {\textup{Ind}(\mathbf{D})}}\left\{({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big)+q(\pi_v)\cdot \textbf{1}\right\}

    by the order completeness. We claim that q^\prime=({\varepsilon_{\mathbf{D}}})_0(q). Because the definition of q^\prime and (Proof) imply q^\prime\geq ({\varepsilon_{\mathbf{D}}})_0(q), it suffices to show that for each v\in {\textup{Ind}(\mathbf{D})}, q^\prime(v)\leq ({\varepsilon_{\mathbf{D}}})_0(q)(v)=q(\pi_v). This is proved as follows:

    \begin{aligned} q^\prime(v) &=\left(\inf_{v\in {\textup{Ind}(\mathbf{D})}}\left\{({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big)+q(\pi_v)\cdot \textbf{1}\right\}\right)(v)\\ &\leq \left(({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big)+q(\pi_v)\cdot \textbf{1}\right)(v)\\ &=({\varepsilon_{\mathbf{D}}})_0\big(\overline{Y}(\pi_v)\big)(v)+(q(\pi_v)\cdot \textbf{1})(v)\\ &=d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_v,\pi_v)+q(\pi_v)\\ &\leq 0+q(\pi_v)\\ &=q(\pi_v). \end{aligned}

  • [({\varepsilon_{\mathbf{D}}^\prime})_0(\mathbf{D}_0)\subseteq [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}, \overline{\mathbb{K}}]_0\!\!\! ] The condition for ({\varepsilon_{\mathbf{D}}^\prime})_0(p) to be an element of [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}, \overline{\mathbb{K}}]_0 is that

    d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_v,\pi_w)\geq ({\varepsilon_{\mathbf{D}}^\prime})_0(p)(\pi_w)-({\varepsilon_{\mathbf{D}}^\prime})_0(p)(\pi_v)\quad (\forall \pi_v,\pi_w\in \{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}),

    which is equivalent to

    \sup_{p\in \mathbf{D}_0}\{p(w)-p(v)\}\geq p(w)-p(v)\quad (\forall v,w\in {\textup{Ind}(\mathbf{D})}),

    an obvious inequality.

  Therefore, we have two homomorphisms

  \begin{aligned} {\varepsilon_{\mathbf{D}}}&\colon [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]\longrightarrow \mathbf{D},\\ {\varepsilon_{\mathbf{D}}^\prime}&\colon \mathbf{D}\longrightarrow [{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]. \end{aligned}

  Clearly {\textup{Ind}({\varepsilon_{\mathbf{D}}^\prime})}\circ {\textup{Ind}({\varepsilon_{\mathbf{D}}})}=1_{\textup{Ind}(\mathbf{D})} and {\textup{Ind}({\varepsilon_{\mathbf{D}}})}\circ {\textup{Ind}({\varepsilon_{\mathbf{D}}^\prime})}=1_{\{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}} hold, and they are isomorphisms.

• [Order completeness ] Let S be a set of nonexpansive maps from \mathcal{A} to \overline{\mathbb{K}}. The claim is that \bigvee_{p\in S} p, \bigwedge_{p\in S}p are again nonexpansive maps from \mathcal{A} to \overline{\mathbb{K}}. In other words, that

  \begin{aligned} d_\mathcal{A}(a,b) &\geq d_{\overline{\mathbb{K}}}\big(\bigvee_{p\in S} p(a), \bigvee_{p\in S} p(b)\big) =\inf_{p\in S} \{p(b)\}-\inf_{p\in S} \{p(a)\},\\ d_\mathcal{A}(a,b) &\geq d_{\overline{\mathbb{K}}}\big(\bigwedge_{p\in S} p(a),\bigwedge_{p\in S} p(b)\big) =\sup_{p\in S} \{p(b)\}-\sup_{p\in S} \{p(a)\} \end{aligned}

  hold for all a,b\in \textup{Ob}(\mathcal{A}).

  • [(Proof) ] For each fixed p^\prime\in S, the increasing condition implies

    d_\mathcal{A}(a,b)\geq p^\prime(b)-p^\prime(a) \geq \inf_{p\in S} \{p(b)\}-p^\prime (a).

    By taking \sup with respect to p^\prime\in S, we have

    d_\mathcal{A}(a,b)\geq \sup_{p^\prime\in S} \left\{\inf_{p\in S}\{p(b)\}-p^\prime(a)\right\} =\inf_{p\in S} \{p(b)\}-\inf_{p\in S} \{p(a)\},

    where the equality follows from an instance of a statement in Proposition 2.5 that

    \inf_{p\in S} \{p(b)\}-(-)

    turns suprema (\inf’s) into infima (\sup’s).

  • [(Proof) ] For each fixed p^\prime\in S, the increasing condition implies

    d_\mathcal{A}(a,b)\geq p^\prime(b)-p^\prime(a) \geq p^\prime(b)-\sup_{p\in S} \{p(a)\}.

    By taking \sup with respect to p^\prime\in S, we have

    d_\mathcal{A}(a,b)\geq \sup_{p^\prime\in S} \left\{p^\prime(b)-\sup_{p\in S} \{p(a)\}\right\} =\sup_{p\in S} \{p(b)\}-\sup_{p\in S} \{p(a)\},

    where the equality follows from an instance of a statement in Proposition 2.4 that

    (-)-\sup_{p\in S} \{p(a)\}

    preserves infima (\sup’s).

• [Weight completeness (for +) ] Let p be a nonexpansive map from \mathcal{A} to \overline{\mathbb{K}} and \alpha\in \mathbb{K}\cup\{-\infty,\infty\}. The claim is that p+\alpha\cdot\textbf{1} is again a nonexpansive map from \mathcal{A} to \overline{\mathbb{K}}. In other words, that

  \begin{aligned} d_\mathcal{A}(a,b)&\geq d_{\overline{\mathbb{K}}}\big(p(a)+\alpha,p(b)+\alpha\big) =\big(p(b)+\alpha\big)-\big(p(a)+\alpha\big) \end{aligned}

  hold for all a,b\in \textup{Ob}(\mathcal{A}). We use the increasing condition for p

  d_\mathcal{A}(a,b)\geq p(b)-p(a)

  and show

  p(b)-p(a)\geq \big(p(b)+\alpha\big)-\big(p(a)+\alpha\big),

  which has an equivalent formula:

  Prooftree.

  p(b)-p(a)\ \geq\ \big(p(b)+\alpha\big)-\big(p(a)+\alpha\big) \big(p(b)-p(a)\big)+\big(p(a)+\alpha\big) \ \geq\ p(b)+\alpha \big(\big(p(b)-p(a)\big)+p(a)\big)+\alpha \ \geq\ p(b)+\alpha

  Therefore it suffices to prove \big(p(b)-p(a)\big)+p(a)\geq p(b), as follows:

  Prooftree.

  \big(p(b)-p(a)\big)+p(a)\ \geq\ p(b) p(b)-p(a) \ \geq\ p(b)-p(a)

First note that elements of {\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}_0 can canonically be identified with that of {\textup{Ind}(\mathbf{D})}, via a bijection \pi_\mathbf{D} defined as follows:

where

The underlying maps of \pi_v’s are given as the “projection maps”:

See Fig. Proof for an illustration. Thus we may write {\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}_0=\{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}. Also note that

• [Composition law ] The claim is

  d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_u,\pi_v)+ d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_v,\pi_w)\geq d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_u,\pi_w),

  or by (Proof), equivalently,

  \begin{aligned} \sup_{p\in \mathbf{D}_0}\{p(v)-p(u)\}+\sup_{p\in \mathbf{D}_0}\{p(w)-p(v)\} \geq\sup_{p\in \mathbf{D}_0}\{p(w)-p(u)\}. \end{aligned}

  We first prove

  \begin{aligned} \big(p(v)-p(u)\big) + \big(p(w)-p(v)\big)\geq p(w)-p(u) \end{aligned}

  for each p\in \mathbf{D}_0, as follows:

  Prooftree.

  \big(p(v)-p(u)\big) + \big(p(w)-p(v)\big)\ \geq\ p(w)-p(u) \big(p(w)-p(v)\big)+\big(p(v)-p(u)\big) \ \geq\ p(w)-p(u) p(w)-p(v) \ \geq\ \big(p(w)-p(u)\big)-\big(p(v)-p(u)\big)

  where the bottom expression is an instance of the composition law for -. Thus, by taking \sup in (Proof) with respect to p, we have

  \begin{aligned} \sup_{p\in \mathbf{D}_0}\big\{\big(p(v)-p(u)\big) +\big(p(w)-p(v)\big)\big\} \geq\sup_{p\in \mathbf{D}_0}\{p(w)-p(u)\}. \end{aligned}

  On the other hand, we have

  \sup_{p\in \mathbf{D}_0}\{p(v)-p(u)\} +\sup_{p\in \mathbf{D}_0}\{p(w)-p(v)\} \geq\big(p^\prime(v)-p^\prime(u)\big) +\big(p^\prime(w)-p^\prime(v)\big)

  for each p^\prime\in \mathbf{D}_0, and therefore

  \sup_{p\in \mathbf{D}_0}\{p(v)-p(u)\} +\sup_{p\in \mathbf{D}_0}\{p(w)-p(v)\}\geq \sup_{p\in \mathbf{D}_0}\big\{\big(p(v)-p(u)\big) +\big(p(w)-p(v)\big)\big\}.

  We combine this with (Proof) and obtain (Proof).

• [Identity law ] The claim is

  0\geq d_{{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}}(\pi_v,\pi_v),

  or by (Proof), equivalently,

  \begin{aligned} 0\geq\sup_{p\in \mathbf{D}_0}\{p(v)-p(v)\}. \end{aligned}

  First note that for each p\in \mathbf{D}_0

  \begin{aligned} 0\geq p(v)-p(v) \end{aligned}

  holds, as proved below:

  Prooftree.

  0\ \geq\ p(v)-p(v) p(v)\ \geq\ p(v)

  Taking \sup in (Proof) with respect to p yields (Proof).

• [(i) ] Since for each \overline{\mathbb{K}}-functor F\colon\mathcal{A}\longrightarrow\mathcal{B}, [F,\overline{\mathbb{K}}] is defined as

  {\textup{Ind}([F,\overline{\mathbb{K}}])}=\textup{Ob}(F),

  [-,\overline{\mathbb{K}}] is clearly injective.

  To prove surjectivity of [-,\overline{\mathbb{K}}], take an arbitrary homomorphism

  \Phi\colon[\mathcal{B},\overline{\mathbb{K}}]\longrightarrow[\mathcal{A},\overline{\mathbb{K}}].

  Let F_\Phi={\eta_{\mathcal{B}}}^{-1}\circ{\llbracket \Phi,\overline{\mathbb{K}} \rrbracket}\circ{\eta_{\mathcal{A}}}, where \overline{\mathbb{K}}-functors {\eta_{\mathcal{A}}} and {\eta_{\mathcal{B}}} are the isomorphisms defined in the proof of Theorem 3.9 (i):

  The paper has a picture here, which this page does not show.

  We claim that [F_\Phi,\overline{\mathbb{K}}]=\Phi. Recall \textup{Ob}({\llbracket [\mathcal{A},\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket})={\llbracket [\mathcal{A},\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}_0=\{\pi_a\}_{a\in\textup{Ob}(\mathcal{A})} and

  \textup{Ob}({\eta_{\mathcal{A}}})=\pi_{[\mathcal{A},\overline{\mathbb{K}}]}=\lambda a\in\textup{Ob}(\mathcal{A}).\,\pi_a \colon\textup{Ob}(\mathcal{A})\longrightarrow\textup{Ob}({\llbracket [\mathcal{A},\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}).

  Now we can conclude that

  \begin{aligned} {\textup{Ind}([F_\Phi,\overline{\mathbb{K}}])}&=\textup{Ob}(F_\Phi)\\ &=\textup{Ob}({\eta_{\mathcal{B}}})^{-1}\circ\textup{Ob}({\llbracket \Phi,\overline{\mathbb{K}} \rrbracket})\circ\textup{Ob}({\eta_{\mathcal{A}}})\\ &=\textup{Ob}({\eta_{\mathcal{B}}})^{-1}\circ\pi_{[\mathcal{B},\overline{\mathbb{K}}]}\circ{\textup{Ind}(\Phi)}\circ\pi_{[\mathcal{A},\overline{\mathbb{K}}]}^{-1}\circ\textup{Ob}({\eta_{\mathcal{A}}})\\ &=1_{\textup{Ob}(\mathcal{B})}\circ{\textup{Ind}(\Phi)}\circ1_{\textup{Ob}(\mathcal{A})}\\ &={\textup{Ind}(\Phi)}, \end{aligned}

  hence [F_\Phi,\overline{\mathbb{K}}]=\Phi.

• [(ii) ] Since for each homomorphism \Phi\colon\mathbf{D}\longrightarrow\mathbf{E}, {\llbracket \Phi,\overline{\mathbb{K}} \rrbracket} is defined as

  \textup{Ob}({\llbracket \Phi,\overline{\mathbb{K}} \rrbracket})=\pi_\mathbf{D}\circ{\textup{Ind}(\Phi)}\circ\pi_\mathbf{E}^{-1},

  where \pi_\mathbf{D} and \pi_\mathbf{E} are fixed bijections, {\llbracket -,\overline{\mathbb{K}} \rrbracket} is clearly injective.

  To prove surjectivity of {\llbracket -,\overline{\mathbb{K}} \rrbracket}, take an arbitrary \overline{\mathbb{K}}-functor

  F\colon{\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket}\longrightarrow{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}.

  Let \Phi_F={\varepsilon_{\mathbf{E}}}\circ[F,\overline{\mathbb{K}}]\circ{\varepsilon_{\mathbf{D}}}^{-1}, or equivalently, {\textup{Ind}(\Phi_F)}={\textup{Ind}({\varepsilon_{\mathbf{D}}})}^{-1}\circ{\textup{Ind}([F,\overline{\mathbb{K}}])}\circ{\textup{Ind}({\varepsilon_{\mathbf{E}}})}, where homomorphisms {\varepsilon_{\mathbf{D}}} and {\varepsilon_{\mathbf{E}}} are the isomorphisms defined in the proof of Theorem 3.9 (ii):

  The paper has a picture here, which this page does not show.

  We claim that {\llbracket \Phi_F,\overline{\mathbb{K}} \rrbracket}=F. Recall {\textup{Ind}([{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}])}=\textup{Ob}({\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket})={\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}_0=\{\pi_v\}_{v\in{\textup{Ind}(\mathbf{D})}} and

  \begin{aligned} {\textup{Ind}({\varepsilon_{\mathbf{D}}})}=\pi_\mathbf{D}=\lambda v\in{\textup{Ind}(\mathbf{D})}.\,\pi_v\colon {\textup{Ind}(\mathbf{D})}\longrightarrow {\textup{Ind}([{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}])}. \end{aligned}

  Now we can conclude that

  \begin{aligned} \textup{Ob}({\llbracket \Phi_F,\overline{\mathbb{K}} \rrbracket})&= \pi_\mathbf{D}\circ{\textup{Ind}(\Phi_F)}\circ\pi_\mathbf{E}^{-1}\\ &=\pi_\mathbf{D}\circ{\textup{Ind}({\varepsilon_{\mathbf{D}}})}^{-1}\circ{\textup{Ind}([F,\overline{\mathbb{K}}])}\circ{\textup{Ind}({\varepsilon_{\mathbf{E}}})}\circ\pi_\mathbf{E}^{-1}\\ &=1_{{\textup{Ind}([{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}])}}\circ{\textup{Ind}([F,\overline{\mathbb{K}}])}\circ 1_{{\textup{Ind}([{\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}])}}\\ &={\textup{Ind}([F,\overline{\mathbb{K}}])}\\ &=\textup{Ob}(F), \end{aligned}

  hence {\llbracket \Phi_F,\overline{\mathbb{K}} \rrbracket}=F.

Since [\mathcal{B},\overline{\mathbb{K}}]=(\textup{Ob}(\mathcal{B}),[\mathcal{B},\overline{\mathbb{K}}]_0) and [\mathcal{A},\overline{\mathbb{K}}]=(\textup{Ob}(\mathcal{A}),[\mathcal{A},\overline{\mathbb{K}}]_0), a homomorphism from [\mathcal{B},\overline{\mathbb{K}}] to [\mathcal{A},\overline{\mathbb{K}}] is given as a map from {\textup{Ind}([\mathcal{A},\overline{\mathbb{K}}])}=\textup{Ob}(\mathcal{A}) to {\textup{Ind}([\mathcal{B},\overline{\mathbb{K}}])}=\textup{Ob}(\mathcal{B}), such as \textup{Ob}(F); so at least the type matches. What we have to check is that for all p\in[\mathcal{B},\overline{\mathbb{K}}]_0,

is an element of [\mathcal{A},\overline{\mathbb{K}}]_0, i.e., nonexpansive. But (Proof) is a composition of nonexpansive maps and so nonexpansive as well.

Since {\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket}= \big({\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket}_0,d_{\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket}\big) and {\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}= \big({\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}_0,d_{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}\big), a \overline{\mathbb{K}}-functor from {\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket} to {\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket} is given as a map from \textup{Ob}({\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket})={\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket}_0 to \textup{Ob}({\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket})={\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}_0, such as \textup{Ob}({\llbracket \Phi,\overline{\mathbb{K}} \rrbracket})=\pi_\mathbf{D}\circ {\textup{Ind}(\Phi)}\circ \pi_\mathbf{E}^{-1}:

We adopt the notation {\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket}_0=\{\pi_w\}_{w\in {\textup{Ind}(\mathbf{E})}} and {\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}_0=\{\pi_v\}_{v\in {\textup{Ind}(\mathbf{D})}}; then

We aim to show that

or equivalently (by (Proof) in the proof of Lemma 3.11),

Now recall that the condition for {\textup{Ind}(\Phi)} to define a homomorphism is that for all p\in \mathbf{D}_0, p\circ{\textup{Ind}(\Phi)}\in \mathbf{E}_0; hence

and the proof is done.

• [(i), the “only if” part ] Since [F,\overline{\mathbb{K}}],[G,\overline{\mathbb{K}}]\colon[\mathcal{B},\overline{\mathbb{K}}]\longrightarrow[\mathcal{A},\overline{\mathbb{K}}], we aim to prove that for all q\in[\mathcal{B},\overline{\mathbb{K}}]_0,

  q\circ \textup{Ob}(F)(a)\geq q\circ \textup{Ob}(G)(a) \quad(\forall a\in\textup{Ob}(\mathcal{A})).

  In fact, when we view q as a \overline{\mathbb{K}}-functor, it is equivalent to q\circ F\Rightarrow q\circ G, which follows from the fact that \Rightarrow on \overline{\mathbb{K}}-functors is reflexive and preserved under composition.

• [(ii), the “only if” part ] Since {\llbracket \Phi,\overline{\mathbb{K}} \rrbracket},{\llbracket \Psi,\overline{\mathbb{K}} \rrbracket}\colon{\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket}\longrightarrow{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}, we aim to prove that for all \pi_w\in{\llbracket \mathbf{E},\overline{\mathbb{K}} \rrbracket},

  d_{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket}(\pi_{{\textup{Ind}(\Phi)}(w)},\pi_{{\textup{Ind}(\Psi)}(w)})=\sup_{p\in\mathbf{D}_0}\{\Psi_0(p)(w)-\Phi_0(p)(w)\}\leq0.

  Because 0\geq\Psi_0(p)(w)-\Phi_0(p)(w)\iff\Phi_0(p)(w)\geq\Psi_0(p)(w) by

  Prooftree.

  0\ \geq\ \Psi_0(p)(w)-\Phi_0(p)(w) \Phi_0(p)(w)\ \geq\ \Psi_0(p)(w)

  it suffices to show that

  \Phi_0(p)\geq\Psi_0(p)

  holds in \mathbf{E}_0 for all p\in\mathbf{D}_0, but this is nothing but the condition for \Phi\Rightarrow\Psi.

• [(i), the “if” part ] The “only if” part of (ii) implies that {\llbracket [F,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}\Rightarrow{\llbracket [G,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket} holds. By the proof of Theorem 3.13 (i), we have the following commutative diagram:

  The paper has a picture here, which this page does not show.

  and similarly for G. In equations,

  \begin{aligned} F&={\eta_{\mathcal{B}}}^{-1}\circ{\llbracket [F,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}\circ{\eta_{\mathcal{A}}},\\ G&={\eta_{\mathcal{B}}}^{-1}\circ{\llbracket [G,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}\circ{\eta_{\mathcal{A}}}. \end{aligned}

  Since {\eta_{\mathcal{A}}}, {\eta_{\mathcal{B}}} are isomorphisms, we have

  \begin{aligned} d_\mathcal{B}(F(a),G(a))&= d_\mathcal{B}({\eta_{\mathcal{B}}}^{-1}\circ{\llbracket [F,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}\circ{\eta_{\mathcal{A}}}(a),{\eta_{\mathcal{B}}}^{-1}\circ{\llbracket [G,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}\circ{\eta_{\mathcal{A}}}(a))\\ &=d_\mathcal{B}({\eta_{\mathcal{B}}}^{-1}\circ{\llbracket [F,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}(\pi_a),{\eta_{\mathcal{B}}}^{-1}\circ{\llbracket [G,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}(\pi_a))\\ &=d_{\llbracket [\mathcal{B},\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}({\llbracket [F,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}(\pi_a),{\llbracket [G,\overline{\mathbb{K}}],\overline{\mathbb{K}} \rrbracket}(\pi_a))\\ &\leq 0 \end{aligned}

  for all a\in \textup{Ob}(\mathcal{A}).

• [(ii), the “if” part ] The “only if” part of (i) implies that [{\llbracket \Phi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]\Rightarrow[{\llbracket \Psi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}] holds. By the proof of Theorem 3.13 (ii), we have the following commutative diagram:

  The paper has a picture here, which this page does not show.

  and similarly for \Psi. In equations,

  \begin{aligned} \Phi&={\varepsilon_{\mathbf{E}}}\circ[{\llbracket \Phi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]\circ{\varepsilon_{\mathbf{D}}}^{-1},\\ \Psi&={\varepsilon_{\mathbf{E}}}\circ[{\llbracket \Psi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]\circ{\varepsilon_{\mathbf{D}}}^{-1}. \end{aligned}

  We have

  \begin{aligned} \Phi_0(p)(w)&=({\varepsilon_{\mathbf{E}}})_0\circ[{\llbracket \Phi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0\circ({\varepsilon_{\mathbf{D}}}^{-1})_0(p)(w)\\ &=({\varepsilon_{\mathbf{E}}})_0\big([{\llbracket \Phi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0\circ({\varepsilon_{\mathbf{D}}}^{-1})_0(p)\big)(w)\\ &=\big(\lambda w^\prime\in{\textup{Ind}(\mathbf{E})}.\,[{\llbracket \Phi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0\circ({\varepsilon_{\mathbf{D}}}^{-1})_0(p)(\pi_{w^\prime})\big)(w)\\ &=[{\llbracket \Phi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0\circ({\varepsilon_{\mathbf{D}}}^{-1})_0(p)(\pi_w)\\ &=[{\llbracket \Phi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0\big(({\varepsilon_{\mathbf{D}}}^{-1})_0(p)\big)(\pi_w) \end{aligned}

  and

  \Psi_0(p)(w)=[{\llbracket \Psi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0\big(({\varepsilon_{\mathbf{D}}}^{-1})_0(p)\big)(\pi_w)

  for all p\in\mathbf{D}_0 and w\in{\textup{Ind}(\mathbf{E})}. Since ({\varepsilon_{\mathbf{D}}}^{-1})_0(p)\in[{\llbracket \mathbf{D},\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0, we have

  [{\llbracket \Phi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0\big(({\varepsilon_{\mathbf{D}}}^{-1})_0(p)\big)(\pi_w)\geq [{\llbracket \Psi,\overline{\mathbb{K}} \rrbracket},\overline{\mathbb{K}}]_0\big(({\varepsilon_{\mathbf{D}}}^{-1})_0(p)\big)(\pi_w).

  Therefore we obtain \Phi(p)(w)\geq \Psi(p)(w) for all p\in\mathbf{D}_0 and w\in{\textup{Ind}(\mathbf{E})}; so \Phi(p)\geq\Psi(p) for all p\in\mathbf{D}_0; so \Phi\Rightarrow\Psi.