Is there a way to write dependent product of propositions?

Stream: new members

[YH]

Something like
def square_root (a : ℝ) (ha : 0 ≤ a) : Σ (b : ℝ), (0 ≤ b) ∧ (b ^ 2 = a)

(I tried, won't allow me, seems like it only allows Σ over Types)

[Johan Commelin]

What's the error you get?

[Johan Commelin]

Do you want something like

def square_root (a : ℝ) (ha : 0 ≤ a) : { (b : ℝ) // (0 ≤ b) ∧ (b ^ 2 = a) }

[Simon Hudon]

subtype (as pointed out by @Johan Commelin) and Σ' should do it

[Kevin Buzzard]

This { ... // ...} notation is for subtypes, which is one of the two ways Lean thinks about what mathematicians call subsets of a set. The difference between the term {x : real | x ^ 2 = 2} and the subtype {x : real // x ^ 2 = 2} is that one is a term and the other is a type, but they both express the idea of the collection of reals whose square is 2. To make a term of the subtype you need to provide a pair -- a real number, and a proof that its square is 2.