{k : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : Group H] →
            (φ : G →* H) →
              {A : Type u_4} →
                [inst_3 : AddCommGroup A] →
                  [inst_4 : Module k A] → (ρ : Representation k G A) → Representation k H (Representation.IndV φ ρ)