Categorical semantics of dependent type theory - Πλίτσης, Εμμανουήλ (Εθνικό Μετσόβιο Πολυτεχνείο. Σχολή Εφαρμοσμένων Μαθηματικών και Φυσικών Επιστημών, 2018)
After a brief historical note on type theory and its semantics, we give the syntax of a basic dependent type theory in the style of Martin-Löf's Type Theory. We then discuss set-theoretic and categorical models, their uses and weaknesses. We describe the construction of a model of dependent type theory in categories with families (CwF). Finally, we examine the completeness and soundness properties of the semantics that we constructed.