Type of Sets with an Assocaitive Operation in Lean

Question

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))

Answer 1

The error actually consists of two parts, the first of which is easier to spot. Namely, the type of Σ assumes both of its arguments live in the Type universe, but = is a Prop: "has type ... → Prop ... but is expected to have type ... → Type ?". So instead the Σ should be Σ' which allows the Prop universe too at the expense of some more complicated universe variables.

If we replace Σ with Σ' we'll see another error: "failed to solve universe constraint 2 =?= max 1 ?u.3". This is because Magma is actually in Type 1 instead of Type 2, since it quantifies only over things in Type (= Type 0).

So a fixed version would look like:

def Magma : Type 1 :=
Σ M : Type,
Σ' mul : (∀ x y : M, M),
(∀ x y z : M, mul (mul x y) z = mul x (mul y z))

I should point out that it is much more idiomatic to instead use the structure command to define these kinds of tuples. It would look something like:

structure Magma' : Type 1 :=
(M : Type)
(mul : (∀ x y : M, M))
(mul_assoc : (∀ x y z : M, mul (mul x y) z = mul x (mul y z)))

The structure command gives you access to a lot of useful constructs that Σ does not have. In particular, this means you don't have to worry about Σ versus Σ'.

(I'm using Lean 4 but everything should be backwards-compatible with Lean 3.)