Removing Prop in setoidtt-proto

[atennapel]

Hi,

In setoidtt-proto there is already Set : Set, making the language inconsistent. I wonder if, when you:

• Remove Prop
• Change ⊤ to the 1 type
• Change ⊥ to the 0 type
• Change ∧ to sigma
• Change ∀ to pi Then do we get a language that is practically the same, or does it make things much worse?

I ask because Set : Set seems to make things must simpler and for practical programming the inconsistency might not be so bad. We can still prove things, we just have to be more disciplined in that the proof cannot be an infinite loop, and we cannot erase proofs. So if one wanted a simple dependently type programming with function extensionality, then is the above idea practical or not?

[AndrasKovacs]

It doesn't work without Prop. I don't remember where's exactly the issue but progress/preservation will fail if you attempt the coe/equality rules without Prop.

Cubical TTs have funext but not strict Prop, but they are much more complex and more general. The current setoid TT is the simplest system that I know which has funext and which should have a sensible semantics.

Strict Prop is very convenient on its own, BTW. E.g. in non-cubical Agda (without funext) we can still enable Prop, and it highly useful there as well.

[atennapel]

Would quantitative type theory be able to subsume Prop? Because you can explicitly say that something is not computationally used, which is what you want for the proofs, I think.

[AndrasKovacs]

No. QTT gives the guarantee that any 0 binder is not used computationally. Prop gives the guarantee that any inhabitant of any A : Prop cannot be used to eliminate into Set (with the sole exception of the empty proposition). The two are very different. QTT ties relevance to binders, Prop to universes.

If we have "squash" type, Squash : Set -> Prop with squash : A -> Squash A, such that we can only eliminate from Squash A to Prop, we can use that to emulate 0 binders, but 0 binders cannot emulate Prop.