refactor(CategoryTheory/Sites): sheafification as an abstract left ad…

…joint (#9012)

We define a typeclass `HasSheafify` which says that presheaves on a site with values in some category can be sheafified, i.e. that the inclusion functor from sheaves to presheaves has a left exact left adjoint. We redefine `presheafToSheaf` as an arbitrary choice of such a left adjoint.

Mathlib.lean

@@ -1297,6 +1297,7 @@ import Mathlib.CategoryTheory.Sites.RegularExtensive
 import Mathlib.CategoryTheory.Sites.Sheaf
 import Mathlib.CategoryTheory.Sites.SheafHom
 import Mathlib.CategoryTheory.Sites.SheafOfTypes
+import Mathlib.CategoryTheory.Sites.Sheafification
 import Mathlib.CategoryTheory.Sites.Sieves
 import Mathlib.CategoryTheory.Sites.Spaces
 import Mathlib.CategoryTheory.Sites.Subsheaf

Mathlib/CategoryTheory/Sites/Adjunction.lean

@@ -21,32 +21,26 @@ namespace CategoryTheory
 
 open GrothendieckTopology CategoryTheory Limits Opposite
 
-universe w₁ w₂ v u
+universe v u
 
 variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
 
-variable {D : Type w₁} [Category.{max v u} D]
+variable {D : Type*} [Category D]
 
-variable {E : Type w₂} [Category.{max v u} E]
+variable {E : Type*} [Category E]
 
 variable {F : D ⥤ E} {G : E ⥤ D}
 
-variable [∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (S.index P).multicospan F]
-
-variable [ConcreteCategory.{max v u} D] [PreservesLimits (forget D)]
+variable [HasWeakSheafify J D] [HasSheafCompose J F]
 
 /-- The forgetful functor from `Sheaf J D` to sheaves of types, for a concrete category `D`
 whose forgetful functor preserves the correct limits. -/
-abbrev sheafForget : Sheaf J D ⥤ SheafOfTypes J :=
+abbrev sheafForget [ConcreteCategory D] [HasSheafCompose J (forget D)] :
+    Sheaf J D ⥤ SheafOfTypes J :=
   sheafCompose J (forget D) ⋙ (sheafEquivSheafOfTypes J).functor
 set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf_forget CategoryTheory.sheafForget
 
--- We need to sheafify...
-variable [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)]
-  [∀ X : C, HasColimitsOfShape (J.Cover X)ᵒᵖ D]
-  [∀ X : C, PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [ReflectsIsomorphisms (forget D)]
-
 namespace Sheaf
 
 noncomputable section
@@ -63,21 +57,21 @@ set_option linter.uppercaseLean3 false in
 def composeEquiv (adj : G ⊣ F) (X : Sheaf J E) (Y : Sheaf J D) :
     ((composeAndSheafify J G).obj X ⟶ Y) ≃ (X ⟶ (sheafCompose J F).obj Y) :=
   let A := adj.whiskerRight Cᵒᵖ
-  { toFun := fun η => ⟨A.homEquiv _ _ (J.toSheafify _ ≫ η.val)⟩
-    invFun := fun γ => ⟨J.sheafifyLift ((A.homEquiv _ _).symm ((sheafToPresheaf _ _).map γ)) Y.2⟩
+  { toFun := fun η => ⟨A.homEquiv _ _ (toSheafify J _ ≫ η.val)⟩
+    invFun := fun γ => ⟨sheafifyLift J ((A.homEquiv _ _).symm ((sheafToPresheaf _ _).map γ)) Y.2⟩
     left_inv := by
       intro η
       ext1
       dsimp
       symm
-      apply J.sheafifyLift_unique
+      apply sheafifyLift_unique
       rw [Equiv.symm_apply_apply]
     right_inv := by
       intro γ
       ext1
       dsimp
       -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-      erw [J.toSheafify_sheafifyLift, Equiv.apply_symm_apply] }
+      erw [toSheafify_sheafifyLift, Equiv.apply_symm_apply] }
 set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf.compose_equiv CategoryTheory.Sheaf.composeEquiv
 
@@ -113,6 +107,8 @@ instance [IsRightAdjoint F] : IsRightAdjoint (sheafCompose J F) :=
 
 section ForgetToType
 
+variable [ConcreteCategory D] [HasSheafCompose J (forget D)]
+
 /-- This is the functor sending a sheaf of types `X` to the sheafification of `X ⋙ G`. -/
 abbrev composeAndSheafifyFromTypes (G : Type max v u ⥤ D) : SheafOfTypes J ⥤ Sheaf J D :=
   (sheafEquivSheafOfTypes J).inverse ⋙ composeAndSheafify _ G
@@ -132,7 +128,7 @@ theorem adjunctionToTypes_unit_app_val {G : Type max v u ⥤ D} (adj : G ⊣ for
     (Y : SheafOfTypes J) :
     ((adjunctionToTypes J adj).unit.app Y).val =
       (adj.whiskerRight _).unit.app ((sheafOfTypesToPresheaf J).obj Y) ≫
-        whiskerRight (J.toSheafify _) (forget D) := by
+        whiskerRight (toSheafify J _) (forget D) := by
   dsimp [adjunctionToTypes, Adjunction.comp]
   simp
   rfl
@@ -143,12 +139,12 @@ set_option linter.uppercaseLean3 false in
 theorem adjunctionToTypes_counit_app_val {G : Type max v u ⥤ D} (adj : G ⊣ forget D)
     (X : Sheaf J D) :
     ((adjunctionToTypes J adj).counit.app X).val =
-      J.sheafifyLift ((Functor.associator _ _ _).hom ≫ (adj.whiskerRight _).counit.app _) X.2 := by
-  apply J.sheafifyLift_unique
+      sheafifyLift J ((Functor.associator _ _ _).hom ≫ (adj.whiskerRight _).counit.app _) X.2 := by
+  apply sheafifyLift_unique
   dsimp only [adjunctionToTypes, Adjunction.comp, NatTrans.comp_app,
     instCategorySheaf_comp_val, instCategorySheaf_id_val]
   rw [adjunction_counit_app_val]
-  erw [Category.id_comp, J.sheafifyMap_sheafifyLift, J.toSheafify_sheafifyLift]
+  erw [Category.id_comp, sheafifyMap_sheafifyLift, toSheafify_sheafifyLift]
   ext
   dsimp [sheafEquivSheafOfTypes, Equivalence.symm, Equivalence.toAdjunction,
     NatIso.ofComponents, Adjunction.whiskerRight, Adjunction.mkOfUnitCounit]

Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
 import Mathlib.CategoryTheory.Sites.CompatiblePlus
-import Mathlib.CategoryTheory.Sites.ConcreteSheafification
+import Mathlib.CategoryTheory.Sites.LeftExact
 
 #align_import category_theory.sites.compatible_sheafification from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
 

Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Adam Topaz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
-import Mathlib.CategoryTheory.Adjunction.FullyFaithful
 import Mathlib.CategoryTheory.Sites.Plus
+import Mathlib.CategoryTheory.Sites.Sheafification
 import Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
 import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
 
@@ -525,7 +525,8 @@ noncomputable def toSheafification : 𝟭 _ ⟶ sheafification J D :=
 #align category_theory.grothendieck_topology.to_sheafification CategoryTheory.GrothendieckTopology.toSheafification
 
 @[simp]
-theorem toSheafification_app (P : Cᵒᵖ ⥤ D) : (J.toSheafification D).app P = J.toSheafify P :=
+theorem toSheafification_app (P : Cᵒᵖ ⥤ D) :
+    (J.toSheafification D).app P = J.toSheafify P :=
   rfl
 #align category_theory.grothendieck_topology.to_sheafification_app CategoryTheory.GrothendieckTopology.toSheafification_app
 
@@ -550,8 +551,7 @@ theorem isoSheafify_hom {P : Cᵒᵖ ⥤ D} (hP : Presheaf.IsSheaf J P) :
   rfl
 #align category_theory.grothendieck_topology.iso_sheafify_hom CategoryTheory.GrothendieckTopology.isoSheafify_hom
 
-/-- Given a sheaf `Q` and a morphism `P ⟶ Q`, construct a morphism from
-`J.sheafify P` to `Q`. -/
+/-- Given a sheaf `Q` and a morphism `P ⟶ Q`, construct a morphism from `J.sheafify P` to `Q`. -/
 noncomputable def sheafifyLift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) :
     J.sheafify P ⟶ Q :=
   J.plusLift (J.plusLift η hQ) hQ
@@ -613,26 +613,26 @@ variable (D)
 
 /-- The sheafification functor, as a functor taking values in `Sheaf`. -/
 @[simps]
-noncomputable def presheafToSheaf : (Cᵒᵖ ⥤ D) ⥤ Sheaf J D where
+noncomputable def plusPlusSheaf : (Cᵒᵖ ⥤ D) ⥤ Sheaf J D where
   obj P := ⟨J.sheafify P, J.sheafify_isSheaf P⟩
   map η := ⟨J.sheafifyMap η⟩
   map_id _ := Sheaf.Hom.ext _ _ <| J.sheafifyMap_id _
   map_comp _ _ := Sheaf.Hom.ext _ _ <| J.sheafifyMap_comp _ _
 set_option linter.uppercaseLean3 false in
-#align category_theory.presheaf_to_Sheaf CategoryTheory.presheafToSheaf
+#align category_theory.presheaf_to_Sheaf CategoryTheory.plusPlusSheaf
 
-instance presheafToSheaf_preservesZeroMorphisms [Preadditive D] :
-    (presheafToSheaf J D).PreservesZeroMorphisms where
+instance plusPlusSheaf_preservesZeroMorphisms [Preadditive D] :
+    (plusPlusSheaf J D).PreservesZeroMorphisms where
   map_zero F G := by
     ext : 3
     refine' colimit.hom_ext (fun j => _)
     erw [colimit.ι_map, comp_zero, J.plusMap_zero, J.diagramNatTrans_zero, zero_comp]
 set_option linter.uppercaseLean3 false in
-#align category_theory.presheaf_to_Sheaf_preserves_zero_morphisms CategoryTheory.presheafToSheaf_preservesZeroMorphisms
+#align category_theory.presheaf_to_Sheaf_preserves_zero_morphisms CategoryTheory.plusPlusSheaf_preservesZeroMorphisms
 
 /-- The sheafification functor is left adjoint to the forgetful functor. -/
 @[simps! unit_app counit_app_val]
-noncomputable def sheafificationAdjunction : presheafToSheaf J D ⊣ sheafToPresheaf J D :=
+noncomputable def plusPlusAdjunction : plusPlusSheaf J D ⊣ sheafToPresheaf J D :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun P Q =>
         { toFun := fun e => J.toSheafify P ≫ e.val
@@ -645,10 +645,10 @@ noncomputable def sheafificationAdjunction : presheafToSheaf J D ⊣ sheafToPres
       homEquiv_naturality_right := fun η γ => by
         dsimp
         rw [Category.assoc] }
-#align category_theory.sheafification_adjunction CategoryTheory.sheafificationAdjunction
+#align category_theory.sheafification_adjunction CategoryTheory.plusPlusAdjunction
 
 noncomputable instance sheafToPresheafIsRightAdjoint : IsRightAdjoint (sheafToPresheaf J D) :=
-  ⟨_, sheafificationAdjunction J D⟩
+  ⟨_, plusPlusAdjunction J D⟩
 set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf_to_presheaf_is_right_adjoint CategoryTheory.sheafToPresheafIsRightAdjoint
 
@@ -666,31 +666,7 @@ set_option linter.uppercaseLean3 false in
 @[simps! hom_app inv_app]
 noncomputable
 def GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf :
-    J.sheafification D ≅ presheafToSheaf J D ⋙ sheafToPresheaf J D :=
+    J.sheafification D ≅ plusPlusSheaf J D ⋙ sheafToPresheaf J D :=
   NatIso.ofComponents fun P => Iso.refl _
 
-variable {J D}
-
-/-- A sheaf `P` is isomorphic to its own sheafification. -/
-@[simps]
-noncomputable def sheafificationIso (P : Sheaf J D) : P ≅ (presheafToSheaf J D).obj P.val where
-  hom := ⟨(J.isoSheafify P.2).hom⟩
-  inv := ⟨(J.isoSheafify P.2).inv⟩
-  hom_inv_id := by
-    ext1
-    apply (J.isoSheafify P.2).hom_inv_id
-  inv_hom_id := by
-    ext1
-    apply (J.isoSheafify P.2).inv_hom_id
-#align category_theory.sheafification_iso CategoryTheory.sheafificationIso
-
-instance isIso_sheafificationAdjunction_counit (P : Sheaf J D) :
-    IsIso ((sheafificationAdjunction J D).counit.app P) :=
-  isIso_of_fully_faithful (sheafToPresheaf J D) _
-#align category_theory.is_iso_sheafification_adjunction_counit CategoryTheory.isIso_sheafificationAdjunction_counit
-
-instance sheafification_reflective : IsIso (sheafificationAdjunction J D).counit :=
-  NatIso.isIso_of_isIso_app _
-#align category_theory.sheafification_reflective CategoryTheory.sheafification_reflective
-
 end CategoryTheory

Mathlib/CategoryTheory/Sites/ConstantSheaf.lean

@@ -37,10 +37,7 @@ noncomputable def constantPresheafAdj {T : C} (hT : IsTerminal T) :
           simp }
       naturality := by intros; ext; simp /- Note: `aesop` works but is kind of slow -/ } }
 
-variable [ConcreteCategory D] [PreservesLimits (forget D)]
-  [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)]
-  [∀ X : C, HasColimitsOfShape (J.Cover X)ᵒᵖ D]
-  [∀ X : C, PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [ReflectsIsomorphisms (forget D)]
+variable [HasWeakSheafify J D]
 
 /--
 The functor which maps an object of `D` to the constant sheaf at that object, i.e. the

Mathlib/CategoryTheory/Sites/CoverLifting.lean

@@ -369,13 +369,7 @@ noncomputable def Functor.sheafAdjunctionCocontinuous [G.IsCocontinuous J K]
 #align category_theory.sites.pullback_copullback_adjunction CategoryTheory.Functor.sheafAdjunctionCocontinuous
 
 variable
-  [ConcreteCategory.{max v u} A]
-  [PreservesLimits (forget A)]
-  [ReflectsIsomorphisms (forget A)]
-  [∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget A)]
-  [∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ A]
-  [∀ (X : D), PreservesColimitsOfShape (K.Cover X)ᵒᵖ (forget A)]
-  [∀ (X : D), HasColimitsOfShape (K.Cover X)ᵒᵖ A]
+  [HasWeakSheafify J A] [HasWeakSheafify K A]
   [G.IsCocontinuous J K] [G.IsContinuous J K]
 
 /-- The natural isomorphism exhibiting compatibility between pushforward and sheafification. -/
