Three extensional models of type theory
From MaRDI portal
Publication:3625679
DOI10.1017/S0960129509007440zbMath1184.03070MaRDI QIDQ3625679
Publication date: 6 May 2009
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
03G30: Categorical logic, topoi
18B25: Topoi
18C50: Categorical semantics of formal languages
03F65: Other constructive mathematics
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