Remarks on isomorphisms of simple inductive types

International audienceWe study isomorphisms of types in the system of simply-typed λ-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