{R : Type u} →
  {A : Type v} →
    {B : Type w} →
      {inst : CommSemiring R} →
        {inst_1 : Semiring A} →
          {inst_2 : Semiring B} → {inst_3 : Algebra R A} → {inst_4 : Algebra R B} → (A ≃ₐ[R] B) → ℕ