Type vs Set

Stream: maths

[Brandon Brown]

This is sort of a curious meta question from a non-mathematician , but I notice that while Lean has a type Set and all of traditional mathematics is based on structures made of sets, that a lot of the basic definitions are defined on arbitrary types (α : Type u). E.g rather than a group being structure of a set with a binary operation satisfying the group axioms, it is a (α : Type u) with the binary operation, which seems like a much more general sort of thing. Is it true that such algebraic structures in Lean really are more general than one just defined on sets? or is this just syntax

[Mario Carneiro]

Lean is based on type theory, so types are the more basic construct here

[Mario Carneiro]

when you say "more general", do you mean more general in lean or more general in maths? The answer is yes to the first question and not really to the second

[Mario Carneiro]

In traditional maths a "set" is basically the same as what we would call a "type"

[Brandon Brown]

I meant more general in mathematics. But I guess that makes sense since ZFC isn't somehow less expressive than dependent type theory

[Patrick Massot]

Brandon, there is a very light discussion of this at https://leanprover-community.github.io/lean-perfectoid-spaces/type_theory.html