confusion with sigma types

Stream: general

[Scott Morrison]

Oops... oversimplified my example.

[Scott Morrison]

def f (n : ℕ) : Type := { l : list ℕ // l.length = n }

def foo : Σ n ≥ 5, f n := sorry
def foo' : Σ n : ℕ, Σ H : n ≥ 5, f n := sorry

[Scott Morrison]

both foo and foo'error with

type mismatch at application
  Σ (H : n ≥ 5), f n
term
  λ (H : n ≥ 5), f n
has type
  n ≥ 5 → Type : Type 1
but is expected to have type
  ?m_1 → Type : Type (max ? 1)

[Scott Morrison]

what am I doing wrong?

[Scott Morrison]

Can you just not index sigma types by Props?!

[Scott Morrison]

ugh.

[Mario Carneiro]

use Σ' or subtype

[Scott Morrison]

Thanks.

[Simon Hudon]

Does subtype do anything that Σ' doesn't do?

[Mario Carneiro]

no, except have easier universe constraints

[Simon Hudon]

Could it benefit from a unit / punit approach?

[Mario Carneiro]

Huh? It is a unit/punit approach. I mean it's even called psigma

[Simon Hudon]

Right but what happened with unit is that it became a synonym for punit.{0}