University of Cambridge > Talks.cam > Category Theory Seminar > Gluing models of type theory

Gluing models of type theory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Tamara von Glehn.

There is a ‘logical relations’ or ‘gluing’ construction for models of intensional Martin-Löf type theory. In one form it constructs a model of type theory fibred over some base model out of a fibrewise collection of models. I will summarize the construction of the fibred type-theoretic structure on the total category of a fibration, and show how dependent products can still exist in the total model even if they do not quite exist in the fibrewise models. This generalizes the construction of von Glehn’s polynomial model.

This talk is part of the Category Theory Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity