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?

  • $\begingroup$ That's not the only use of Prop, and no, Prop is not obsolete. $\endgroup$ – Andrej Bauer Jun 19 '20 at 13:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.