We present the internal type theory of a Heyting pretopos with a natural numbers object. The resulting theory is based on dependent types and proof-terms. We prove that there is a sort of equivalence between such type theories and the category of Heyting pretoposes. By using the type theory we also build the free Heyting pretopos generated by a category.
The internal type theory of an Heyting Pretopos.
MAIETTI, MARIA EMILIA
1998
Abstract
We present the internal type theory of a Heyting pretopos with a natural numbers object. The resulting theory is based on dependent types and proof-terms. We prove that there is a sort of equivalence between such type theories and the category of Heyting pretoposes. By using the type theory we also build the free Heyting pretopos generated by a category.File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
