## Stream: new members

### Topic: singleton class

#### Horatiu Cheval (Apr 11 2021 at 07:23):

Sorry if it's obvious, but I can't find it. Is there in mathlib a typeclass saying that a type is a singleton (i.e. it has exactly one term)? has_singleton.singleton seems to be something else.

#### Horatiu Cheval (Apr 11 2021 at 07:23):

I'm thinking of something like

class single (α : Sort*) extends inhabited α :=
(all_eq : ∀ x y : α, x = y)


docs#unique

Perfect, thanks!

#### Mario Carneiro (Apr 11 2021 at 07:31):

subsingleton is usually more useful

#### Horatiu Cheval (Apr 11 2021 at 07:34):

Though I find kind of strange that this doesn't work out of the box

  variables {α β : Type} [unique α] [unique β]
def f (γ : Type) [unique γ] : true := sorry
#check f (α × β)

-- failed to synthesize type class instance for
-- α β : Type,
-- _inst_1 : unique α,
-- _inst_2 : unique β
-- ⊢ unique (α × β)


#### Horatiu Cheval (Apr 11 2021 at 07:35):

And I have to first define

instance : unique (α × β) := unique.mk' (α × β)


#### Horatiu Cheval (Apr 11 2021 at 07:36):

Mario Carneiro said:

subsingleton is usually more useful

Doesn't subsingleton mean at most one term?

#### Eric Wieser (Apr 11 2021 at 08:57):

Don't we have docs#prod.unique or docs#unique.prod?

I guess not

#### Eric Wieser (Apr 11 2021 at 09:05):

Note that unique implies subsingleton, so it's often best to provide an instance of the former but where possible assume only the latter

Last updated: May 08 2021 at 18:17 UTC