Comparing general definitions of type theories

Add to your list(s) Download to your calendar using vCal

• Peter LeFanu Lumsdaine, Stockholm University
• Friday 03 December 2021, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Jamie Vicary.

In the last few years, several authors have proposed quite general definitions of dependent type theories. Previously this has been a major gap in the literature; a good such definition should allow a more unified study of type theories and their models, with theorems and constructions given in a precise and broad generality, instead of (as currently) given for specific individual type theories, and adapted to others as needed, with their range of applicability understood at best heuristically.

With several proposals now available, the stage is set to develop and compare them. The main proposals so far are:

- Uemura (arXiv:1904.04097) gives an abstract categorical definition, categories with representable maps, together with several syntactic definitions, and a fruitful ∞-categorical generalisation.

- Bauer–Haselwarter–Lumsdaine (arXiv:2009.05539) give a concrete syntactic definition (based on Fiore-Plutkin-Turi or similar syntax with binding), and have formalised this definition in Coq. A similar definition was independently given by Brunerie (unpublished).

- Isaev (arXiv:1602.08504) gives an essentially-algebraic definition

I will concisely present these definitions, and survey the connections between them.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.