 A first attempt towards a Unifying Principle for extensional type theory with primitive equality is presented in Kohlhase 1993. The conditions given there, which are still  incomplete[1],  were subsequently modified and complemented as follows: