no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ stalk Y ((CategoryTheory.forget TopCat).map α.base x) = stalk Y ((CategoryTheory.forget TopCat).map β.base x)
rw [h]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ stalkMap α x =
    eqToHom
        (_ :
          stalk Y ((CategoryTheory.forget TopCat).map α.base x) =
            stalk Y ((CategoryTheory.forget TopCat).map β.base x)) ≫
      stalkMap β x
rw [← stalkMap.congr α β h x x rfl, eqToHom_refl, Category.comp_id]