Tarski asked whether the arithmetic identities taught in high school are
complete for showing all arithmetic equations valid for the natural numbers.
The answer to this question for the language of arithmetic expressions using a
constant for the number one and the operations of product and exponentiation is
affirmative, and the complete equational theory also characterizes isomorphism
in the typed lambda calculus, where the constant for one and the operations of
product and exponentiation respectively correspond to the unit type and the
product and arrow type constructors.
This paper studies isomorphisms in typed lambda calculi with empty and sum types
from this viewpoint. We close an open problem by establishing that the theory
of type isomorphisms in the presence of product, arrow, and sum types (with or
without the unit and/or the empty type) is not finitely axiomatizable.
Further, we observe that for type theories with arrow, empty and sum types
the correspondence between isomorphism and arithmetic equality generally
breaks down, but that it still holds in the particular case of type
isomorphism with the empty type and equality with zero.
