SBtw and Sbtw

Stream: mathlib4

[Yury G. Kudryashov]

We have docs#SBtw and docs#Sbtw that mean different things.

[Yury G. Kudryashov]

Not only one is a class and another is a relation, but they are about different notions (affine and circular).

[Eric Wieser]

Can we merge the notions?

[Eric Wieser]

I guess one is directed and the other isn't

[Yury G. Kudryashov]

One is a typeclass, another takes a base ring as a parameter.

[Eric Wieser]

Ah I forgot about the base ring

[Yaël Dillies]

Yes we can. @Bhavik Mehta and I have been working on axiomatising betweenness. TLDR there is a niche but useful literature on the subject, and we're implementing one of the papers there.

[Yury G. Kudryashov]

Are you formalizing it as a typeclass? As a bundled operator? Something else?

[Yaël Dillies]

As a typeclass, but it's still up in the air

[Eric Wieser]

Isn't the base ring thing unavoidable?

[Yaël Dillies]

It's not yet clear to me how to handle the base ring

[Yaël Dillies]

We might have to do typeclasses on unbundled functions

[Yaël Dillies]

We might have to do typeclasses on unbundled functions

[Yury G. Kudryashov]

I don't see how it helps to unify a notation class and a predicate. I see how it can help deduplicate API.