Categoricity Results of Second-Order ZF in Dependent Type Theory

Saarland University Computer Science

Dominik Kirst, Gert Smolka

We formalise the axiomatic set theory second-order ZF in the constructive type theory of Coq assuming excluded middle. In this setting we prove Zermelo's embedding theorem for models, categoricity in all cardinalities, and the correspondence of inner models and Grothendieck universes. Our results are based on an inductive definition of the cumulative hierarchy eliminating the need for ordinals and transfinite recursion.


Coq Formalisation (Last edit 18.4.2017, Coq version 8.6)