BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:CaTT\, a type-theory to describe weak omega-catego
ries - Thibaut Benjamin\, CEA Tech
DTSTART;TZID=Europe/London:20211022T140000
DTEND;TZID=Europe/London:20211022T150000
UID:TALK163993AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/163993
DESCRIPTION:The 2000's have taught us that although mathematic
ians consider equality as a completely basic notio
n\, and use it everyday without a second thought\,
a computational approach to (provable) equality i
s necessarily complicated. Specifically\, the iden
tity types that represent equality in Martin-Löf t
ype theory ship with a very intricate algebraic st
ructure called weak omega-groupoids. Several appro
ach have been proposed to handle this complexity\,
among which is homotopy type theory\, whose philo
sophy is to embrace it\, to establish a connection
with homotopy theory\, another domain where weak
omega-groupoids show up. Indeed\, those are very c
omplicated to study\, and the fact that they appea
r naturally in weak omega-groupoids are hard to de
scribe and study\, and homotopy type theory has pr
ovided a concrete way to get a grasp on them. In t
his talk\, I will explore the possibility of repea
ting the same story\, when we replace equality wit
h a (proof-theoretic) notion of rewriting\, which
can be seen as equality with a prvilidged directio
n. This is an open problem\, for which I will pres
ent one step: a description of the corresponding a
lgebraic structure\, weak omega-categories\, as we
ll as a type theory specifically describe those st
ructure. I will also present a proof-assistant bas
ed on this theory and demonstrate how we can use s
uch a tool to gain insight on them.
LOCATION:FW26
CONTACT:Jamie Vicary
END:VEVENT
END:VCALENDAR