Type theories, toposes and constructive set theory: Predicative aspects of AST
type: Item
instance of: scholarly article
title: Type theories, toposes and constructive set theory: Predicative aspects of AST
zbMATH Open document ID: 0999.03061
DOI: 10.1016/S0168-0072(01)00079-3
author: Ieke Moerdijk
author: Erik Palmgren
published in: Annals of Pure and Applied Logic
publication date: 2002-12-03T00:00:00Z
review text: The correlation between type theories and categorical structures (e.g., simply-typed lambda calculus and Cartesian closed categories) is very significant in categorical logic. The categorical counterpart of higher-order intuitionistic logic is topos theory, which is essentially impredicative in nature. The authors present a categorical counterpart of constructive predicative type theories, such as Martin-Löf's, which is called a ``stratified pseudotopos''. They show that the sheaves on an internal site in a stratified pseudotopos again form such a pseudotopos. They also show that any stratified pseudotopos provides a model of Aczél-Myhill set theory.
reviewed by: Hirokazu Nishimura
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 18B25
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 03F35
zbMATH DE Number: 1719171
zbMATH Keywords: constructive type theory
zbMATH Keywords: predicative type theory
zbMATH Keywords: categorical logic
zbMATH Keywords: topos theory
zbMATH Keywords: sheaves
zbMATH Keywords: stratified pseudotopos
zbMATH Keywords: Aczél-Myhill set theory
MaRDI profile type: Publication
cites work: Q3762311
cites work: Q3869509
cites work: Intuitionistic choice and classical logic
cites work: Q3214890
cites work: Q4247303
cites work: Q4145861
cites work: Q4853985
cites work: Sheaves in geometry and logic: a first introduction to topos theory
cites work: Q4099614
cites work: Q3688389
cites work: Wellfounded trees in categories
cites work: Constructive set theory
cites work: Q4247308
cites work: Q3313859
cites work: Constructivism in mathematics. An introduction. Volume I
cites work: Q4175559
full work available at URL: s0168-0072(01)00079-3
OpenAlex ID: W2121213425
description: scientific article; zbMATH DE number 1719171