∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A B : Rep k G),
  ((CategoryTheory.ihom.coev A).app B).hom =
    ModuleCat.ofHom (TensorProduct.mk k ↑A.V ↑((CategoryTheory.Functor.id (Rep k G)).obj B).1).flip