transparent instances

Stream: lean4

[Julien Marquet]

I'm trying to write some category theory in Lean 4.
I essentially ported mathlib's code, and I have this notation for arrows:

class HasHom (α : Type u) : Sort (max u v + 1) where
  hom : α → α → Sort v

infixr:10 "⟶" => HasHom.hom -- \h

I defined Category and Functor, then the category of categories.
I have this notation for functors:

infixr:26 "⥤" => Functor

(By the way, I choose to have all objects bundled, rather than a carrier+typeclass setup. That is why Functor and Category are structures to me here, rather than a typeclass, and I don't have "unbundled functors". This works well in Lean 4 imho, at least in my use case.)

Now, in the category of categories, I of course defined arrows between C and D to be functors C ⥤ D.
The thing is, the notation C ⥤ D is more natural than C ⟶ D for functors, and sometimes it makes more sense to define some constructions on Functor than on - ⟶ - (it's the case to me when I define a product of functors as a functor between the products).
Is it possible to make Lean remove the typeclass application whenever it sees C ⟶ D, to instead desugar it to C ⥤ D?

I guess this behavior would be something like "transparent instances", just like marking a definition @[reducible] makes it transparent to typeclass resolution.

(I guess it would also make sense to have a similar behavior for other objets where arrows also make sense "outside of the category", possibly in linear maps between vector spaces, but I can't really find another compelling example than the functors off the top of my head.)

[Julien Marquet]

Actually now that I think of it there may be more places where such a behavior would be relevant: for instance, if I define monoidal categories, I want to have a notation for monoidal functors, and I also want to be able to write about functors between monoidal categories by forgetting the monoidal structure. I guess this situation can be generalized to any category with additional structure.
Also, if I want to write about formal semantics, I may want to have a category between terms where arrows are reductions (I'm kind of making that up though, I don't really know how it's done), then I want the reductions to be properly denoted with a wiggly arrow rather than the hom arrow. This goes beyond notation: there is additional structure in reductions (for instance, I may want to define deduction rules for my reductions) that has not much to do with the categorical structure.

[Adam Topaz]

I don't know the answer, but I think it's an important question. In mathlib, it routinely causes a lot of pain to go back and forth between, say, linear maps and morphisms in Module R.

[Adam Topaz]

We've used some tricks in some cases, e.g. docs#category_theory.Sheaf.hom is a structure wrapper around natural transformations for precisely this reason