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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,423

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

Quotient Completion for the Foundation of Constructive Mathematics.Maria Emilia Maietti & Giuseppe Rosolini - 2013 - Logica Universalis 7 (3):371-402.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
Inaccessibility in constructive set theory and type theory.Michael Rathjen, Edward R. Griffor & Erik Palmgren - 1998 - Annals of Pure and Applied Logic 94 (1-3):181-200.
The inconsistency of higher order extensions of Martin-löf's type theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
Intuitionistic choice and classical logic.Thierry Coquand & Erik Palmgren - 2000 - Archive for Mathematical Logic 39 (1):53-74.
Syntactic calculus with dependent types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.
On some peculiar aspects of the constructive theory of point-free spaces.Giovanni Curi - 2010 - Mathematical Logic Quarterly 56 (4):375-387.
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.
Realizing Mahlo set theory in type theory.Michael Rathjen - 2003 - Archive for Mathematical Logic 42 (1):89-101.
Assertion and grounding: a theory of assertion for constructive type theory.Maria Schaar - 2011 - Synthese 183 (2):187-210.
Assertion and grounding: a theory of assertion for constructive type theory.Maria van der Schaar - 2011 - Synthese 183 (2):187-210.
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
The strength of Martin-Löf type theory with a superuniverse. Part II.Michael Rathjen - 2001 - Archive for Mathematical Logic 40 (3):207-233.
The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.

Analytics

Added to PP
2013-12-31

Downloads
19 (#781,160)

6 months
4 (#800,606)

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