On Wed, 23 Jan 2008, Paul B Levy wrote: > Also, are any other isomorphisms (beyond the obvious beta-eta ones) known? Having just looked at Fiore, di Cosmo and Balat's "Remarks on isomorphisms in typed lambda calculi with empty and sum types", please scratch the word "obvious" from before "beta-eta"! Paul