Confused about name collisions and notations

Stream: new members

[Klaus Gy]

I have this

import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

universe u v u₀ v₀

namespace CategoryTheory

open Category Limits Functor

local notation "Δ" => diag

variable {C : Type u} {B : C} [Category.{v} C] [HasFiniteLimits C]

#check Δ B
#check diag B

and it's weird, when I hover over diag in the notation, it resolves to CategoryTheory.Limits.diag but #check Δ B reports a problem because it tries to resolve to @Functor.diag. However #check diag B works fine and resolves to CategoryTheory.Limits.diag again.

[Kevin Buzzard]

Indeed that it surprising (at least to me)