Zulip Chat Archive

Stream: new members

Topic: singleton class


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

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

view this post on Zulip Eric Wieser (Apr 11 2021 at 07:24):

docs#unique

view this post on Zulip Horatiu Cheval (Apr 11 2021 at 07:26):

Perfect, thanks!

view this post on Zulip Mario Carneiro (Apr 11 2021 at 07:31):

subsingleton is usually more useful

view this post on Zulip 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 (α × β)

view this post on Zulip Horatiu Cheval (Apr 11 2021 at 07:35):

And I have to first define

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

view this post on Zulip Horatiu Cheval (Apr 11 2021 at 07:36):

Mario Carneiro said:

subsingleton is usually more useful

Doesn't subsingleton mean at most one term?

view this post on Zulip Eric Wieser (Apr 11 2021 at 08:57):

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

view this post on Zulip Eric Wieser (Apr 11 2021 at 08:58):

I guess not

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