singleton / unique

Stream: general

[Johan Commelin]

It has been remarked before that we need a class that is nonempty + subsingleton. I guess the canonical name would be singleton. How would people want to define it?

class singleton (X : Type u) :=
(elem : X)
(uniq : \Pi (x,y : X), x = y)

[Nicholas Scheel]

why not just take nonempty and subsingleton as assumptions together?

[Johan Commelin]

I guess there are two options: either we make an inductive Prop, or we make a thing that lives in Type* but has an easy projector to the element.

[Johan Commelin]

I'm not sure what is best.

[Johan Commelin]

@Johannes Hölzl There is probably common wisdom on this in the wider community. What would you suggest?

[Johannes Hölzl]

Hm, this is a case which is not often used. But I would guess the Type* variant could be more helpful.

[Johan Commelin]

It is not? Ooh, that surprises me.

[Johannes Hölzl]

Up to now we didn't need it in mathlib...

[Johan Commelin]

Where would you put it?

[Johan Commelin]

Somewhere in data/?

[Johannes Hölzl]

Maybe even in logic/basic.lean? Plus the unit instance.

[Johan Commelin]

Is it ok to extend inhabited?

[Johan Commelin]

Or is that wrong for semantic reasons?

[Johan Commelin]

I still don't know the semantics of all those types like inhabited, default, etc...

[Johannes Hölzl]

Yes, extend inhabited and derive subsingleton

[Johan Commelin]

Ooop :see_no_evil: the name singleton is of course already taken by singleton sets...

[Johan Commelin]

@Kenny Lau Do you have a good suggestion for a name?

[Kenny Lau]

nope

[Johan Commelin]

Aahrg, punit.inhabited is only for Type, not Type u.

[Johan Commelin]

I guess the name contractible is to HoTT, right?

[Reid Barton]

Maybe unique?

[Johan Commelin]

Yes, that might work. But I'dd like to also emphasise the existence.

[Johan Commelin]

People might think that unique is a variant on subsingleton.

[Johan Commelin]

#605 @Johannes Hölzl

[Mario Carneiro]

what's wrong with just inhabited + subsingleton or nonempty + subsingleton?

[Johan Commelin]

That it's longer to write?

[Mario Carneiro]

not good enough, definitions are worth more than that

[Johan Commelin]

When I'm pulling a limit cone through and adjoint functor I want to spend as little time with these stupid classes...

[Mario Carneiro]

aha, okay sure I've seen this. Are you perhaps saying this about a subtype?

[Johan Commelin]

No...

[Johan Commelin]

Why do you think that?

[Mario Carneiro]

That's the way it usually goes with universal properties

[Mario Carneiro]

there exists a unique map satisfying such and such property

[Johan Commelin]

Ok, maybe. I haven't thought of it like that. But there are no subtypes in sight with what I'm doing right now.

[Johan Commelin]

Aah, but that's all packaged into cone_morphism

[Johan Commelin]

I want to say that c is a limit cone if \Pi t, unique (cone_morphism c t)

[Mario Carneiro]

why not say that in two conditions?

[Mario Carneiro]

you have a morphism and a proof of uniqueness

[Johan Commelin]

And then adjunctions give me equivs, and equiv.unique_of_equiv will let me easily manipulate it.

[Johan Commelin]

It's too unbundled.

[Johan Commelin]

I agree that that is also useful. And it is what we have right now in the library.

[Johan Commelin]

It's good when you are applying these things in concrete cases.

[Johan Commelin]

But for abstract category theory, I think it becomes a lot easier to manipulate these things when they are bundled.

[Mario Carneiro]

I take it you don't want to use this like a typeclass then?

[Johan Commelin]

Uuuh, I don't know?

[Mario Carneiro]

what does equiv.unique_of_equiv say?

[Johan Commelin]

If X \equiv Y and you know unique Y then you get unique X.

[Johan Commelin]

But you knew that.

[Johan Commelin]

You want code.

[Mario Carneiro]

and that's all you intend to do with unique, besides using the projections directly?

[Johan Commelin]

https://github.com/leanprover/mathlib/pull/605/files#diff-a714d761eac2ec5a2e4b0ed4592f9c46R474

