Type theories, toposes and constructive set theory: predicative aspects of AST
Type theories, toposes and constructive set theory: predicative aspects of AST
复制标题
类型论、倾向和构造性集合论：AST 的预测方面
DOI：
10.1016/s0168-0072(01)00079-3
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Erik Palmgren
中科院分区：
文献类型：
--
作者：
I. Moerdijk;Erik Palmgren
我们介绍了一个预言版本的拓扑（分层pseudotopos）的基础上的概念，小地图代数集理论，开发的Joyal和作者之一。分层伪拓扑的例子可以在马丁-勒夫类型理论中构造，这是一个谓词理论。一个分层的伪拓扑允许层的内部范畴的构造，这又是一个分层的伪拓扑。我们还展示了如何建立模型的Aczel-Myhill建设性集合理论使用这个范畴结构。
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.