enriched bifunctor PR to mathlib

Stream: Infinity-Cosmos

[Emily Riehl]

@Daniel Carranza is starting to PR his work on enriched cotensors. The first PR #35144 constructs enriched bifunctors.

This may be of interest to @Arnoud van der Leer and others.

[Arnoud van der Leer]

Ah, nice!
Did not know that he also wrote the bifunctor stuff. That came in handy for the tensors as well.

Would it be an idea to PR the tensors and cotensors together, making them consistent with eachother? I can help with that, when the time comes.

[Emily Riehl]

I'm hoping @Daniel Carranza will weigh in to indicate which approach he'd prefer. Maybe this will depend a bit on how the PR process goes...

[Daniel Carranza]

Thanks a bunch, I appreciate the interest in the PR!

I have some code on my machine which generalizes a few lemmas in the cotensor file to the braided monoidal setting (as opposed to symmetric monoidal), as well as a proof that if V is closed symmetric monoidal then V itself is a V-category with cotensors. However, because it is old, it does not compile with the current version of mathlib. As soon as the code is error-free, I can PR it to the infinity-cosmos repository in an unpolished state, so that everyone has access to the proofs. Is this okay?

What I don't want to do is slow anyone else down. While I'm polishing, I'm more than happy to make any code publicly accessible (e.g. via a PR marked as WIP) if it's any benefit, but I would feel bad if @Arnoud van der Leer has to wait for me to submit a joint PR.

[Arnoud van der Leer]

Don't worry about me. I'll find something fun to do, and if you'd like, we can, at some point, PR some (co)tensor stuff together.
If you'd like, I can also try to help polish some stuff (for some definition of polish ^^)

[Arnoud van der Leer]

I'm fairly new here, so in any joint stuff, I'll follow you, I think