15 June 2006

2:30 - 4:00   Benno van den Berg

Title: Predicative topos theory

Abstract: 
The interest of topos theory for the logician derives from its role in
providing models for impredicative logical theories like HHA
(higher-order Heyting arithmetic) and IZF (intuitionistic
ZF). Recently, Moerdijk and Palmgren have initiated the program of
developing a theory analogous to topos theory that has applications to
predicative logical theories like Martin-Lof type theory and Aczel's
set theory CZF. For this to work, the notion of topos has to be made
more predicative and a suitable notion of "predicative topos" has to
be formulated. Moerdijk and Palmgren have put forward the notion of a
PiW-pretopos. In this talk, I will give an overview of how far the
program has been carried out: what has been achieved and what remains
to be done. In particular, I would like to discuss the free
PiW-pretopos.