∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : Type u) [inst_1 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (X : CategoryTheory.Sheaf J A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Functor.sheafPushforwardContinuousId A J).inv.app X).val.app X_1 =
    CategoryTheory.CategoryStruct.id (X.val.obj X_1)