(R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      {inst : CommSemiring R} →
        {inst_1 : Semiring A} →
          {inst_2 : TopologicalSpace A} →
            {inst_3 : Semiring B} →
              {inst_4 : TopologicalSpace B} →
                {inst_5 : Algebra R A} →
                  {inst_6 : Algebra R B} → [SizeOf R] → [SizeOf A] → [SizeOf B] → SizeOf (A ≃A[R] B)