Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets (Q448334)

Comparing Bishop's informal set theory with Lawvere's elementary theory of the category of sets (ETCS), the author proposes a constructive and predicative version of ETCS whose standard model is based on the constructive type theory of Martin-Löf. The theory, CETCS, provides a structuralist foundation for constructive mathematics in the style of Bishop. As one may expect, CETCS is classically equivalent to ETCS plus the Axiom of Choice and the Principle of Excluded Middle. Also, the theory allows to ``reason using elements'' which greatly simplifies its potential application, avoiding most of the rather complex categorical notions. Nevertheless, a purely categorical characterisation of categorical models for CETCS is possible and the author shows it. This characterisation requires to show that the category is locally Cartesian closed, among a few other properties. Since deciding whether a category is locally Cartesian closed apparently requires the use of the Axiom of Choice in the meta-theory, the author reduces this check to the simpler task of verifying the validity of a specific axiom of CETCS. This last result has an independent value from CETCS and may be useful in other contexts.