Type theories, toposes and constructive set theory: Predicative aspects of AST (Q5957856): Difference between revisions

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.