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!