[Merged by Bors] - feat: port CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers#2764
Conversation
mattrobball
commented
Mar 10, 2023
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
| /- Porting note: the original parameter [∀ (J) [Fintype J], PreservesColimitsOfShape | ||
| (Discrete.{0} J) G] triggered the error "invalid parametric local instance, parameter | ||
| with type Fintype J does not have forward dependencies, type class resolution cannot | ||
| use this kind of local instance because it will not be able to infer a value for this | ||
| parameter." Changed to implicit below. -/ |
There was a problem hiding this comment.
Should the outer or the inner [] be changed to {}?
The same for the other instance of this problem lower in the file.
There was a problem hiding this comment.
I tried that. I asked a question on Zulip: invalid parametric local instance
I also tried to refactor adding a new class PreservesFiniteProducts but that was too involved for the port (IMO). So I expanded the porting note. This (and the colimit version) only pop each once more for left exact functors. If that is a bear, I'll come back and fiddle with this more.
There was a problem hiding this comment.
Ok. So I went back and refactored as minimally as possible. I think this is the optimal solution.
Now we have `PreservesFiniteProducts` and `PreservesFiniteCoproducts` as separate classes
|
Pull request successfully merged into master. Build succeeded: |