{R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N : Type u_7} →
        {inst : CommSemiring R} →
          {inst_1 : AddCommMonoid M₁} →
            {inst_2 : AddCommMonoid M₂} →
              {inst_3 : AddCommMonoid N} →
                {inst_4 : Module R M₁} →
                  {inst_5 : Module R M₂} →
                    {inst_6 : Module R N} →
                      (Q₁ : QuadraticMap R M₁ N) →
                        (Q₂ : QuadraticMap R M₂ N) →
                          [SizeOf R] → [SizeOf M₁] → [SizeOf M₂] → [SizeOf N] → SizeOf (Q₁ →qᵢ Q₂)