BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Coherence through normalisation-by-evaluation for cartesian closed
  bicategories - Philip Saville (University of Edinburgh)
DTSTART:20191112T141500Z
DTEND:20191112T151500Z
UID:TALK134755@talks.cam.ac.uk
CONTACT:José Siqueira
DESCRIPTION:Cartesian closed bicategories arise in categorical logic\, cat
 egorical algebra and game semantics\, and may be thought of as cartesian c
 losed\ncategories 'up to isomorphism'. In this talk I shall outline a proo
 f\nof a sharp form of coherence\, namely that in the free cartesian closed
 \nbicategory on a set there is at most one 2-cell between any parallel\npa
 ir of 1-cells. Thus\, there is at most one structural isomorphism\nbetween
  any pair of 1-cells in a cartesian closed bicategory. My focus\nwill be o
 n the proof stategy\, which recasts a technique from\ncategorical semantic
 s as a tool for proving coherence. I use a version\nof normalisation-by-ev
 aluation\, first employed to prove normalisation\nof the simply-typed lamb
 da calculus [1]\, applied to a type theory\nsatisfying suitable properties
 . In particualar\, I adapt Fiore's\ncategorical reconstruction of the tech
 nique [2] which\, as we shall\nsee\, is particularly amenable to being tra
 nslated into a bicategorical\nargument.\n\nI shall assume the usual Lambek
 -style semantics of the simply-typed\nlambda calculus\, but not any backgr
 ound in bicategory theory.\n\nJoint work with Marcelo Fiore
LOCATION:MR4\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR