## Stream: new members

### Topic: How do I make a one out of a set

#### Lars Ericson (Dec 13 2020 at 05:20):

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 (Dec 13 2020 at 05:56):

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 (Dec 13 2020 at 14:40):

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 }


Last updated: May 08 2021 at 19:11 UTC