BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Coherence by Normalization for Linear Multicategorical Structures 
 - Federico Olimpieri\, University of Leeds
DTSTART:20231020T130000Z
DTEND:20231020T140000Z
UID:TALK207640@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:We establish a formal correspondence between resource calculi 
 and appropriate linear multicategories. We consider the cases of (symmetri
 c) representable\, symmetric closed and autonomous multicategories.  For a
 ll these structures\, we prove that morphisms of the corresponding free co
 nstructions can be presented by means of typed resource terms\, up to a re
 duction relation and a structural equivalence.  Thanks to the linearity of
  the calculi\, we can prove strong normalization of the reduction by combi
 natorial methods\, defining appropriate decreasing measures.  From this\, 
 we achieve a general coherence result: morphisms that live in the free mul
 ticategorical structures are the same whenever the normal forms of the ass
 ociated terms are equal.  As further application\, we obtain syntactic pro
 ofs of Mac Lane's coherence theorems for (symmetric) monoidal categories.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR