definition. power object functor [kostecki2011introduction, 6.8] [tt-004M]

✍️source

The contravariant power object functor \(\mathscr {P}: {\cal C}^{o p} \to {\cal C}\), given by \[\mathscr {P}: X \mapsto \Omega ^X\] for \(X \in \mathrm {Ob}({\cal C})\) and such that \(\mathscr {P}(f): \Omega ^Y \mapsto \Omega ^X\) for \(f: X \to Y\) in \({\cal C}\) is given by \[\mathscr {P}(f)(Y)=\{x \in X \mid f(x) \in Y\}\]

When power object is defined for cartesian closed categories, we have \[ \frac {X \times Y \to \Omega }{Y \to \Omega ^X} \] thus for every category with power objects \[ \operatorname {Hom}(X \times Y, \Omega ) \cong \operatorname {Hom}\left (Y, \Omega ^X\right ) \] This equation, together with lemma [tt-004K] written in the form \(\operatorname {Sub}(X \times Y) \cong \operatorname {Hom}(X \times Y, \Omega )\), gives the isomorphism \[ \operatorname {Sub}(X \times Y) \cong \operatorname {Hom}(Y, \mathscr {P}(X)) \]