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.