Quotient topologies in constructive set theory and type theory

&
Annals of Pure and Applied Logic 141 (1):257-265 (2006)
  Copy   BIBTEX

Abstract

The standard construction of quotient spaces in topology uses full separation and power sets. We show how to make this construction using only the predicative methods available in constructive type theory and constructive set theory

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2005.11.005

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 100,793

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Aspects of general topology in constructive set theory.Peter Aczel - 2006 - Annals of Pure and Applied Logic 137 (1-3):3-29.
Aspects of general topology in constructive set theory.Peter Azcel - 2006 - Annals of Pure and Applied Logic 137 (1-3):3-29.
Type theories, toposes and constructive set theory: predicative aspects of AST.Ieke Moerdijk & Erik Palmgren - 2002 - Annals of Pure and Applied Logic 114 (1-3):155-201.
On the T 1 axiom and other separation properties in constructive point-free and point-set topology.Peter Aczel & Giovanni Curi - 2010 - Annals of Pure and Applied Logic 161 (4):560-569.
A minimalist two-level foundation for constructive mathematics.Maria Emilia Maietti - 2009 - Annals of Pure and Applied Logic 160 (3):319-354.
Topological inductive definitions.Giovanni Curi - 2012 - Annals of Pure and Applied Logic 163 (11):1471-1483.
Apartness spaces as a framework for constructive topology.Douglas Bridges & Luminiţa Vîţă - 2003 - Annals of Pure and Applied Logic 119 (1-3):61-83.
Apartness spaces as a framework for constructive topology.Douglas Bridges & Luminia Vî - 2003 - Annals of Pure and Applied Logic 119 (1-3):61-83.
Non-deterministic inductive definitions.Benno van den Berg - 2013 - Archive for Mathematical Logic 52 (1-2):113-135.
On some peculiar aspects of the constructive theory of point-free spaces.Giovanni Curi - 2010 - Mathematical Logic Quarterly 56 (4):375-387.

Analytics

Added to PP
2013-12-31

Downloads
38 (#571,706)

6 months
5 (#1,012,768)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Quasi-apartness and neighbourhood spaces.Hajime Ishihara, Ray Mines, Peter Schuster & Luminiţa Vîţă - 2006 - Annals of Pure and Applied Logic 141 (1):296-306.
Relating Bishopʼs function spaces to neighbourhood spaces.Hajime Ishihara - 2013 - Annals of Pure and Applied Logic 164 (4):482-490.

Add more citations

References found in this work

Constructive set theory.John Myhill - 1975 - Journal of Symbolic Logic 40 (3):347-382.
The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Inaccessible set axioms may have little consistency strength.L. Crosilla & M. Rathjen - 2002 - Annals of Pure and Applied Logic 115 (1-3):33-70.

View all 7 references / Add more references