Least dense truth characterizes an open local operator

ID: least-dense-truth-characterizes-an-open-local-operator

For , the dense monomorphism classifier consists of the truth values above , so has least element . Conversely, if it has least element , density of a monomorphism is exactly containment of the pulled-back subterminal . For a subobject , the mono is dense, so and . Since , applying to gives . Hence equality holds.

New to topics? Read the docs here!