University of Birmingham > Talks@bham > Theoretical computer science seminar > Identity, indiscernibility, and univalence: a higher structure identity principle

## Identity, indiscernibility, and univalence: a higher structure identity principleAdd to your list(s) Download to your calendar using vCal - Mike Shulman, University of San Diego
- Friday 01 May 2020, 20:30-21:30
- Zoom.
If you have a question about this talk, please contact Paul Levy. https://us04web.zoom.us/j/2517319462 The Structure Identity Principle in univalent type theory says that for a range of structures in ordinary mathematics, identity is equivalent to isomorphism, with the consequence that isomorphic structures are formally indiscernible. A similar principle says that for categories, identity is equivalent to equivalence, so that equivalent categories are also indiscernible, as long as the categories themselves satisfy a SIP for their objects. We generalize these principles to a wide range of categorical and higher-categorical structures, using a notion of signature for higher structures inspired by Makkai’s First-Order Logic with Dependent Sorts; the general SIP for objects requires structures to satisfy a relativized form of the identity of indiscernibles. This is joint work with Benedikt Ahrens, Paige North, and Dimitris Tsementzis. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Theoretical computer science seminar
- Zoom
- computer sience
Note that ex-directory lists are not shown. |
## Other listsRSLC PhD/Postdoc Seminars (Chemistry) computer sience EPS - College Research and KT Support Activities## Other talksTheory: This is moved to next year, 2023 ! [Colloquium:] Aperture Fever: The Extremely Large Telescope (Special colloquium): Quantum enhanced superresolution confocal microscopy TBC Tight Lower Bounds for Parameterized Algorithms under ETH Hidden Markov Model in Multiple Testing on Dependent Data |