Teorija tipov za sintetične kategorije

In this thesis, we study the interactions of dependent type theory and synthetic category theory. Our main goal is to formally express the axioms of synthetic category theory as type-theoretic derivation rules. In the first chapter, we present a detailed account of Grothendieck-Maltsiniotis $omega$-categories, an algebraic notion of higher categories, which can be recovered syntactically as models of the type theory CaTT, which we present in the second chapter. We introduce an analogous notion of $(omega,n)$-categories, together with a family of corresponding type theories, which we prove again recover the notion syntactically. In the third chapter, we formalize fully coherent universal properties of categorical constructions, extending modified CaTT with additional term construction rules. To this end, we introduce the framework of type morphisms and pointwise homotopies, and study the functoriality properties of the whiskering and product constructions. We implement the crucial parts of the third chapter in the computer proof assistant Agda.