{A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                Module.Presentation A M₂ → (M₁ →ₗ[A] M₂) → {ι : Type w₁} → (ι → M₁) → Type (max (max u w₁) w₂₀)