Title of article
Inductive types and exact completion
Author/Authors
van den Berg، نويسنده , , Benno، نويسنده ,
Issue Information
روزنامه با شماره پیاپی سال 2005
Pages
27
From page
95
To page
121
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.
Keywords
Realizability toposes , Exact completion , Initial algebras , Pretoposes , Martin-Lِf Type Theory
Journal title
Annals of Pure and Applied Logic
Serial Year
2005
Journal title
Annals of Pure and Applied Logic
Record number
1443647
Link To Document