License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05021.8
URN: urn:nbn:de:0030-drops-4361
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/436/
Go to the corresponding Portal

Palmgren, Erik

Coequalisers of formal topology

pdf-format:
05021.PalmgrenErik.Paper.436.pdf (0.3 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{palmgren:DagSemProc.05021.8,
  author =	{Palmgren, Erik},
  title =	{{Coequalisers of formal topology}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/436},
  URN =		{urn:nbn:de:0030-drops-4361},
  doi =		{10.4230/DagSemProc.05021.8},
  annote =	{Keywords: Formal topology, type theory}
}

Keywords: Formal topology, type theory
Collection: 05021 - Mathematics, Algorithms, Proofs
Issue Date: 2006
Date of publication: 17.01.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI