19 October 2004
4:00 - 5:30  Nicola Gambino
Wellfounded trees in locally cartesian closed categories

Abstract:

The correspondence between cartesian closed categories
and simple type theories was extended in [1], where it
was shown how locally cartesian closed categories relate
to dependent type theories. The connections between type
theories and categories were recently taken further with
the introduction of a categorical counterpart of the type-theoretic
notion of W-type [2]. In the category of sets, W-types are
sets of wellfounded trees, and can be characterized abstractly
as initial algebras for endofunctors of a special kind.

In the first part of my talk, I will present some joint work with
Martin Hyland describing some of the consequences of the assumption
of the existence of wellfounded trees in a locally  cartesian closed
category. One of the main results shows that W-types allow us to
define initial algebras and free monads for wide classes of endofunctors.
In the second part of my talk, I will show how W-types can be used
to construct categorical models for intuitionistic set theories,
following the approach of Algebraic Set Theory [3].

[1] R. Seely, Locally cartesian closed categories and type theory,
  Math. Proc. Cam. Phil. Soc. 95 (33-48), 1984
[2] I. Moerdijk and E. Palmgren, Wellfounded trees in categories,
  Annals of Pure and Applied Logic, 104 (189 - 218), 2000
[3] A. Joyal and I. Moerdijk, Algebraic Set Theory, Cambridge University
  Press, 1995