From Sets and Types to Topology and Analysis

|s

• 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