case a
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 Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ toSheafify J P ≫ sheafifyMap J η ≫ sheafifyLift J γ hR = η ≫ γ
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 Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ sheafifyMap J η ≫ sheafifyLift J γ hR = sheafifyLift J (η ≫ γ) hR
apply J.sheafifyLift_unique
no goals
case a
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 Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ toSheafify J P ≫ sheafifyMap J η ≫ sheafifyLift J γ hR = η ≫ γ
rw [← Category.assoc, ← J.toSheafify_naturality, Category.assoc, toSheafify_sheafifyLift]