Categorical and algebraic aspects of Martin-Löf type theory

DOI10.1007/BF00370827zbMath0714.03050OpenAlexW2030950371MaRDI QIDQ750438

Adam Obtułowicz

Publication date: 1989

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00370827

zbMATH Keywords

lambda calculusCartesian closed categoryindexed categoryMartin- Löf Type Theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40)

Related Items

Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Generalized algebraic theories and contextual categories
• On the syntax of Martin-Löf's type theories
• Locally cartesian closed categories and type theory
• Recursive models for constructive set theories
• Aspects of topoi