The classifying weak omega-category of a type theory

Add 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 defined 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).

References

[AKL09] Steve Awodey, Chris Kapulkin, and Peter LeFanu Lumsdaine, The classifying weak ω-category of a type theory, Work in progress.

[GvdB08] Richard Garner and Benno van den Berg, Types are weak ω-groupoids, Submitted, 2008, arXiv:0812.0298.

[HS98] Martin Hofmann and Thomas Streicher, The groupoid interpretation of type theory, Twenty-Five Years of Constructive Type Theory (Venice, 1995), Oxford Logic Guides, vol. 36, Oxford Univ. Press, New York, 1998, pp. 83–111.

[Lum08] Peter LeFanu Lumsdaine, Weak ω-categories from intensional type theory (extended version), 2008, arXiv:0812.0409.

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.