Sets in Coq, Coq in Sets

Barras, Bruno; INRIA Saclay - France
This work is about formalizing models of various type theories of the Calculus of Constructions family. Here we focus on set theoretical models. The long-term goal is to build a formal set theoretical model of the Calculus of Inductive Constructions, so we can be sure that Coq is consistent with the language used by most mathematicians. One aspect of this work is to axiomatize several set theories: ZF possibly with inaccessible cardinals, and HF, the...