デカルト射

デカルト射の定義を微妙に間違えて理解してたみたいで、改めて考え直してみた。
また迷うのもいやなので、論理式でメモしておく。まだ完全に自信があるわけではないので、間違ってたらごめんなさい＆教えてください。
上の図を見ながらだとわかりやすいかも。

p: E ---> B を関手とする。
E の射 f: X ---> Y が 圏 B の射 u: I ---> J のデカルト射である ⇔

(pf = u) ∧
(∀g∈Mor(E)(∀w∈Mor(B)(((cod g = Y)∧(dom w = p(dom g))∧(cod w = I)∧(w;u = pg))→(∃!h∈Mor(E)((dom h = dom g)∧(cod h = X)∧(ph = w))))))

"∃!" は、「唯一つ存在する」のつもり。関係ないけど、これって論理式でどう書くのかな。めんどくさくなりそう。

追記

「唯一つ存在する」の部分の理解があいまいだったので追記。
任意の g 、任意の w で下(圏 B)が可換三角になったときに、

• 上(E)での三角を可換にする。
• 下(B)に下ろす(関手 p で移す)と w になる。

の二つを満たすような h が上(圏 E)に存在してさらに唯一であるということ。