From Sets and Types to Topology and Analysis: Towards practicable foundations for constructive mathematics

Description

Content: Introduction Errett Bishop 1. Generalized Inductive Definitions in Constructive Set Theory 2. Constructive Set Theories and their Category-theoretic Models 3. Presheaf models for Constructive Set Theories 4. Universes in Toposes 5. Toward a minimalistic foundation for constructive mathematics 6. Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory 7. Applications of inductive definitions and choice principles to program synthesis 8. The duality of lcassical and constructive notions and proofs 9. Continuity on the real line and in formal spaces 10. Separation Properties in Constructive Topology 11. Spaces as comonoids 12. Predicative exponentiation of locally compact formal topologies over inductively generated ones 13. Some constructive roads to Tychonoff 14. An elementary characterisation of Krull dimension 15. Constructive reverse mathematics: compactness properties 16. Approximating integrable sets by compacts constructively 17. An introduction to the theory of c*-algegras in constructive mathematics 18. Approximations to the numerical range of an element of a Banach algebra 19. The constructive uniqueness of the locally convex topology on rn 20. Computability on Non-Separable Banach Spaces and Landau's Theorem