Type x Prop

Stream: new members

[Calvin Lee]

Is a dependent pair from Type to Prop valid? I tried writing the following type signature

def lengthPresMap {α : Type u} {β : Type v} :
  (α -> β) -> (as : List α)
  ->-----------------------
  Σ bs : List β, as.length = bs.length

but it fails with the error

error: type mismatch
  List.length as = List.length bs
has type
  Prop
but is expected to have type
  Type ?u.16

[Kenny Lau]

use subtype

[Calvin Lee]

How do I do this? I don't see it anywhere in the lean4 codebase

[Eric Wieser]

Do you want docs#psigma?

[Eric Wieser]

Oh, this is #lean4

[Patrick Massot]

Yes, questions about Lean4 in new members are a bit confusing.

[Patrick Massot]

But it seems that the milestone release of Lean 4 actually brought us new users that use only Lean 4.

[Calvin Lee]

Patrick Massot said:

Yes, questions about Lean4 in new members are a bit confusing.

yes, sorry I'm a new user who's using lean4 :(

[Patrick Massot]

You don't have to be sorry, we're simply having a small organization issue.

[Patrick Massot]

In the mean time, you should probably post in the lean4 stream.