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

✍️source

The power object \(P(X)\) of an object \(X\) in a cartesian closed category \({\cal C}\) with subobject classifier \(\Omega \) is defined as the exponential object \(\Omega ^X\).

If \(\Omega ^X\) exists for any \(X\) in \({\cal C}\), we say that \({\cal C}\) has power objects.