A complete decision procedure for isomorphism of kinds that contain only dependent product, constant Type and variables is obtained. All proofs are done using Z. Luo's logical framework. They can be easily transferred to a large class of type theories with dependent product.
['Sergei Soloviev']
On Isomorphism of Dependent Products in a Typed Logical Framework.