Inductive types and exact completion

DOI10.1016/j.apal.2004.09.003zbMath1064.03041OpenAlexW2068946935MaRDI QIDQ556819

Benno van den Berg

Publication date: 23 June 2005

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2004.09.003

zbMATH Keywords

Exact completionInitial algebrasMartin-Löf Type TheoryPretoposesRealizability toposes

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Categorical semantics of formal languages (18C50) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items (8)

Non-well-founded trees in categories ⋮ Flatness, weakly lex colimits, and free exact completions ⋮ Derived rules for predicative set theory: an application of sheaves ⋮ Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets ⋮ EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS ⋮ Aspects of predicative algebraic set theory. I: Exact completion ⋮ Three extensional models of type theory ⋮ W-types in setoids

Cites Work

• Unnamed Item
• Unnamed Item
• A presentation of the initial lift-algebra
• Cocomplete toposes whose exact completions are toposes
• Set theory. An introduction to independence proofs
• The extended calculus of constructions (ECC) with inductive types
• Wellfounded trees in categories
• Locally cartesian closed exact completions
• Some free constructions in realizability and proof theory
• Recursive models for constructive set theories
• Type theories, toposes and constructive set theory: Predicative aspects of AST

This page was built for publication: Inductive types and exact completion