University of Cambridge > Talks.cam > Category Theory Seminar > A functional interpretation 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

A functional interpretation of type theory

Download to your calendar using vCal

If you have a question about this talk, please contact Julia Goedecke .

Dependent types are interpreted in a category as certain maps, called fibrations, where substitution corresponds to pullback, quantifiers correspond to adjoints to pullback, and identity types arise from a weak factorisation system. In this talk I will look at how, given such a category C with fibrations modelling dependent type theory, we can get another model in the category of polynomials in C. These can be thought of as types with quantifiers freely added, with maps analogous to implication in Gödel’s Dialectica interpretation of arithmetic.

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

Department of Biochemistry, Sanger Building, Perham Seminar Room Criminology Cancer Research UK Institute, Li Ka Shing Centre, Robinson Way, CB2 0RE, Cambridge

Other talks

The Magic of Magnetism Title to be confirmed Title TBC Fun experiments you can only do with frogs TBC Carrollian momenta from anti de Sitter
 

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