$U$ -powered category

Given a universe $U$ , a category $𝖢$ is called $U$ -powered iff i.e. every object $𝑥 \in 𝖢$ has a poset of subobjects which is equivalent to one which is $U$ -small, #m/def/cat i.e. $𝖲 𝗎 𝖻 ⇥ 𝖢$ is equivalent to a $U$ -small displayed category.

#state/develop | #lang/en | #m/thm/set