Type theories, toposes and constructive set theory: Predicative aspects of AST

Ieke Moerdijk; Erik Palmgren

doi:10.1016/S0168-0072(01)00079-3

Type theories, toposes and constructive set theory: Predicative aspects of AST

Ieke Moerdijk, Erik Palmgren^*

^*Corresponding author for this work

Uppsala University

Research output: Contribution to journal › Article › Academic › peer-review

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	https://doi.org/10.1016/S0168-0072(01)00079-3
Publication status	Published - 15 Apr 2002

Keywords

Constructive set theory
Martin-Löf type theory
Pretoposes
Small maps
Toposes

Access to Document

10.1016/S0168-0072(01)00079-3

Cite this

@article{afba0ab3950f49ea87d4f95fe8f00028,

title = "Type theories, toposes and constructive set theory: Predicative aspects of AST",

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{\"o}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.",

keywords = "Constructive set theory, Martin-L{\"o}f type theory, Pretoposes, Small maps, Toposes",

author = "Ieke Moerdijk and Erik Palmgren",

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.",

year = "2002",

month = apr,

day = "15",

doi = "10.1016/S0168-0072(01)00079-3",

language = "English",

volume = "114",

pages = "155--201",

journal = "Annals of Pure and Applied Logic",

issn = "0168-0072",

publisher = "Elsevier",

number = "1-3",

}

TY - JOUR

T1 - Type theories, toposes and constructive set theory

T2 - Predicative aspects of AST

AU - Moerdijk, Ieke

AU - Palmgren, Erik

N1 - 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.

PY - 2002/4/15

Y1 - 2002/4/15

N2 - 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.

AB - 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.

KW - Constructive set theory

KW - Martin-Löf type theory

KW - Pretoposes

KW - Small maps

KW - Toposes

UR - http://www.scopus.com/inward/record.url?scp=0037089746&partnerID=8YFLogxK

U2 - 10.1016/S0168-0072(01)00079-3

DO - 10.1016/S0168-0072(01)00079-3

M3 - Article

AN - SCOPUS:0037089746

SN - 0168-0072

VL - 114

SP - 155

EP - 201

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 1-3

ER -

Type theories, toposes and constructive set theory: Predicative aspects of AST

Abstract

Keywords

Access to Document

Fingerprint

Cite this