@@ -393,35 +387,34 @@ def Functor.pushforwardContinuousSheafificationCompatibility :
 /- Implementation: This is primarily used to prove the lemma
 `pullbackSheafificationCompatibility_hom_app_val`. -/
 lemma Functor.toSheafify_pullbackSheafificationCompatibility (F : Dᵒᵖ ⥤ A) :
-    J.toSheafify (G.op ⋙ F) ≫
+    toSheafify J (G.op ⋙ F) ≫
     ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
-    whiskerLeft _ (K.toSheafify _) := by
+    whiskerLeft _ (toSheafify K _) := by
   dsimp [pushforwardContinuousSheafificationCompatibility, Adjunction.leftAdjointUniq]
   apply Quiver.Hom.op_inj
   apply coyoneda.map_injective
   ext E : 2
   dsimp [Functor.preimage, Full.preimage, coyoneda, Adjunction.leftAdjointsCoyonedaEquiv]
   erw [Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]
   dsimp [Adjunction.comp]
-  simp only [sheafificationAdjunction_unit_app, Category.comp_id, Functor.map_id,
-    whiskerLeft_id', GrothendieckTopology.sheafifyMap_comp,
-    GrothendieckTopology.sheafifyMap_sheafifyLift, Category.id_comp,
-    Category.assoc, GrothendieckTopology.toSheafify_sheafifyLift]
+  simp only [Category.comp_id, map_id, whiskerLeft_id', map_comp, Sheaf.instCategorySheaf_comp_val,
+    sheafificationAdjunction_counit_app_val, sheafifyMap_sheafifyLift,
+    Category.id_comp, Category.assoc, toSheafify_sheafifyLift]
   ext t s : 3
   dsimp [sheafPushforwardContinuous]
   congr 1
   simp only [← Category.assoc]
   convert Category.id_comp (obj := A) _
   have := (Ran.adjunction A G.op).left_triangle
-  apply_fun (fun e => (e.app (K.sheafify F)).app s) at this
+  apply_fun (fun e => (e.app (sheafify K F)).app s) at this
   exact this
 
 @[simp]
 lemma Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val (F : Dᵒᵖ ⥤ A) :
     ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
-    J.sheafifyLift (whiskerLeft G.op <| K.toSheafify F)
+    sheafifyLift J (whiskerLeft G.op <| toSheafify K F)
       ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F).cond := by
-  apply J.sheafifyLift_unique
+  apply sheafifyLift_unique
   apply toSheafify_pullbackSheafificationCompatibility
 
 end CategoryTheory

Mathlib/CategoryTheory/Sites/DenseSubsite.lean

@@ -545,14 +545,7 @@ noncomputable def sheafEquivOfCoverPreservingCoverLifting : Sheaf J A ≌ Sheaf
 set_option linter.uppercaseLean3 false in
 #align category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting CategoryTheory.Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting
 
-variable
-  [ConcreteCategory.{max v u} A]
-  [Limits.PreservesLimits (forget A)]
-  [ReflectsIsomorphisms (forget A)]
-  [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget A)]
-  [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ A]
-  [∀ (X : D), Limits.PreservesColimitsOfShape (K.Cover X)ᵒᵖ (forget A)]
-  [∀ (X : D), Limits.HasColimitsOfShape (K.Cover X)ᵒᵖ A]
+variable [HasWeakSheafify J A] [HasWeakSheafify K A]
 
 /-- The natural isomorphism exhibiting the compatibility of
 `sheafEquivOfCoverPreservingCoverLifting` with sheafification. -/

