2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/31368We define a sound and complete proof system for affine beta-eta-retractions in simple types built over many atoms, and we state simple necessary conditions for arbitrary beta-eta-retractions in simple and polymorphic types.First International Workshop on Isomorphisms of Types Toulouse, France, 8-9 november 2002Logic in Computer ScienceF.4.1text