Three extensional models of type theory

DOI10.1017/S0960129509007440zbMath1184.03070OpenAlexW2105781220MaRDI QIDQ3625679

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

Martin-Löf type theoryexact completionssetoids\(\Pi W\)-pretopoi\(W\)-types

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Inductive types and exact completion
• Sheaves in geometry and logic: a first introduction to topos theory
• Induction-recursion and initial algebras.
• Wellfounded trees in categories
• Artin glueing
• Some free constructions in realizability and proof theory
• A fixpoint theorem for complete categories
• Locally cartesian closed categories and type theory