University of Cambridge > Talks.cam > Category Theory Seminar > A functional interpretation of type theory

A functional interpretation of type theory

Add to your list(s) 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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