{R : Type u} →
  [inst : Ring R] →
    {M N : ModuleCat R} →
      {S : Type u_1} →
        [inst_1 : Semiring S] → [inst_2 : Module S ↑N] → [inst_3 : SMulCommClass R S ↑N] → (M ⟶ N) ≃ₗ[S] ↑M →ₗ[R] ↑N