Mathlib/CategoryTheory/Sites/LeftExact.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Adam Topaz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
-import Mathlib.CategoryTheory.Sites.ConcreteSheafification
 import Mathlib.CategoryTheory.Sites.Limits
 import Mathlib.CategoryTheory.Limits.FunctorCategory
 import Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
@@ -243,7 +242,7 @@ variable (K : Type w')
 variable [SmallCategory K] [FinCategory K] [HasLimitsOfShape K D]
 
 instance preservesLimitsOfShape_presheafToSheaf :
-    PreservesLimitsOfShape K (presheafToSheaf J D) := by
+    PreservesLimitsOfShape K (plusPlusSheaf J D) := by
   let e := (FinCategory.equivAsType K).symm.trans (AsSmall.equiv.{0, 0, max v u})
   haveI : HasLimitsOfShape (AsSmall.{max v u} (FinCategory.AsType K)) D :=
     Limits.hasLimitsOfShape_of_equivalence e
@@ -261,22 +260,42 @@ instance preservesLimitsOfShape_presheafToSheaf :
     reflectsLimitsOfShapeOfReflectsIsomorphisms
   -- porting note: the mathlib proof was by `apply is_limit_of_preserves (J.sheafification D) hS`
   have : PreservesLimitsOfShape (AsSmall.{max v u} (FinCategory.AsType K))
-      (presheafToSheaf J D ⋙ sheafToPresheaf J D) :=
+      (plusPlusSheaf J D ⋙ sheafToPresheaf J D) :=
     preservesLimitsOfShapeOfNatIso (J.sheafificationIsoPresheafToSheafCompSheafToPreasheaf D)
-  exact isLimitOfPreserves (presheafToSheaf J D ⋙ sheafToPresheaf J D) hS
+  exact isLimitOfPreserves (plusPlusSheaf J D ⋙ sheafToPresheaf J D) hS
 
 instance preservesfiniteLimits_presheafToSheaf [HasFiniteLimits D] :
-    PreservesFiniteLimits (presheafToSheaf J D) := by
+    PreservesFiniteLimits (plusPlusSheaf J D) := by
   apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{max v u}
   intros
   infer_instance
 
+instance : HasWeakSheafify J D := ⟨sheafToPresheafIsRightAdjoint J D⟩
+
+variable (J D)
+
+/-- `plusPlusSheaf` is isomorphic to an arbitrary choice of left adjoint. -/
+def plusPlusSheafIsoPresheafToSheaf : plusPlusSheaf J D ≅ presheafToSheaf J D :=
+  (plusPlusAdjunction J D).leftAdjointUniq (sheafificationAdjunction J D)
+
+/-- `plusPlusFunctor` is isomorphic to `sheafification`. -/
+def plusPlusFunctorIsoSheafification : J.sheafification D ≅ sheafification J D :=
+  isoWhiskerRight (plusPlusSheafIsoPresheafToSheaf J D) (sheafToPresheaf J D)
+
+/-- `plusPlus` is isomorphic to `sheafify`. -/
+def plusPlusIsoSheafify (P : Cᵒᵖ ⥤ D) : J.sheafify P ≅ sheafify J P :=
+  (sheafToPresheaf J D).mapIso  ((plusPlusSheafIsoPresheafToSheaf J D).app P)
+
+instance [HasFiniteLimits D] : HasSheafify J D := HasSheafify.mk' J D (plusPlusAdjunction J D)
+
+variable {J D}
+
 instance [FinitaryExtensive D] [HasFiniteCoproducts D] [HasPullbacks D] :
     FinitaryExtensive (Sheaf J D) :=
-  finitaryExtensive_of_reflective (sheafificationAdjunction _ _)
+  finitaryExtensive_of_reflective (plusPlusAdjunction _ _)
 
 instance [Adhesive D] [HasPullbacks D] [HasPushouts D] : Adhesive (Sheaf J D) :=
-  adhesive_of_reflective (sheafificationAdjunction _ _)
+  adhesive_of_reflective (plusPlusAdjunction _ _)
 
 instance SheafOfTypes.finitary_extensive {C : Type u} [SmallCategory C]
     (J : GrothendieckTopology C) : FinitaryExtensive (Sheaf J (Type u)) :=