A globalization of the Hahn-Banach theorem (Q1177237)

The aim of this paper is to reformulate the Hahn-Banach theorem in order to avoid the effects of its dependence on the Axiom of Choice, which is a non-constructive principle. A new form of the theorem is proved in any Grothendieck topos. It provides a result which applies equally to situations involving continuity in parameters and equivalence with respect to a group action. This definition, when applied to the topos of sets, yields precisely the classical version of the Hahn-Banach theorem.