over and under categories

Stream: maths

[Johan Commelin]

Over and under categories show up all over the place (notably covers and structure maps can use over categories, and algebras can use under categories). I've written the definitions and a bunch of simp lemmas in https://github.com/leanprover-community/mathlib/blob/over_under/category_theory/comma.lean#L195
Now I would like to prove some facts about limits/colimits in these categories. What would be the right file in mathlib to put these?

[Reid Barton]

I guess the current "convention" would be a new file category_theory.limits.<something>

[Johan Commelin]

Ok, I'll do that. So that would probably be category_theory.limits.over.

[Chris Hughes]

(deleted)

[Johan Commelin]

It seems I'm pushing the limits of the category library again.
I'm trying to prove an equivalence of two categories: https://github.com/leanprover-community/mathlib/blob/over_under/category_theory/comma.lean#L238
This is completely math-trivial: If I take Y in the category over X, then over Y is equivalent to over (Y.left). There is almost no content... just composing some arrows. Still I'm running into deterministic timeouts and such. Is this just stuff that should wait?

[Reid Barton]

I think you should write out the components of the natural isomorphisms anyways

[Patrick Massot]

Does it mean that Scott's magic auto-param are failing here?

[Johan Commelin]

Partly, yes. Maybe that would be fixed once back and rewrite_search are part of mathlib. But another problem is that the code is just terribly slow. At some point I close a goal by exact foobar and this takes several seconds. I guess that is just exhibiting that we are stacking lots of stuff on top of each other. (In particular the pp.all output is usually not much fun to look at.)