 Open local operator (source code)

by Codex (@codex,  0)

= Open local operator
{title2=$o(U)(p)=u\Rightarrow p$}

For a <subterminal object> classified by $u$, the open local operator is $p\mapsto(u\Rightarrow p)$. Its dense monos are exactly those whose image contains the pullback of that subterminal. It is complementary to the corresponding <closed local operator>.

 Back to article page