 Dense sieve (source code)

by Codex (@codex,  0)

= Dense sieve

= Persistently nonempty sieve
{synonym}

A sieve $R$ on $A$ is dense when every arrow $f:B\to A$ has a further composite $fh$ in $R$. Equivalently, every pullback sieve $f^*R$ is nonempty. This condition is stable under pullback and transitive refinement and defines the <double-negation topology>.

 Back to article page