1
$\begingroup$

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))
$\endgroup$
2
  • 1
    $\begingroup$ You can use three backticks to surround your code (or code-like text). This makes the format "verbatim", i.e. it doesn't ignore the spaces and line breaks, which makes these easier to read. I've changed it for you this time, feel free to re-edit or to rollback! $\endgroup$
    – Trebor
    Aug 10, 2023 at 14:30
  • 1
    $\begingroup$ If your curious, here is how it is defined in Lean’s math library as a (multiplicative) Semigroup. In particular it is a class so you can say automatically apply Group theorems to Semigroups. It extends Mul so that you can use the * notation. It is semi-bundled where the carrier is a parameter to the class instead of a datafield to the class. This is pretty idiomatic in mathlib. $\endgroup$
    – Jason Rute
    Aug 14, 2023 at 12:37

1 Answer 1

2
$\begingroup$

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

$\endgroup$
1
  • 1
    $\begingroup$ Ahh, I thought Type = Type 1. I forgot that computer people start counting with 0. $\endgroup$
    – Nico
    Aug 10, 2023 at 15:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.