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

被引：37
作者：
Moerdijk, I
Palmgren, E
机构：
[1] Uppsala Univ, Dept Math, SE-75106 Uppsala, Sweden
[2] Univ Utrecht, Inst Math, NL-3508 TA Utrecht, Netherlands
来源：
ANNALS OF PURE AND APPLIED LOGIC | 2002年 / 114卷 / 1-3期
基金：
瑞典研究理事会;
关键词：
toposes; pretoposes; small maps; Martin-Lof type theory; constructive set theory;
D O I：
10.1016/S0168-0072(01)00079-3
中图分类号：
O29 [应用数学];
学科分类号：
070104 ;
摘要：
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-Lof 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. (C) 2002 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：155 / 201
页数：47
相关论文
共 23 条
[1]  
ACZEL P, 1986, LOGIC METHODOLOGY PH, V7
[2]  
ACZEL P, 1979, LOG C 77
[3]  
ACZEL P, 1997, UNPUB NOTES CONSTRUC
[4]  
Bunge M., 1979, CAHIERS TOPOLOGIE GE, V20, P373
[5]  
BUTZ C, 1999, BERNAYSGODEL TYPE TH
[6]   Intuitionistic choice and classical logic [J].
Coquand, T ;
Palmgren, E .
ARCHIVE FOR MATHEMATICAL LOGIC, 2000, 39 (01) :53-74
[7]  
Friedman H., 1973, LECT NOTES MATH, P113
[8]  
Hofmann Martin, 1998, Twentyfive years of constructive type theory (Venice, 1995), V36, P83, DOI [10.1093/oso/9780198501275.003.0008, DOI 10.1093/OSO/9780198501275.003.0008]
[9]  
Johnstone Peter, 1977, Topos theory
[10]  
Joyal A., 1995, ALGEBRAIC SET THEORY
123