[Johan Commelin]

Eehm, yes, for the time being.

[Mario Carneiro]

By the way, you can define unique in a simpler way, with only one quantifier

[Mario Carneiro]

there is x : A and \forall y, x = y

[Johan Commelin]

Yes, I've derived those versions. But I wanted to be as symmetric as possible.

[Johan Commelin]

Or is that not useful?

[Mario Carneiro]

For the structure you want the axiom to be easy to prove. Probably when one picks a default it will be easy to work with

[Mario Carneiro]

like how one shows a zero ring is unique, you show every element is 0, and hence every element is equal

[Mario Carneiro]

saves you a step

[Johan Commelin]

Ok, fine. I'll rewrite that.

[Mario Carneiro]

besides, the two quantifier version is available as subsingleton.eq

[Johan Commelin]

Ok, sure.

[Mario Carneiro]

I don't have any better suggestions for the name than unique

[Mario Carneiro]

but I think it might be usable as a regular type

[Johan Commelin]

Ok, so structure instead of class?

[Mario Carneiro]

maybe a class on some days? If you use attribute [class] unique after the definition you can use it as a class when you feel like it but the projections won't have inst implicit

[Johan Commelin]

Aah, maybe that helps.

[Johan Commelin]

I guess I should make some simp-lemmas. And then hopefully tidy can work with this nicely.

[Mario Carneiro]

Here are some interesting facts: subsingleton (unique A), and unique (unique A) <-> unique A, unique A -> unique B if f : A -> B is a surjection (not required to be a bijection)

[Johan Commelin]

Yep... would you like all of those?

[Mario Carneiro]

if you are going to define a thing you should prove all the basic theorems

[Johan Commelin]

Where should those go?

[Johan Commelin]

logic/basic?

[Mario Carneiro]

how about logic/unique unless there is a reason to merge it

[Mario Carneiro]

I don't think there are currently any new definitions in logic/basic

[Mario Carneiro]

but logic/basic probably needs a refactor, it's a bit of a grab bag

[Mario Carneiro]

it literally has a miscellaneous section, that's never a good sign

[Johan Commelin]

Ok, I can start logic/unique

[Johan Commelin]

If I do the attribute [class] thing, and I assume [unique X] then it still doesn't infer inhabited X. So I have to state those inferences by hand?

[Johan Commelin]

@Mario Carneiro Should I include simp-lemmas like this?

instance : inhabited α := to_inhabited ‹unique α›

@[simp] lemma eq_default (a : α) : a = default α := uniq _ a

[Mario Carneiro]

you have to mark unique.to_inhabited as instance

[Mario Carneiro]

eq_default won't work

[Mario Carneiro]

neither will default_eq

[Johan Commelin]

Why not?

[Johan Commelin]

It would be cool if simp would just simplify every element to the default.

[Mario Carneiro]

simp lemmas with a variable on the left trigger on anything

[Mario Carneiro]

at least that's what lean says; I don't see why that's a problem but it's explicitly rejected by simp

[Johan Commelin]

Aah, and simp doesn't know yet if the unique X instance will be found or not.

[Mario Carneiro]

well, it could just try to apply it on every term... you know I think this is a bad idea

[Johan Commelin]

you have to mark unique.to_inhabited as instance

Like so: attribute [instance] unique.to_inhabited?

[Mario Carneiro]

yes

[Johan Commelin]

But then

variables {α : Sort u} [unique α]

instance : inhabited α := by apply_instance

still fails.

[Mario Carneiro]

oh, I guess that's because the unique is explicit in unique.to_inhabited. So you will have to make an instance like you did

[Johan Commelin]

@Mario Carneiro Should the following be done with instances or not?

def of_surjective (f : α → β) (hf : surjective f) (h : inhabited α) : inhabited β :=
{ default := f h.default }

[Johannes Hölzl]

hf is not required...

[Johan Commelin]

Lol... I've been thinking too much about unique :grinning:

[Johan Commelin]

@Johannes Hölzl @Mario Carneiro I pushed an update to #605

[Johan Commelin]

Woops, forgot to git add the new file.