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

  Browse A-Z

Log in

Cambridge users (raven)details Other usersdetails No account?details

Information on

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

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.

Other lists

Type the title of a new list here Cambridgeshire Bird Club Cambridge Language Sciences Annual Symposium Cambridge Infectious Diseases Climate and Sustainable Development Finance for Industrial Sustainability in Developing Countries Spanish & Portuguese

Other talks

Private Statistics and Their Applications to Distributed Learning: Tools and Challenges Chains and Invisible Threads: Marx on Republican Liberty and Domination 'Nobody comes with an empty head': enterprise Hindutva and social media in urban India Optimising the definition of MR-based lung imaging biomarkers Viral infection dynamics in transplant recipients undergoing immunosuppression Equations in groups
 

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