Document Open Access Logo

Constructive algebraic integration theory without choice

Author Bas Spitters

Thumbnail PDF


  • Filesize: 283 kB
  • 13 pages

Document Identifiers

Author Details

Bas Spitters

Cite AsGet BibTex

Bas Spitters. Constructive algebraic integration theory without choice. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2006)


We present a constructive algebraic integration theory. The theory is constructive in the sense of Bishop, however we avoid the axiom of countable, or dependent, choice. Thus our results can be interpreted in any topos. Since we avoid impredicative methods the results may also be interpreted in Martin-Löf type theory or in a predicative topos in the sense of Moerdijk and Palmgren. We outline how to develop most of Bishop's theorems on integration theory that do not mention points explicitly. Coquand's constructive version of the Stone representation theorem is an important tool in this process. It is also used to give a new proof of Bishop's spectral theorem.
  • Algebraic integration theory
  • spectral theorem
  • choiceless constructive mathematics
  • pointfree topology


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail