This is probably a really simple question, but I am no able to find something in the Lean reference manual. I want to define a type of sets equipped with an associative operation. I have tried the following code.
def Magma : Type 2 := Σ M : Type, Σ mul : (Π x y : M, M), (∀ x y z : M, mul (mul x y) z = mul x (mul y z))
My idea was that a term should be a tuple $(M,(mul,p))$ consisting of a set $M$, a multiplication function $mul$ and a proof that the multiplication is associative.
Lean does not accept the definition above. What is wrong about it? I do not understand Leans explanation:
type mismatch at application Σ (mul : M → M → M), ∀ (x y z : M), mul (mul x y) z = mul x (mul y z) term λ (mul : M → M → M), ∀ (x y z : M), mul (mul x y) z = mul x (mul y z) has type (M → M → M) → Prop : Type 1 but is expected to have type (M → M → M) → Type ? : Type (max 1 (?+1))