| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 10118864 | Annals of Pure and Applied Logic | 2005 | 27 Pages |
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.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Benno van den Berg,