∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (X : CategoryTheory.Arrow C),
  CategoryTheory.Arrow.mapCechConerve (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id X.cechConerve