Accessing a shadowed definition

Stream: new members

[Nicolas Rolland]

can I refer to Equivalence defined in Core.lean when I am the namespace CategoryTheory which has Equivalence redefined, shadowing the other one ?

The only way I found was to close the namespace, then reopen it again...

...
end CategoryTheory.Cat

theorem EqvGenCat.is_equivalence {C : CategoryTheory.Cat} :
    Equivalence (@CategoryTheory.Cat.EqvGenCat C) := sorry

namespace CategoryTheory.Cat
...

[Kevin Buzzard]

_root_.Equivalence maybe?