Abstract
We introduce a predicative version of topos (stratified pseudotopos) based on the notion of small maps in algebraic set theory, developed by Joyal and one of the authors. Examples of stratified pseudotoposes can be constructed in Martin-Löf type theory, which is a predicative theory. A stratified pseudotopos admits construction of the internal category of sheaves, which is again a stratified pseudotopos. We also show how to build models of Aczel-Myhill constructive set theory using this categorical structure.
| Original language | English |
|---|---|
| Pages (from-to) | 155-201 |
| Number of pages | 47 |
| Journal | Annals of Pure and Applied Logic |
| Volume | 114 |
| Issue number | 1-3 |
| DOIs | |
| Publication status | Published - 15 Apr 2002 |
Bibliographical note
Funding Information:This paper is part of a series (together with [15, 16]), the research for which was done during mutual visits, supported by the Netherlands Science Organisation (NWO) and the Swedish Research Council for Natural Sciences (NFR), and during a stay at the Mathematisches Forschungsinstitut Oberwolfach, January 18–24, 1998. We are grateful to these three institutions for support. We would like to thank Peter Aczel, for posing the question whether there is a predicative and constructive model of CZF extended with omniscience principles (see Remark 12.9), and Michael Rathjen for helpful discussions on CZF. In addition we are most grateful to the referee for her =his careful comments.
Funding
This paper is part of a series (together with [15, 16]), the research for which was done during mutual visits, supported by the Netherlands Science Organisation (NWO) and the Swedish Research Council for Natural Sciences (NFR), and during a stay at the Mathematisches Forschungsinstitut Oberwolfach, January 18–24, 1998. We are grateful to these three institutions for support. We would like to thank Peter Aczel, for posing the question whether there is a predicative and constructive model of CZF extended with omniscience principles (see Remark 12.9), and Michael Rathjen for helpful discussions on CZF. In addition we are most grateful to the referee for her =his careful comments.
Keywords
- Constructive set theory
- Martin-Löf type theory
- Pretoposes
- Small maps
- Toposes