# What can we have in exchange if we drop subtyping from definition of Calculus of Inductive Constructions?

If we remove subtyping (https://coq.inria.fr/distrib/current/refman/language/cic.html#subtyping-rules) from CIC we will lose some expressive power. But is that power necessary for a programming language?

If we demand programmer to write e.g. Type(1) and Type(2) to mean respectively type and kind, that won't be anything novel in software engineering.

Can we get something in exchange? For example relaxed requirement on strict positivity of inductive types (without creating inconsistency in the language)?

We should get at least simpler term equivalence check where problem of η-reduction (https://coq.inria.fr/distrib/current/refman/language/cic.html#expansion) doesn't exist.

Is there some research on this topic? How does it compare to e.g. inductive types from NuPrl (https://ecommons.cornell.edu/handle/1813/6710)?