Upstreaming

Stream: toric

[Yaël Dillies]

@Moisés Herradón Cueto, according to the upstreaming dashboard, your file Toric.Mathlib.CategoryTheory.WithTerminal is ready to be upstreamed to mathlib. Will you do it or should I?

[Moisés Herradón Cueto]

Sure, I'll do it!

[Yaël Dillies]

@Moisés Herradón Cueto, actually your other file Toric.Mathlib.CategoryTheory.WithTerminal.Cones is ready too

[Yaël Dillies]

@Justus Springer, polyhedral cones are available to upstream. I don't know whether we actually want to upstream them, or to wait for @Martin Winter's version to be upstreamed instead.

[Martin Winter]

After speaking to @Justus Springer we are currently implementing major changes for polyhedral cones, and this is not yet ready for upstreaming.

[Yaël Dillies]

Perfect! I was suspecting as much

[Yaël Dillies]

What is your opinion on removing the polyhedral cone material from Toric? In my mind, it makes sense for Toric to depend on Polyhedral, so long as I can bump Polyhedral whenever necessary

[Yaël Dillies]

I have done so :smiling_devil: