BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:CaTT\, a type-theory to describe weak omega-categories - Thibaut B
 enjamin\, CEA Tech
DTSTART:20211022T130000Z
DTEND:20211022T140000Z
UID:TALK163993@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:The 2000's have taught us that although mathematicians conside
 r equality as a completely basic notion\, and use it everyday without a se
 cond thought\, a computational approach to (provable) equality is necessar
 ily complicated. Specifically\, the identity types that represent equality
  in Martin-Löf type theory ship with a very intricate algebraic structure
  called weak omega-groupoids. Several approach have been proposed to handl
 e this complexity\, among which is homotopy type theory\, whose philosophy
  is to embrace it\, to establish a connection with homotopy theory\, anoth
 er domain where weak omega-groupoids show up. Indeed\, those are very comp
 licated to study\, and the fact that they appear naturally in weak omega-g
 roupoids are hard to describe and study\, and homotopy type theory has pro
 vided a concrete way to get a grasp on them. In this talk\, I will explore
  the possibility of repeating the same story\, when we replace equality wi
 th a (proof-theoretic) notion of rewriting\, which can be seen as equality
  with a prvilidged direction. This is an open problem\, for which I will p
 resent one step: a description of the corresponding algebraic structure\, 
 weak omega-categories\, as well as a type theory specifically describe tho
 se structure. I will also present a proof-assistant based on this theory a
 nd demonstrate how we can use such a tool to gain insight on them.
LOCATION:FW26
END:VEVENT
END:VCALENDAR