In this thesis we present a formalisation of Tarski-Grothendieck set
theory, that is, Zermelo-Fraenkel set theory with Grothendieck
universes. The development is executed in Coq, extended with the law
of the excluded middle and a powerful choice principle. This yields a
powerful metatheory where the inhabitance of every type is
decidable. From the axiomatisation we develop the usual theory of
sets, including restricted comprehension, ordered pairs, functions and
finite ordinals.
The formalisation is designed to support the construction of
proof-irrelevant, classical models for type theories like the Calculus
of (co)inductive Constructions. The actual model constructions are
left for future work.