Overnamespacing

Stream: general

[Yaël Dillies]

Having typeclasses and defs in namespaces (as opposed to just lemmas), as is done in category theory, ends up giving us some stupid names, like docs#category_theory.bundled_hom.category_theory.bundled.category_theory.concrete_category

Could we make it so that instances only get the namespace once?

[Eric Rodriguez]

can you even type that without the linter having a fit?

[Yaël Dillies]

Just about! It's 86 characters long.