∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {D : Type u'} [inst_2 : CategoryTheory.Category.{v, u'} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [inst_4 : F.IsEquivalence],
  CategoryTheory.Limits.compNatIso F =
    CategoryTheory.NatIso.ofComponents
      (fun j =>
        match j with
        | CategoryTheory.Limits.WalkingParallelPair.zero =>
          CategoryTheory.Iso.refl
            (((CategoryTheory.Limits.parallelPair f 0).comp F).obj CategoryTheory.Limits.WalkingParallelPair.zero)
        | CategoryTheory.Limits.WalkingParallelPair.one =>
          CategoryTheory.Iso.refl
            (((CategoryTheory.Limits.parallelPair f 0).comp F).obj CategoryTheory.Limits.WalkingParallelPair.one))
      ⋯