∀ {k G : Type u_1} [inst : CommRing k] [inst_1 : Group G] (A B C : Rep k G),
  Function.LeftInverse ((CategoryTheory.ihom.adjunction A).homEquiv B C).invFun
    ((CategoryTheory.ihom.adjunction A).homEquiv B C).toFun