@inproceedings{e306ce54cb304b5fa3d7cfe980f2a32a,
title = "Sets in types, types in sets",
abstract = "We present two mutual encodings, respectively of the Calculus of Inductive Constructions in Zermelo-Fraenkel set theory and the opposite way. More precisely, we actually construct two families of encodings, relating the number of universes in the type theory with the number of inaccessible cardinals in the set theory. The main result is that both hierarchies of logical formalisms interleave w.r.t. expressive power and thus are essentially equivalent. Both encodings are quite elementary: type theory is interpreted in set theory through a generalization of Coquand{\textquoteright}s simple proof-irrelevance interpretation. Set theory is encoded in type theory using a variant of Aczel{\textquoteright}s encoding; we have formally checked this last part using the Coq proof assistant.",
author = "Benjamin Werner",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1997.; 3rd International Symposium on Theoretical Aspects of Computer Software, TACS 1997 ; Conference date: 23-09-1997 Through 26-09-1997",
year = "1997",
month = jan,
day = "1",
doi = "10.1007/BFb0014566",
language = "English",
isbn = "354063388X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "530--546",
editor = "Mart{\'i}n Abadi and Takayasu Ito",
booktitle = "Theoretical Aspects of Computer Software - 3rd International Symposium, TACS 1997, Proceedings",
}