A sieve on U is asubfunctor of the representable functoryU, equivalently a family of arrows into U closed under precomposition. For f:V→U, the pullback sieve consists of arrows g into V for which fg belongs to the original sieve.
A sieve R on A is dense when every arrow f:B→Ahas 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.