Abstract

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.