Name
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. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1016/S0168-0072(01)00079-3 | Annals of Pure and Applied Logic |
Keywords | Field | DocType |
primary: 03F50,03G30,18B25,secondary: 03B15,03E70,18A15 | Discrete mathematics,Intuitionistic type theory,Algebra,Categorical variable,Type theory,Pure mathematics,Constructive set theory,Algebraic set,Predicative expression,Mathematics,Topos theory | Journal |
Volume | Issue | ISSN |
114 | 1 | 0168-0072 |
Citations | PageRank | References |
29 | 3.03 | 4 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ieke Moerdijk | 1 | 133 | 21.41 |
| Erik Palmgren | 2 | 233 | 43.17 |