トポスでのベキ集合関手

この記事の証明は難しいとしても、ベキ集合の存在ぐらいは知っておいたほうがいいかなとやり始めたら全然できないのでガックリきました。
仕方ないので色々調べまわってやっと見つけました。先の記事にもあった、TOPOSES, TRIPLES AND THEORIES (Barr, Wells. PDF)

  • 3. Properties of Toposes
  • 3.1. Functoriality of P.
  • 3.3. Proposition. P has a unique extension to a functor from Eop to E ...

あたりに載っています。

でも、要するに、

        f
 A ------------> B
 |               |
 | {.}A          | {.}B
 |               |
 v               v
ΩA <----------> ΩB

を可換にする下段左向きの射を見つけるだけなんですけど、簡単に出ないのかなぁ、これ。トポスの計算に不慣れすぎる。
ちなみに、下段右向きもあるはずで、それは共変版のベキ集合関手になります。たぶん。これも簡単に出ないかなぁ。誰かご存知でしたら教えてください。