case hγ
C : Type u
inst✝⁸ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category D
E : Type w₂
inst✝⁶ : Category E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
hP : Presheaf.IsSheaf J (plusObj J P ⋙ F)
⊢ toPlus J (P ⋙ F) ≫ (plusCompIso J F P).inv = whiskerRight (toPlus J P) F
C : Type u
inst✝⁸ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category D
E : Type w₂
inst✝⁶ : Category E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
hP : Presheaf.IsSheaf J (plusObj J P ⋙ F)
⊢ (plusCompIso J F P).inv = plusLift J (whiskerRight (toPlus J P) F) hP
apply J.plusLift_unique
no goals
case hγ
C : Type u
inst✝⁸ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category D
E : Type w₂
inst✝⁶ : Category E
F : D ⥤ E
inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝³ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
hP : Presheaf.IsSheaf J (plusObj J P ⋙ F)
⊢ toPlus J (P ⋙ F) ≫ (plusCompIso J F P).inv = whiskerRight (toPlus J P) F
simp [Iso.comp_inv_eq]