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 > Category Theory Seminar > The classifying weak omega-category of a type theory

## The classifying weak omega-category of a type theoryAdd to your list(s) Download to your calendar using vCal - Chris Kapulkin, University of Warsaw
- Tuesday 24 November 2009, 14:15-15:45
- MR9, Centre for Mathematical Sciences.
If you have a question about this talk, please contact Julia Goedecke. Starting with [HS98] it has become clear that (weak) higher categories provide natural semantics for intensional Martin-Löf Type Theory. Roughly speaking, the semantics can be deﬁned by interpreting types as objects and terms as morphisms. The higher cells are given by identity types: a term ρ : Id(t,t′) is interpreted as a 2-cell [[ρ]] : [[t]] ⇒ [[t′ ]] and a term χ : Id(ρ,ρ′) as an appropriate 3-cell and so on. In my talk I would like to present the results by Lumsdaine [Lum08] and Garner and van den Berg [GvdB08], where they proved that with the interpretation as above every type carries a weak ω-category structure. Finally, I want to sketch a proposal for the construction of the classifying weak ω-category for a type theory according to [AKL09]. This is joint work with Steve Awodey and Peter LeFanu Lumsdaine (Carnegie Mellon University).
[AKL09] Steve Awodey, Chris Kapulkin, and Peter LeFanu Lumsdaine, [GvdB08] Richard Garner and Benno van den Berg, [HS98] Martin Hofmann and Thomas Streicher, [Lum08] Peter LeFanu Lumsdaine, This talk is part of the Category Theory Seminar series. ## This talk is included in these lists:- All CMS events
- All Talks (aka the CURE list)
- CMS Events
- Category Theory Seminar
- DPMMS Lists
- DPMMS Pure Maths Seminar
- DPMMS info aggregator
- DPMMS lists
- Hanchen DaDaDash
- Interested Talks
- MR9, Centre for Mathematical Sciences
- School of Physical Sciences
- bld31
- ndb35's list
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsEngineering for the Life Sciences Seminars Part III Seminar Series Lent 2008 Home## Other talksmTORC1 signaling coordinates different POMC neurons subpopulations to regulate feeding Accelerating the control of bovine Tuberculosis in developing countries A lifelong project in clay: Virtues of Unity The persistence and transience of memory CANCELLED - Methodology Masterclass: Exploring the pedagogic possibilities of new diaspora formations and transnationalism. Taking Investment in Education Seriously - Two Part Series Cambridge-Lausanne Workshop 2018 - Day 1 Towards bulk extension of near-horizon geometries Formation and disease relevance of axonal endoplasmic reticulum, a "neuron within a neuron”. BP KEYNOTE LECTURE: Importance of C-O Bond Activation for CO2/COUtilization - An Approach to Energy Conversion and Storage CANCELLED DUE TO STRIKE ACTION Recent advances in understanding climate, glacier and river dynamics in high mountain Asia |