MCMTT Categorical models of type theory

Faculty of Science
Spring 2022
Extent and Intensity
2/0/0. 2 credit(s) (příf plus uk k 1 zk 2 plus 1 > 4). Recommended Type of Completion: zk (examination). Other types of completion: z (credit).
Teacher(s)
Raffael Stenzel, PhD (lecturer)
doc. John Denis Bourke, PhD (assistant)
Guaranteed by
prof. RNDr. Jiří Rosický, DrSc.
Department of Mathematics and Statistics – Departments – Faculty of Science
Supplier department: Department of Mathematics and Statistics – Departments – Faculty of Science
Timetable
Wed 14:00–15:50 M5,01013
Course Enrolment Limitations
The course is offered to students of any study field.
Syllabus
  • Since its conception in the very beginning of the 20th century as an attempt to formalize a logical foundation for mathematics, type theory has undergone a considerable development to become a rich domain of contemporary research. As such, it found interdisciplinary applications in various aspects of category theory, computer science, constructive mathematics, and prominently in recent years, homotopy theory and higher category theory. The lecture is aimed to give a comprehensive introduction to the syntax of type theory and some of its semantics in category theory. We will therefore start with the untyped Lambda-calculus and its interpretation in combinatory algebras, and progressively add new type formers and dependency structure towards intensional Martin-Löf type theories and their interpretation in categorical settings with fibrational structure. The goal is to give a rigorous account of the theoretical foundations necessary to motivate and understand the role type theory plays in categorical logic and homotopy theory, with a view towards the homotopical nature of identity types and Voevodsky's notion of univalence.
Language of instruction
English
Further Comments
Study Materials
The course is taught only once.
  • Enrolment Statistics (recent)
  • Permalink: https://is.muni.cz/course/sci/spring2022/MCMTT