(F : Type u_14) →
  (R : outParam (Type u_15)) →
    (M : outParam (Type u_16)) →
      (M₂ : outParam (Type u_17)) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] → [Module R M] → [Module R M₂] → [EquivLike F M M₂] → Prop