Coq (и другие теории типов, такие как Setoid Type Theory) имеют вселенную Prop для предложений. Насколько я понимаю, эта вселенная нужна для уверенности в том, что предложения можно стереть. В количественной теории типов можно явно указать, какие параметры используются только в типах и могут быть удалены. Таким образом, делает ли количественная теория типов ненужной отдельная вселенная Prop?