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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Gluing models of type theory

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Hybrid: in-person in Cambridge & online via Teams women@CL Coffee and Cake McCrum Lecture Theate, Corpus Christi College. Bene’t Street, Cambridge

Other talks

Title and abstract tba Title to be confirmed Christmas Social Evening & Annual General Meeting Differences between Robin and Neumann eigenvalues Title to be confirmed Washing machines and their rare components: lessons from kidney patients
 

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