MFG Seminar 19th JunePublished: Friday, 16 June 2017
There will be an MFG seminar on Monday 19th June.It will take place as usual from 2.00 in 2.33.This seminar will be given by Pouya Adrom, and his abstract is given below.
There will be an MFG seminar on Monday 19th June. It will take place as usual from 2.00 in 2.33. This seminar will be given by Pouya Adrom, and his abstract is given below.
I will begin with an overview of simple and dependent type theory, mentioning common type constructors and their rules - introduction, elimination, etc. Then identity types will be introduced, with focus on intensional type theory, that is where these have non-trivial higher-dimensional structure. We will see how the syntax of intensional identity types allows interpretation in terms of notions coming from homotopy theory, thus forming the subject of homotopy type theory.