  We define a new topos, the Herbrand topos, inspired by the modified
realizability topos and our earlier work on Herbrand realizability. We also
introduce the category of Herbrand assemblies and characterise these as the
double-negation-separated objects in the Herbrand topos. In addition, we show
that the category of sets is included as the category of
double-negation-sheaves and prove that the inclusion functor preserves and
reflects validity of first-order formulas.
