BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Gluing models of type theory - Sean Moss (University of Cambridge)
DTSTART:20170207T141500Z
DTEND:20170207T151500Z
UID:TALK70939@talks.cam.ac.uk
CONTACT:Tamara von Glehn
DESCRIPTION:There is a 'logical relations' or 'gluing' construction for mo
 dels of intensional Martin-Löf type theory. In one form it constructs a m
 odel of type theory fibred over some base model out of a fibrewise collect
 ion of models. I will summarize the construction of the fibred type-theore
 tic structure on the total category of a fibration\, and show how dependen
 t products can still exist in the total model even if they do not quite ex
 ist in the fibrewise models. This generalizes the construction of von Gleh
 n's polynomial model.
LOCATION:MR5\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR