COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Higher Categorical Structures, Type-Theoretically

## Higher Categorical Structures, Type-TheoreticallyAdd to your list(s) Download to your calendar using vCal - Nicolai Kraus, University of Nottingham
- Friday 12 May 2017, 14:00-15:00
- FW26.
If you have a question about this talk, please contact Dominic Mulligan. Category theory internally in homotopy type theory is intricate as categorical laws can only be stated ‘up to homotopy’, requiring coherence (similar to how the associator in a bicategory requires the pentagon). To avoid this, one can consider definitions with truncated types such as the univalent categories by Ahrens-Kapulkin-Shulman, which however fail to capture some important examples. A more general structure are (n,1)-categories, ideally with n = infinity, and a possible definition is given by Capriotti’s complete semi-Segal types. I will show how simplified (complete) semi-Segal types are indeed equivalent to univalent categories. Very much related is the question what an appropriate notion of a type-valued diagram is (joint work with Sattler). Using the type universe as a semi-Segal type, I will present several constructions of homotopy coherent diagrams (some of them infinite) and show, as an application, how one can construct all the degeneracies that a priori are missing in a complete semi-Segal type. With a further construction, we get a (finite) definition of simplicial types (up to a finite level). This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory talks
- Computing and Mathematics
- FW26
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
Note that ex-directory lists are not shown. |
## Other listsCambridge University Linguistic Society The Blackett Society History and Philosophy of Science long list## Other talksColorectal cancer. Part 1. Presentation, Diagnosis and Intervention. Part 2. Cellular signalling networks in colon cancer and the models to study them - a basic research perspective The role of myosin VI in connexin 43 gap junction accretion Identification of Active Species and Mechanistic Pathways in the Enantioselective Catalysis with 3d Transition Metal Pincer Complexes Light Echoes in Art and Science: How far do the Two Constituencies Reflect Each Other in Theory and Practice? Re/Fram/ing Geography: Fridtjof Nansen at the Royal Geographical Society c.1888-1914 Hydrodynamic instabilties and modern artistic painting |