Zulip Chat Archive

Stream: maths

Topic: Type vs Set


view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2020 at 05:15):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2020 at 05:17):

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

view this post on Zulip 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

view this post on Zulip 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