∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)).map (CategoryTheory.Arrow.mapCechNerve F))
      g.augmentedCechNerve.hom =
    CategoryTheory.CategoryStruct.comp f.augmentedCechNerve.hom ((CategoryTheory.SimplicialObject.const C).map F.right)