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.
|
