Bundled coercion

Stream: mathlib4

[Pim Otte]

I'm trying my first port, and I nearly have something that compiles. I have a feeling I'm overlooking something small on the final bit.

This bit, doesn't work. Trying this doesn't either, and I think the reason is I'm missing some coercion-related stuff for either the functions or the objects, but I can't quite pinpoint it.

[Scott Morrison]

It's super helpful if you include the link to the PR when opening threads about ports! !4#3962

[Scott Morrison]

Unfortunately I'm out of time right now, but you might make sure you have master merged, and then try to follow the exact setup in MonCat/RingCat etc, even if it isn't exactly what mathport tells you to.

[Scott Morrison]

I just did a refactor of this in !4#3900 that might be helpful to look over.

[Scott Morrison]

It does mean we have an annoying moment of porting the remaining concrete categories where we can't exactly follow mathport. Sorry. :-( I will try to pay attention to these ports as they happen!