20.500.12556/RUL-171821 A type theory for synthetic categories master's thesis 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. V magistrskem delu raziskujemo povezave med teorijo odvisnih tipov in sintetično teorijo kategorij. Naš glavni cilj je formalno izraziti aksiome sintetične teorije kategorij kot pravila sklepanja v teoriji tipov. V prvem poglavju podamo podroben prikaz Grothendieck-Maltsiniotisovih $\omega$-kategorij. Ta algebraični model višjih kategorij lahko ekvivalentno predstavimo tudi sintaktično, kot modele teorije tipov CaTT, ki jo obravnavamo v drugem poglavju. Vpeljemo analogno definicijo $(\omega,n)$-kategorij, skupaj z družino teorij tipov, in tudi zanje dokažemo korespondenco med sintakso in semantiko. V tretjem poglavju modificirano CaTT razširimo z dodatnimi pravili za konstrukcijo termov, s katerimi formaliziramo koherentne univerzalne lastnosti kategornih konstrukcij. V ta namen vpeljemo pojma morfizmov tipov in prirejenih homotopij, in preučimo funktorialnosti podobne lastnosti posplošene kompozicije in produktov. Ključne dele tretjega poglavja implementiramo v računalniškem dokazovalniku Agda. dependent type theory synthetic category theory higher categories teorija odvisnih tipov sintetična teorija kategorij višje kategorije true false false Angleški jezik Slovenski jezik Magistrsko delo/naloga 2025-09-03 08:15:04 2025-09-03 08:15:08 2025-09-21 03:57:08 0000-00-00 00:00:00 2025 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 510.6 152353 247221507 18812.pdf 18812.pdf 1 67009994C1550DC52987EA4C1203F441 fadb0690bfad798451ecc69859fad23fb1d1847675b09af4c0937f668731ea95 318af148-888d-11f0-9328-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=215311 Fakulteta za matematiko in fiziko 0 0 0