# Normalization and the Yoneda Embedding

Djordje Cubric (DPMMS, Cambridge) LFCS Theory Seminar Room 2511, JCMB, King's Buildings 4pm, Tuesday 29th October 1996

We show how to solve the word problem for simply typed \lambda\beta\eta-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is P-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of P-category theory we develop here is constructive and thus permits extraction of programs.

(Joint work with Peter Dybjer, and Philip Scott)