Stream: general

Topic: confusion with sigma types

Scott Morrison (Sep 22 2018 at 03:03):

Oops... oversimplified my example.

Scott Morrison (Sep 22 2018 at 03:06):

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 (Sep 22 2018 at 03:06):

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 (Sep 22 2018 at 03:06):

what am I doing wrong?

Scott Morrison (Sep 22 2018 at 03:06):

Can you just not index sigma types by Props?!

ugh.

Mario Carneiro (Sep 22 2018 at 03:09):

use Σ' or subtype

Thanks.

Simon Hudon (Sep 22 2018 at 03:51):

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

Mario Carneiro (Sep 22 2018 at 03:52):

no, except have easier universe constraints

Simon Hudon (Sep 22 2018 at 03:54):

Could it benefit from a unit / punit approach?

Mario Carneiro (Sep 22 2018 at 04:31):

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

Simon Hudon (Sep 22 2018 at 04:32):

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

Last updated: May 09 2021 at 20:11 UTC