Dependent type-theory is becoming the standard way to formalize mathematics, at the same time as displacing traditional platforms for high-insurance programming.

However, current implementations of type-theory are not always satisfactory in the sense that some "obvious truth" are impossible to prove, making type-theory awkward to use for many applications, both in formalization and programming.

We propose an extension of type-theory with colored terms, a notion of color erasure, and an interpretation of colored types as predicates. That leads to a more powerful type-theory: Some proofs and definitions can now be trivially derived hence can be omitted; Beside, some parametricity results can be internalized. (Joint work with Jean-Philippe Bernardy.)