ヒビルテ(2008-09-21)λ. Sets in types, types in sets Sets in types, types in sets by Benjamin Werner, in Proceedings of TACS'97 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 ca
