2006/01/01 by Erik Palmgren, Palmgren, Erik
Computer Science · Mathematics · #Advanced Algebra and Logic #Formal topology #Homotopy and Cohomology in Algebraic Topology #Logic, programming, and type systems #type theory
paper · doi:10.4230/dagsemproc.05021.8
openalex publication_date 2006/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We give a predicative construction of quotients of formal topologies. Along with earlier results on the match up between of continuous functions on real numbers (in the sense of Bishop's constructive mathematics) and approximable mappings on the formal space of reals, we argue that formal topology gives an adequate foundation for constructive algebraic topology, also in the predicative sense. Predicativity is of essence when formalising the subject in logical frameworks based on Martin-Löf type theories.