Three extensional models of type theory

DOI10.1017/S0960129509007440MaRDI QIDQ3625679zbMATH OpenOpenAlexFDO

Authors Benno van den Berg

Publication date 6 May 2009

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129509007440

zbMATH Keywords

\(\Pi W\)-pretopoi\(W\)-typesexact completionsMartin-Löf type theorysetoids

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Categorical logic, topoi (03G30) Topoi (18B25) Categorical semantics of formal languages (18C50)

Recommendations

• Undecidability of equality in the free locally Cartesian closed category
• Inductive types and exact completion
• scientific article; zbMATH DE number 6816943
• Conservativity of equality reflection over intensional type theory
• On the syntax of Martin-Löf's type theories
• Type theories, toposes and constructive set theory: Predicative aspects of AST
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
• Topological and simplicial models of identity types
• scientific article; zbMATH DE number 1301736
• Publication:4715478

Cites work

• A fixpoint theorem for complete categories
• Artin glueing
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• Induction-recursion and initial algebras.
• Inductive types and exact completion
• Locally cartesian closed categories and type theory
• Sheaves in geometry and logic: a first introduction to topos theory
• Some free constructions in realizability and proof theory
• Wellfounded trees in categories

Cited in

(2)

• A Comparison of Type Theory with Set Theory
• Constructing unprejudiced extensional type theories with choices via modalities

This page was built for publication: Three extensional models of type theory

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