confused about doubled names

Stream: new members

[Bhavik Mehta]

import category_theory.category

namespace category_theory

universes v u

variables (A : Type u) [category.{v} A]

structure foo :=
(C₀ C₁ : A)
(f : C₀ ⟶ C₁)

structure bar extends foo.{v} A :=
(assoc : begin dedup, end)

end category_theory

[Bhavik Mehta]

if your cursor is in the empty begin end block, you'll see two copies of A, and I have no idea why