Inductive types and exact completion

Annals of Pure and Applied Logic 134 (2-3):95-121 (2005)
  Copy   BIBTEX

Abstract

Using the theory of exact completions, I construct a certain class of pretoposes, consisting of what one might call “predicative realizability toposes”, that can act as categorical models of certain predicative type theories, including Martin-Löf Type Theory

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2004.09.003

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,990

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Aspects of predicative algebraic set theory I: Exact Completion.Benno van den Berg & Ieke Moerdijk - 2008 - Annals of Pure and Applied Logic 156 (1):123-159.
Type theories, toposes and constructive set theory: predicative aspects of AST.Ieke Moerdijk & Erik Palmgren - 2002 - Annals of Pure and Applied Logic 114 (1-3):155-201.
Exact completion and constructive theories of sets.Jacopo Emmenegger & Erik Palmgren - 2020 - Journal of Symbolic Logic 85 (2):563-584.
More exact completions that are toposes.Matı́as Menni - 2002 - Annals of Pure and Applied Logic 116 (1-3):187-203.
Categorical and algebraic aspects of Martin-löf type theory.Adam Obtułowicz - 1989 - Studia Logica 48 (3):299 - 317.
Predicative functionals and an interpretation of ⌢ID.Jeremy Avigad - 1998 - Annals of Pure and Applied Logic 92 (1):1-34.
Inductive definitions over a predicative arithmetic.Stanley S. Wainer & Richard S. Williams - 2005 - Annals of Pure and Applied Logic 136 (1-2):175-188.
A constructive theory of continuous domains suitable for implementation.Andrej Bauer & Iztok Kavkler - 2009 - Annals of Pure and Applied Logic 159 (3):251-267.
Criteria for exact saturation and singular compactness.Itay Kaplan, Nicholas Ramsey & Saharon Shelah - 2021 - Annals of Pure and Applied Logic 172 (9):102992.
Models of intuitionistic set theory in subtoposes of nested realizability toposes.Samuele Maschio & Thomas Streicher - 2015 - Annals of Pure and Applied Logic 166 (6):729-739.

Analytics

Added to PP
2014-01-16

Downloads
28 (#557,911)

6 months
15 (#233,546)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Benno Van Den Berg
University of Amsterdam

Citations of this work

Non-well-founded trees in categories.Benno van den Berg & Federico De Marchi - 2007 - Annals of Pure and Applied Logic 146 (1):40-59.

View all 6 citations / Add more citations

References found in this work

Wellfounded trees in categories.Ieke Moerdijk & Erik Palmgren - 2000 - Annals of Pure and Applied Logic 104 (1-3):189-218.
Recursive models for constructive set theories.M. Beeson - 1982 - Annals of Mathematical Logic 23 (2-3):127-178.
Recursive models for constructive set theories.N. Beeson - 1982 - Annals of Mathematical Logic 23 (2/3):127.

Add more references