search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.42k stars 314 forks source link

Missing `FunLike` instances for Quivers #5017

Open joneugster opened 1 year ago

joneugster commented 1 year ago

In several category theory files, it is necessary to add instances of the form

instance instFunLike (X Y : BddOrdCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
  show FunLike (BoundedOrderHom X Y) X (fun _ => Y) from inferInstance

where the category BddOrdCat and the type of Hom varies. Is it really intended that these have to be added manually for each category defined?

kim-em commented 1 year ago

Unless you can think of a way to avoid doing it! I think this issue needs to be generalized to describe the fact that lean4 is more hesitant to "look through" the types of morphisms in categories (or even more general).

kim-em commented 1 year ago

This link searches for references to this issue in the source code.

eric-wieser commented 1 year ago

I had a go at making Quiver.Hom reducible(https://github.com/leanprover-community/mathlib4/compare/eric-wieser/quiver-reducible), but it seem not to work very well