The problem is that data types define a module and a name. You need to rename the module, too. This works:
module Cactus where
module A₁ where
data B : Set where
module A₂ where
open A₁ renaming (B to B₁; module B to B₁)
data B : Set where
This allows you to refer to constructors in a module-ish way, so if you have a conflict between Level.suc
and your ℕ
one, you can just write ℕ.suc
and have it work without having to go through renaming shenanigans.