1
$\begingroup$

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?

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

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.