BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY: Identity\, indiscernibility\, and univalence: a h
igher structure identity principle - Mike Shulman\
, University of San Diego
DTSTART:20200501T193000Z
DTEND:20200501T203000Z
UID:TALK4207AT
URL:/talk/index/4207
DESCRIPTION:https://us04web.zoom.us/j/2517319462\n\nThe Struct
ure Identity Principle in univalent type theory sa
ys that\nfor a range of structures in ordinary mat
hematics\, identity is\nequivalent to isomorphism\
, with the consequence that isomorphic\nstructures
are formally indiscernible. A similar principle
says that\nfor categories\, identity is equivalent
to equivalence\, so that\nequivalent categories a
re also indiscernible\, as long as the\ncategories
themselves satisfy a SIP for their objects. We g
eneralize\nthese principles to a wide range of cat
egorical and higher-categorical\nstructures\, usin
g a notion of signature for higher structures insp
ired\nby Makkai's First-Order Logic with Dependent
Sorts\; the general SIP\nfor objects requires str
uctures to satisfy a relativized form of the\niden
tity of indiscernibles. This is joint work with B
enedikt Ahrens\,\nPaige North\, and Dimitris Tseme
ntzis.
LOCATION:Zoom
CONTACT:Paul Levy
END:VEVENT
END:VCALENDAR