naming convention about "of" and "to"

Stream: mathlib4

[Edison Xie]

There's AddEquiv.toLinearEquiv, MulEquiv.toRingEquiv but there's also AlgEquiv.ofLinearEquiv, AlgEquiv.ofRingEquiv, when do we use "of" and when do we use "to"? I thought "to" implies projection, e.g "AlgEquiv.toRingEquiv" or "LinearEquiv.toAddEquiv", do we want to unify these names or are they there for a good reason?

[Weiyi Wang]

A.toB: A has richer structure than B and this is downgrading from A to B
A.ofB: A has richer structure than B and this is upgrading from B to A with additional hypothesis
I guess this is the convention?

[Weiyi Wang]

hmm, AddEquiv.toLinearEquiv doesn't fit this

[Edison Xie]

Weiyi Wang said:

A.toB: A has richer structure than B and this is downgrading from A to B
A.ofB: A has richer structure than B and this is upgrading from B to A with additional hypothesis
I guess this is the convention?

that's exactly my point I'm saying that the examples I gave don't fit into this pattern

[Matt Diamond]

(nvm, misunderstood the question)

[Jakub Nowak]

We can have both A.ofB and B.toA.
Given b : B it's easier to read b.toA, then A.ofB b or .ofB b IMO.
But if you have some longer expression : B, then it's easier to read A.ofB <| some longer expression, then some longer expression <|.toA IMO.

[Jakub Nowak]

Maybe distinction that A.toB shouldn't have any additional explicit or autoProp arguments except for A would make sense? In which case we should only use B.ofA only if it does.

[Yaël Dillies]

I personally think the to names Edison is pointing out are in the wrong: .to should only be used for forgetful inheritance

[Kevin Buzzard]

If people have some kind of coherent vision as to what the rules are (or should be) then perhaps we should document it? I have always been confused about the difference between to and of, and my current algorithm is just to guess.

[Wrenna Robson]

I agree with @Yaël Dillies and others - to is forgetful and of constructs. Of course then you have things like toDual and ofDual - I am not sure these are the way round you would expected!

[Yaël Dillies]

Oh, synonyms are a completely different use case for to and of. I'm happy to write something... when I have time

[Edison Xie]

One other thing about this that confuses me is that we deprecated Finset.toSet and we keep Set.toFinset, surely Finset is a “better” structure than Set

[Yaël Dillies]

docs#Finset.toSet was deprecated for a completely different reason. docs#Set.toFinset is, I would argue, forgetful inheritance, in the sense that it takes no proof arguments