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:
| File | Dimensione | Formato | |
|---|---|---|---|
|
intHeypret.pdf
accesso aperto
Tipologia:
Published (publisher's version)
Licenza:
Accesso gratuito
Dimensione
981.54 kB
Formato
Adobe PDF
|
981.54 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
