プロ関手

$\mu$ について示す。$(\mathrm{Hom}_{\mathcal B}\odot P)(a,b')$ の元は $p\in P(a,b)$ と $k\in\mathcal B(b,b')$ の組の類で、生成関係は $g\colon b\to b''$、$k\in\mathcal B(b'',b')$ について $(g\cdot p,\ k)\sim(p,\ kg)$ である。

• 定義できる。 生成関係の両辺は $k\cdot(g\cdot p)$ と $(kg)\cdot p$ に移り、これらは作用が関手的であることから等しい。
• 逆写像。 $\nu(p)=[p\,|\,1_{b'}]$ と置く。$\mu\nu(p)=1\cdot p=p$。また $g=k$ とした生成関係により $\nu\mu[p\,|\,k]=[k\cdot p\,|\,1_{b'}]=[p\,|\,1_{b'}k]=[p\,|\,k]$ である。よって $\mu$ は全単射である。
• 自然性。 $f\colon a''\to a$、$h\colon b'\to b'''$ について $\mu(h\cdot[p\,|\,k]\cdot f)=\mu[p\cdot f\,|\,hk]=hk\cdot p\cdot f=h\cdot\mu[p\,|\,k]\cdot f$ である。
  $\mu'$ も左右を入れ替えて同じである。生成関係は $u\colon a'\to a''$、$f\in\mathcal A(a,a')$、$p\in P(a'',b)$ について $(uf,\ p)\sim(f,\ p\cdot u)$ で、両辺は $p\cdot(uf)$ に移る。$\nu'(p)=[1_a\,|\,p]$ と置くと $\mu'\nu'=\mathrm{id}$ であり、$u=f$ とした関係から $\nu'\mu'[f\,|\,p]=[1_a\,|\,p\cdot f]=[f\,|\,p]$ となる。$\square$

$Z=\coprod_{b,c}P(a,b)\times Q(b,c)\times R(c,d)$ と置き、$Z$ 上の 2 種類の関係
$$ \text{(i)}\ (g\cdot p,\,q,\,r)\sim(p,\,q\cdot g,\,r)\quad(g\colon b\to b'),\qquad \text{(ii)}\ (p,\,h\cdot q,\,r)\sim(p,\,q,\,r\cdot h)\quad(h\colon c\to c') $$
を考える。集合 $S$ を一つ固定し、$\Phi(S)$ を、(i) と (ii) で結ばれた 2 元に同じ値を与える写像 $Z\to S$ の集合とする。
左辺の集合から $S$ への写像は $\Phi(S)$ と一対一に対応する。 $X=\bigl(R\odot(Q\odot P)\bigr)(a,d)$ は $\coprod_c(Q\odot P)(a,c)\times R(c,d)$ を関係 $(h\cdot x,\,r)\sim(x,\,r\cdot h)$ で割ったものである。写像 $X\to S$ は、各 $c$ と各 $r\in R(c,d)$ ごとの写像 $\psi_{c,r}\colon(Q\odot P)(a,c)\to S$ の族で、$\psi_{c',r}(h\cdot x)=\psi_{c,r\cdot h}(x)$ を満たすものと同じである。各 $\psi_{c,r}$ は、関係 (i) を保つ写像 $\coprod_bP(a,b)\times Q(b,c)\to S$ と同じである。これらを $r$ と $c$ についてまとめると、(i) を保つ写像 $\phi\colon Z\to S$ になる。条件 $\psi_{c',r}(h\cdot x)=\psi_{c,r\cdot h}(x)$ は、$x=[p\,|\,q]$ とすれば $h\cdot x=[p\,|\,h\cdot q]$ なので、$\phi(p,h\cdot q,r)=\phi(p,q,r\cdot h)$、すなわち $\phi$ が (ii) を保つことである。対応は $\phi(p,q,r)=\psi_{c,r}([p\,|\,q])$ で与えられる。
右辺の集合から $S$ への写像も $\Phi(S)$ と一対一に対応する。 $Y=\bigl((R\odot Q)\odot P\bigr)(a,d)$ について、上と左右を入れ替えた同じ議論により、写像 $Y\to S$ は $\phi(p,q,r)=\psi'_{b,p}([q\,|\,r])$ の形で $\Phi(S)$ の元と一対一に対応する。ここでは外側の関係が (i)、内側の関係が (ii) にあたる。
全単射であること。 写像 $\chi\colon X\to Y$、$\bigl[\,[p\,|\,q]\,|\,r\bigr]\mapsto\bigl[p\,|\,[q\,|\,r]\,\bigr]$ は、$Z\to Y$、$(p,q,r)\mapsto\bigl[p\,|\,[q\,|\,r]\,\bigr]$ が (i)・(ii) を保つ（$Y$ の内側と外側の関係そのもの）ので、上の対応により定義できる。逆向きの $\bigl[p\,|\,[q\,|\,r]\,\bigr]\mapsto\bigl[\,[p\,|\,q]\,|\,r\bigr]$ も同様に定義でき、$X,Y$ の元はすべて $Z$ の元の像として書けるので、2 つは互いに逆である。
自然性。 $f\colon a'\to a$、$k\colon d\to d'$ の作用はどちらの側でも $p\mapsto p\cdot f$、$r\mapsto k\cdot r$ なので、$\chi$ と可換である。$\square$

$(P\odot F_*)(a,c)$ は $\coprod_b\mathcal B(Fa,b)\times P(b,c)$ を $(ug,\,p)\sim(g,\,p\cdot u)$（$u\colon b\to b'$）で割ったもので、これは $(P\odot\mathrm{Hom}_{\mathcal B})(Fa,c)$ と同じ集合である。thm-profunctor-unit の $\mu'$ により $P(Fa,c)$ と自然に一対一に対応する。$a$ についての自然性は、$f\colon a'\to a$ の作用が $g\mapsto gF(f)$ であることから従う。$P=G_*$ とすると $G_*(Fa,c)=\mathcal C(GFa,c)=(GF)_*(a,c)$ で、作用も一致する。$\square$

$\eta^*$ はプロ関手の射。 $b$ についての自然性は $(gk)\circ\eta_a=g\circ(k\circ\eta_a)$ である。$f\colon a'\to a$ についての自然性は、$G_*$ の作用 $k\mapsto k\circ G(f)$ と $F_*$ の作用 $k\mapsto k\circ F(f)$ に関する等式 $k\circ G(f)\circ\eta_{a'}=k\circ\eta_a\circ F(f)$ で、$\eta$ の自然性 $G(f)\eta_{a'}=\eta_aF(f)$ から従う。
逆写像。 プロ関手の射 $\varphi\colon G_*\Rightarrow F_*$ に対し、$\eta_a=\varphi_{a,Ga}(1_{Ga})\in\mathcal B(Fa,Ga)$ と置く。$b$ についての自然性を $k\colon Ga\to b$ と元 $1_{Ga}$ に当てると
$$ \varphi_{a,b}(k)=\varphi_{a,b}(k\circ1_{Ga})=k\circ\varphi_{a,Ga}(1_{Ga})=k\circ\eta_a $$
となる（米田の補題 の議論）。したがって $\varphi=\eta^*$ である。$\eta$ が自然変換であることは、$a$ についての自然性を $f\colon a'\to a$ と元 $1_{Ga}\in G_*(a,Ga)$ に当てた式 $\varphi_{a',Ga}(G(f))=\varphi_{a,Ga}(1_{Ga})\circ F(f)$ の左辺が、上の式により $G(f)\circ\eta_{a'}$ に等しいことから従う：$G(f)\eta_{a'}=\eta_aF(f)$。逆に $\eta$ から作った $\eta^*$ について $\eta^*_{a,Ga}(1_{Ga})=\eta_a$ なので、2 つの対応は互いに逆である。
同型について。 対応は合成を保ち（$(\eta'\eta)^*=\eta^*\eta'^*$）、恒等を恒等に送るので、可逆な射どうしが対応する。$\square$