Zulip Chat Archive

Stream: general

Topic: confusion with sigma types


view this post on Zulip Scott Morrison (Sep 22 2018 at 03:03):

Oops... oversimplified my example.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Scott Morrison (Sep 22 2018 at 03:06):

what am I doing wrong?

view this post on Zulip Scott Morrison (Sep 22 2018 at 03:06):

Can you just not index sigma types by Props?!

view this post on Zulip Scott Morrison (Sep 22 2018 at 03:06):

ugh.

view this post on Zulip Mario Carneiro (Sep 22 2018 at 03:09):

use Σ' or subtype

view this post on Zulip Scott Morrison (Sep 22 2018 at 03:29):

Thanks.

view this post on Zulip Simon Hudon (Sep 22 2018 at 03:51):

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

view this post on Zulip Mario Carneiro (Sep 22 2018 at 03:52):

no, except have easier universe constraints

view this post on Zulip Simon Hudon (Sep 22 2018 at 03:54):

Could it benefit from a unit / punit approach?

view this post on Zulip Mario Carneiro (Sep 22 2018 at 04:31):

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

view this post on Zulip 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