Category of Subobject Classes is Category

Theorem

Let $\mathbf C$ be a metacategory.

Let $C$ be an object of $\mathbf C$.

Let $\map {\overline {\mathbf {Sub} }_{\mathbf C} } C$ be the category of subobject classes of $C$.

Then $\map {\overline {\mathbf {Sub} }_{\mathbf C} } C$ is a metacategory.

Proof

This needs considerable tedious hard slog to complete it. In particular: A feast of checking well-definedness To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Finish}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.