(R : Type u₀) →
  {inst : CommSemiring R} →
    (A : Type u₁) →
      {inst_1 : Ring A} →
        {inst_2 : Algebra R A} →
          (B : Type u₂) →
            {inst_3 : Ring B} →
              {inst_4 : Algebra R B} → [SizeOf R] → [SizeOf A] → [SizeOf B] → SizeOf (MoritaEquivalence R A B)