HasSheafify instances

In this file, we obtain a HasSheafify (coherentTopology LightProfinite.{u}) (Type u) instance (and similarly for other concrete categories). These instances are not obtained automatically because LightProfinite.{u} is a large category, but as it is essentially small, the instances can be obtained using the results in the file Mathlib/CategoryTheory/Sites/Equivalence.lean.

instance LightProfinite.hasSheafify (A : Type u') [CategoryTheory.Category.{u, u'} A] [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.HasColimits A] {FA : A → A → Type v} {CA : A → Type u} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [(CategoryTheory.forget A).ReflectsIsomorphisms] : CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) A

instance LightProfinite.hasSheafify_type : CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) (Type u)

instance LightProfinite.instWEqualsLocallyBijectiveCoherentTopology (A : Type u') [CategoryTheory.Category.{u, u'} A] [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.HasColimits A] {FA : A → A → Type v} {CA : A → Type u} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [(CategoryTheory.forget A).ReflectsIsomorphisms] : (CategoryTheory.coherentTopology LightProfinite).WEqualsLocallyBijective A