BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The classifying weak omega-category of a type theory - Chris Kapul
 kin\, University of Warsaw
DTSTART:20091124T141500Z
DTEND:20091124T154500Z
UID:TALK20994@talks.cam.ac.uk
CONTACT:Julia Goedecke
DESCRIPTION:Starting with [HS98] it has become clear that (weak) higher ca
 tegories provide natural semantics for intensional Martin-Löf Type Theory
 . Roughly speaking\, the semantics can be defined by interpreting types a
 s objects and terms as morphisms. The higher cells are given by identity t
 ypes: a term ρ : Id(t\,t′) is interpreted as a 2-cell [[ρ]] : [[t]] 
 ⇒ [[t′ ]] and a term χ : Id(ρ\,ρ′) as an appropriate 3-cell and s
 o on.\nIn 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 in
 terpretation as above every type carries a weak ω-category structure. Fin
 ally\, I want to sketch a proposal for the construction of the classifying
  weak ω-category for a type theory according to [AKL09].\nThis is joint w
 ork with Steve Awodey and Peter LeFanu Lumsdaine (Carnegie Mellon Universi
 ty).\n\n*References*\n\n[AKL09] Steve Awodey\, Chris Kapulkin\, and Peter 
 LeFanu Lumsdaine\, _The classifying weak ω-category of a type theory_\, W
 ork in progress.\n\n[GvdB08] Richard Garner and Benno van den Berg\, _Type
 s are weak ω-groupoids_\, Submitted\, 2008\, arXiv:0812.0298.\n\n[HS98] M
 artin 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.\n\n[Lum08] Peter LeFanu Lumsdaine\, _Weak ω-categories from in
 tensional type theory_ (extended version)\, 2008\, arXiv:0812.0409.
LOCATION:MR9\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR