one line in "Algebra.Bundles.Raw" is redundant

[onestruggler]

This line in "Algebra.Bundles.Raw" is redundant:

"open import Relation.Nullary.Negation.Core using (¬_)"

There is no place using "¬" in that file.

[jamesmckinna]

Yup. Absolutely.

The refactoring in favour of Relation.Bundles.RawSetoid and its export of _≉_ didn't mop up this redundant import.

Nice spot! #2681 fixes this.

[onestruggler]

thanks!