CatDat

subobject classifier

A category C\mathcal{C} has a subobject classifier if it has finite limits and a monomorphism :1Ω\top : 1 \to \Omega from the terminal object such that for every monomorphism m:ABm : A \to B there is a unique morphism χm:BΩ\chi_m : B \to \Omega such that BA1B \leftarrow A \rightarrow 1 is the pullback of BΩ1B \rightarrow \Omega \leftarrow 1. Equivalently, the functor Sub:CopSet+\mathrm{Sub} : \mathcal{C}^{\mathrm{op}} \to \mathbf{Set}^+ is representable.

Relevant implications

Examples

Counterexamples

Unknown

For these categories the database has no info if they satisfy this property or not.