C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
⊢ plusMap J (plusMap J (𝟙 P)) = 𝟙 (plusObj J (plusObj J P))
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
⊢ sheafifyMap J (𝟙 P) = 𝟙 (sheafify J P)
dsimp [sheafifyMap, sheafify]
no goals
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
⊢ plusMap J (plusMap J (𝟙 P)) = 𝟙 (plusObj J (plusObj J P))
simp