How do I make a one out of a set

Stream: new members

[Lars Ericson]

I want to make a set X be it's own 1 for the type set X. This isn't working, what's the right way?

import data.finset.basic
def X := fin 3
instance X_has_one : has_one X := fin.has_one
instance PX_has_one : has_one (set X) := { one := X }

The error message is

type mismatch at field 'one'
  X
has type
  Type : Type 1
but is expected to have type
  set X : Type

and I don't know what to make of this.

[Heather Macbeth]

The set of all elements of the type X is given by set.univ.

instance PX_has_one : has_one (set X) := { one := set.univ }

[Lars Ericson]

Thank you @Heather Macbeth that works!

import data.finset.basic
def X := fin 3
instance PX_has_one : has_one (set X) :=
{ one := set.univ }