presheaf morphism not recognized as natural transformation

Stream: general

[Junyan Xu]

Presheaf morphism is not recognized as natural transformation when in quantifiers. Minimum working/failing examples:

import topology.sheaves.presheaf
open category_theory

example {C : Type} [category C] (X : Top) (F : Top.presheaf C X)
  (α : F ⟶ F) : α.app = α.app := rfl
/- works -/

example {C : Type} [category C] (X : Top) (F : Top.presheaf C X)
  : ∀ α : F ⟶ F, α.app = α.app := λα, rfl
/-
invalid field notation, 'app' is not a valid "field" because environment does not contain 'quiver.hom.app'
  α
which has type
  F ⟶ F
Additional information:
Untitled-1:9:18: context: invalid field notation, 'app' is not a valid "field" because environment does not contain 'quiver.rec.app'
  α
which has type
  quiver.rec (λ (hom : Top.presheaf C X → Top.presheaf C X → Sort ?), hom) ?m_1 F F
-/

What's the problem?

[Johan Commelin]

Yeah, this is annoying. Analogous failures happen often in category theory. A workaround would be to write out nat_trans.app α, but that is of course tedious.

[Johan Commelin]

I don't know if Lean could be taught to figure out the dot notation on its own.

[Junyan Xu]

It appears that inside quantifiers, Lean fails to load the category instance for presheaves so the arrow is only recognized as quiver hom. However, the following is a working example showing that Lean can load the category instance and interpret the arrow as nat_trans even within quantifiers:

example {C : Type} [category C] (X : Top) (F : Top.presheaf C X)
  : ∀ α : F ⟶ F, α ◫ 𝟙 (𝟭 C) = α ◫ 𝟙 (𝟭 C) := λα, rfl
/- works -/

[Scott Morrison]

I don't think you're correct about Lean failing to find the category instance. The fact that nat_trans.app α succeeds tells you the instances are correct.

[Scott Morrison]

This problem is something more subtle. When using dot notation, Lean has to unfold the type of the expression to the left of the dot, so that it can look in the various different namespaces the function to the right of the dot could live in. For some reason in this case it is not doing that.

[Scott Morrison]

Your second example using ◫ is not using dot notation, so is not really relevant to the failure, I think.

[Bhavik Mehta]

Is this a case where making presheaf an abbreviation/reducible fixes the annoyance without too much of the usual detriment of reducible?