License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-4361
URL: http://drops.dagstuhl.de/opus/volltexte/2006/436/
Palmgren, Erik

Coequalisers of formal topology

pdf-format:
Dokument 1.pdf (352 KB)

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:DSP:2006:436,
  author =	{Erik Palmgren},
  title =	{Coequalisers of formal topology},
  booktitle =	{Mathematics, Algorithms, Proofs},
  year =	{2006},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran{\c{c}}oise Roy},
  number =	{05021},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2006/436},
  annote =	{Keywords: Formal topology, type theory}
}

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

DROPS-Home | Fulltext Search | Imprint Published by LZI