(Homotopy) Type Theory and Awodey's Nautral Models
David Farrell – 1 June 2022
A "natural model of (homotopy) type theory" was defined, in a 2017 paper by Awodey, to be a map of presheaves equipped with extra structure which allows one to interpret Martin-Löf intensional type theory. At the base level, a natural model of type theory is a representable natural transformation, equipped with a choice of representation for each fiber. This map can then be associated with additional natural transformations capturing the dependent product, dependent sum and intensional identity type constructors of Martin-Löf type theory. In this expository talk I will give a rundown of Martin-Löf type theory, and then very motivate Awodey's definition, explaining the content of the first part of the paper. Time permitting, I will talk briefly on how to construct natural models, and their relationship with model structures.
Back