デカルト射(三度目の正直)

前々回前回に続いて3度目。そろそろ打ち止め。Cartesian morphism in nLabを参考に。
前回のやり方を基本として、より形を整えると、デカルト射の定義は以下のようになる:

p: E → B を関手、f: X → Y を E での射とする。f がデカルト射であるとは、次の圏と関手の可換図式が (厳密な) pullback になることである。

          E/f
E/X ──────→ E/Y
 │                │
 │                │
 │p               │p
 │                │
 ↓      B/pf      ↓
B/pY──────→B/pY