The interpretation of intuitionistic type theory in locally cartesian closed categories: an intuitionistic approach
Add to your list(s)
Download to your calendar using vCal
If you have a question about this talk, please contact Tom Ridge.
I [Peter Dybjer] will give an intuitionistic view of Seely’s interpretation of MartinLöf type in locally cartesian closed categories. The point is to use MartinLöf type theory itself as metalanguage, and a constructive notion of category, a so called Ecategory. As a categorical substitute for the formal system of MartinLöf type theory I will use Ecategories with families, and discuss how to interpret such categories in Elocally cartesian closed categories. This is joint work with Alexandre Buisse, who has formalized the key part of this proof in Coq.
This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
This talk is included in these lists:
Note that exdirectory lists are not shown.
