scientific article; zbMATH DE number 1301736

MaRDI QIDQ4246949zbMATH OpenFDO

Authors Maria Emilia Maietti

Publication date 16 June 1999

zbMATH Keywords

dependent typesnatural numbers objectinternal type theoryHeyting pretopos

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25)

Recommendations

• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• On the Heyting algebra objects in a topos
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
• scientific article; zbMATH DE number 4187810
• Inductive types and exact completion

Cited in

(3)

• Three extensional models of type theory
• Joyal's arithmetic universes via type theory
• On the Heyting algebra objects in a topos

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4246949)