University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Comparing general definitions of type theories

Comparing general definitions of type theories

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

  • UserPeter LeFanu Lumsdaine, Stockholm University
  • ClockFriday 03 December 2021, 14:00-15:00
  • HouseFW26.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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