singleton class

Stream: new members

[Horatiu Cheval]

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]

I'm thinking of something like

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

[Eric Wieser]

docs#unique

[Horatiu Cheval]

Perfect, thanks!

[Mario Carneiro]

subsingleton is usually more useful

[Horatiu Cheval]

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]

And I have to first define

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

[Horatiu Cheval]

Mario Carneiro said:

subsingleton is usually more useful

Doesn't subsingleton mean at most one term?

[Eric Wieser]

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

[Eric Wieser]

I guess not

[Eric Wieser]

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