Functional Programming Seminar

Location
C60 Computer Science Building
Date(s)
Friday 6th November 2009 (15:00-16:00)
Registration URL
http://fp.cs.nott.ac.uk/index.php?option=com_content&view=article&id=55&Itemid=66
Description
Speaker: Krzysztof Kapulkin, (University of Warsaw)
Title: The classifying weak ω-category of a type theory
Abstract:
Starting with [HS98] it has become clear that higher categories provide natural
semantics for intensional Martin-L¨of Type Theory. An ω-category has not only the
ob jects (0-cells) and morphisms (1-cells), but also morphisms between morphisms
(2-cells) and so on. All this data is organized with various kinds of composition.
However, for the purpose of interpreting Martin-Löf Type Theory we have to consider
weak ω-categories, that is those where composition is not strictly associative.
Roughly speaking, the semantics in higher categories can be defined by inter-
preting types as ob jects [[A]] and terms x : A ⊢ t : B as morphisms [[t]] : [[A]] //[[B]].
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 clas-
sifying 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.

See http://fp.cs.nott.ac.uk/index.php?option=com_content&view=article&id=55&Itemid=66
for FP seminars.

School of Computer Science

University of Nottingham
Jubilee Campus
Wollaton Road
Nottingham, NG8 1BB

For all enquires please visit:
www.nottingham.ac.uk/enquire