The internal type theory of a Heyting pretopos

DOI10.1007/BFB0097794MaRDI QIDQ4246949zbMATH OpenFDO

Authors Maria Emilia Maietti

Publication date 16 June 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/11577/181926

zbMATH Keywords

dependent typesHeyting pretoposinternal type theorynatural numbers object

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)

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

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: The internal type theory of a Heyting pretopos

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