BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Comparing general definitions of type theories - Peter LeFanu Lums
 daine\, Stockholm University
DTSTART:20211203T140000Z
DTEND:20211203T150000Z
UID:TALK165289@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:In the last few years\, several authors have proposed quite ge
 neral definitions of dependent type theories.  Previously this has been a 
 major gap in the literature\; a good such definition should allow a more u
 nified study of type theories and their models\, with theorems and constru
 ctions given in a precise and broad generality\, instead of (as currently)
  given for specific individual type theories\, and adapted to others as ne
 eded\, with their range of applicability understood at best heuristically.
 \n\nWith several proposals now available\, the stage is set to develop and
  compare them.  The main proposals so far are:\n\n- Uemura (arXiv:1904.040
 97) gives an abstract categorical definition\, *categories with representa
 ble maps*\, together with several syntactic definitions\, and a fruitful 
 ∞-categorical generalisation.\n\n- Bauer–Haselwarter–Lumsdaine (arXi
 v:2009.05539) give a concrete syntactic definition (based on Fiore-Plutkin
 -Turi or similar syntax with binding)\, and have formalised this definitio
 n in Coq.  A similar definition was independently given by Brunerie (unpub
 lished).\n\n- Isaev (arXiv:1602.08504) gives an essentially-algebraic defi
 nition\n\nI will concisely present these definitions\, and survey the conn
 ections between them.
LOCATION:FW26
END:VEVENT
END:VCALENDAR