# Does Quantitative Type Theory make the Prop universe obsolete?

Coq (and other type theories such as Setoid Type Theory) have a Prop universe for propositions. As far as I understand this universe is needed to be sure that the propositions can be erased. In Quantitative Type Theory one can explicitly say which parameters are only used in types and can be erased. Does Quantitative Type Theory therefore make a separate Prop universe unnecessary?

• That's not the only use of Prop, and no, Prop is not obsolete. Jun 19 '20 at 13:02