Why are dependent products with Prop not used?

Stream: new members

[Nir Paz]

Why is this dependent product not allowed?

import Mathlib

example : (n : ℕ) × (Even n) := sorry

I can see this is becaus in the definition of Sigma, β is a function to Type v, but why can't it be Sort instead to allow this?

I know ∃ n : ℕ, Even n does exactly this, I'm just curious why the other way doesn't work.

[Anne Baanen]

If you want to keep using Prop, you can use docs#PSigma instead. The drawback is that this has a more complicated universe level:

The reason this is not the default is that this type lives in the universe Sort (max 1 u v), which can cause problems for universe level unification, because the equation max 1 u v = ?u + 1 has no solution in level arithmetic. PSigma is usually only used in automation that constructs pairs of arbitrary types.

[Nir Paz]

Ah, thanks! can't believe I didn't see it

[Kyle Miller]

You can also stick in docs#PLift around the prop.

But there's also docs#Subtype for this combination, with notation {n : ℕ // Even n}

[Kyle Miller]

Nir Paz said:

I know ∃ n : ℕ, Even n does exactly this, I'm just curious why the other way doesn't work.

This turns out to be not exactly the same, because it's in Prop rather than Type. One consequence is that, while it's a dependent product, there are strong limitations on when you can do projections.

[Nir Paz]

Oh I didn't think of that, and I spent a while grappling with invalid projection errors on ∃. It seems silly that the error is marked at the theorem itself and not the line with the projection, so you can just keep going with the proof not noticing anything is wrong.