∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  {X Y Z : CategoryTheory.Arrow C} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Arrow.mapAugmentedCechNerve (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.mapAugmentedCechNerve f)
      (CategoryTheory.Arrow.mapAugmentedCechNerve g)