How to return a proof in a product.

Stream: new members

[Julian Sutherland]

I have a function that returns some finset which I want to relate to one of the functions inputs:

evalStatement :
    ∀ ... {vars : finset Identifier}, ... → Σ vars' : finset Identifier, vars ⊆ vars' × ...
...

However, prod is of type Type u → Type v → Type (max u v), and therefore I cannot pass to it an element of type Prop. Is there some standard functor in Lean for lifting a Prop to Type 0?

[Huỳnh Trần Khanh]

(deleted)

[Kevin Buzzard]

plift?

[Yakov Pechersky]

pprod will accept proofs

[Julian Sutherland]

@Kevin Buzzard @Yakov Pechersky Both work for my use case! Thanks to you both! :)

[Eric Wieser]

Is it possible that instead of sigma you want subtype there?

[Eric Wieser]

{ vars' : finset Identifier // vars ⊆ vars' ∧ ... }

[Julian Sutherland]

That might be a better way of doing it, thank you :) I'll give it a try.