∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] (φ : A →+ B) [inst_3 : CategoryTheory.HasShift C B] {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift B] {E : Type u_5}
  [inst_7 : CategoryTheory.Category.{v_3, u_5} E] [inst_8 : CategoryTheory.HasShift E B]
  (G : CategoryTheory.Functor D E) [inst_9 : G.CommShift B],
  CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.PullbackShift.natIsoComp φ F G).hom A