Ultrapowers as sheaves on a category of ultrafilters (Q1762726)

The category whose objects are sets equipped with a filter, and whose morphisms are equivalence classes (modulo agreement on a set in the filter) of partial functions `respecting' the given filters, has been studied by several authors including V.~Koubek, J.~Reiterman and A. R.~Blass. I.~Moerdijk observed that the category carries a subcanonical `finite covering' topology, so that, provided we impose a suitable size restriction (a complication which is never mentioned in the present paper), we may study the topos of sheaves on it. In the present paper, the author restricts his attention to the full subcategory whose objects are ultrafilters: he observes that the induced Grothendieck topology makes this into an atomic site in the sense of Barr and Diaconescu, and he studies the logical properties of the resulting atomic topos. (In general, the proofs given are rather long-winded: for example, the author gives a detailed proof that the axiom of choice does not hold in the topos, when all that is needed is to observe that -- being two-valued and not equivalent to the category of sets -- it cannot be localic over sets.)