http://www.cedar-forest.org/forest/events/Bruijn03/
We study isomorphisms of types in the system of simply-typed lambda-calculus with inductive types and recursion operators. It is shown that in some cases (multiproducts, copies of types), it is possible to add new reductions in such a way that strong normalisation and confluence of the calculus are preserved, and the isomorphisms may be regarded as intensional w.r.t. a stronger equality relation.