## Stream: maths

### Topic: Type vs Set

#### Brandon Brown (May 03 2020 at 05:12):

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 (May 03 2020 at 05:15):

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

#### Mario Carneiro (May 03 2020 at 05:16):

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 (May 03 2020 at 05:17):

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

#### Brandon Brown (May 03 2020 at 05:23):

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 (May 03 2020 at 09:14):

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

Last updated: May 18 2021 at 08:14 UTC