![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > A Type Theory for Strictly Associative Infinity Categories
A Type Theory for Strictly Associative Infinity CategoriesAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Tom de Jong. Many definitions of weak and strict ∞-categories have been proposed. In this paper we present a definition for ∞-categories with strict associators, but which is otherwise fully weak. Our approach is based on the existing type theory Catt, whose models are known to correspond to weak ∞-categories. We add a definitional equality relation to this theory which identifies terms with the same associativity structure, yielding a new type theory Cattsa, for strictly associative ∞-categories. We also provide a reduction relation which generates definitional equality, and show it is confluent and terminating, giving an algorithm for deciding equality of terms, and making typechecking decidable. Our key contribution, on which our reduction is based, is an operation on terms which we call insertion. This has a direct geometrical interpretation, allowing a subterm to be inserted into the head of the term, flatting its syntactic structure. We describe this operation combinatorially in terms of pasting diagrams, and also show can be characterized as a pushout of contexts. This allows reasoning about insertion using just its universal property. This is joint work with Eric Finster and Jamie Vicary. === ZOOM DETAILS === Topic: Theory Seminar – Alex Rice Time: Oct 22, 2021 01:45 PM London Join Zoom Meeting https://bham-ac-uk.zoom.us/j/81602904949?pwd=K3lERVlmVVpRc0RLVi90MWNvRFp1UT09 Meeting ID: 816 0290 4949 Passcode: 742214 One tap mobile +442034815237,,81602904949#,,,,742214# United Kingdom +442034815240,,81602904949#,,,,742214# United Kingdom Dial by your location +44 203 481 5237 United Kingdom +44 203 481 5240 United Kingdom +44 203 901 7895 United Kingdom +44 208 080 6591 United Kingdom +44 208 080 6592 United Kingdom +44 330 088 5830 United Kingdom +44 131 460 1196 United Kingdom Meeting ID: 816 0290 4949 Passcode: 742214 Find your local number: https://bham-ac-uk.zoom.us/u/kdKESm8UGf Join by SIP 81602904949@zoomcrc.com Join by H.323 162.255.37.11 (US West) 162.255.36.11 (US East) 115.114.131.7 (India Mumbai) 115.114.115.7 (India Hyderabad) 213.19.144.110 (Amsterdam Netherlands) 213.244.140.110 (Germany) 103.122.166.55 (Australia Sydney) 103.122.167.55 (Australia Melbourne) 149.137.40.110 (Singapore) 64.211.144.160 (Brazil) 149.137.68.253 (Mexico) 69.174.57.160 (Canada Toronto) 65.39.152.160 (Canada Vancouver) 207.226.132.110 (Japan Tokyo) 149.137.24.110 (Japan Osaka) Meeting ID: 816 0290 4949 Passcode: 742214 This talk is part of the Theoretical computer science seminar series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsMathematics Colloquium Algebra seminar Lab LunchOther talksThe percolating cluster is invisible to image recognition with deep learning Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Signatures of structural criticality and universality in the cellular anatomy of the brain Many-body localization from Hilbert- and real-space points of view [Friday seminar]: Irradiated brown dwarfs in the desert |