ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₄<VAR>D₂ : Type u₅<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₄, u₄} D₁<VAR>CategoryTheory.Category.{v₅, u₅} D₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₂.IsLocalization W₂<VAR>G : CategoryTheory.Functor D₁ D₂<VAR>h : Φ.IsLocalizedEquivalence<VAR>CategoryTheory.CatCommSq Φ.functor L₁ L₂ G<GOAL>G.IsEquivalence
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₂ : Type u₅<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₅, u₅} D₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₂.IsLocalization W₂<VAR>(Φ.functor.comp L₂).IsLocalization W₁<GOAL>Φ.IsLocalizedEquivalence
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>Φ.functor.IsEquivalence<VAR>h : W₂ ≤ W₁.map Φ.functor<GOAL>Φ.IsLocalizedEquivalence
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<GOAL>Φ.arrow.functor = Φ.functor.mapArrow
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>J : Type<VAR>CategoryTheory.Limits.HasProductsOfShape J C<VAR>hW : W.IsStableUnderProductsOfShape J<GOAL>(W.functorCategory (CategoryTheory.Discrete J)).IsInvertedBy (CategoryTheory.Limits.lim.comp L)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.ContainsIdentities<VAR>J : Type<VAR>Finite J<VAR>CategoryTheory.Limits.HasProductsOfShape J C<VAR>hW : W.IsStableUnderProductsOfShape J<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete J) C<GOAL>(CategoryTheory.Localization.HasProductsOfShapeAux.adj L hW).counit.app (F.comp L) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const (CategoryTheory.Discrete J)).map ((CategoryTheory.Localization.HasProductsOfShapeAux.compLimitFunctorIso L hW).hom.app F)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.compConstIso (CategoryTheory.Discrete J) L).hom.app (CategoryTheory.Limits.lim.obj F)) (CategoryTheory.whiskerRight (CategoryTheory.Limits.constLimAdj.counit.app F) L))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.ContainsIdentities<VAR>J : Type<VAR>Finite J<VAR>CategoryTheory.Limits.HasProductsOfShape J C<VAR>hW : W.IsStableUnderProductsOfShape J<GOAL>CategoryTheory.Limits.HasProductsOfShape J D
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.ContainsIdentities<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>W.IsStableUnderFiniteProducts<GOAL>CategoryTheory.Limits.HasFiniteProducts D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>x : CategoryTheory.Meq P S<VAR>Y : C<VAR>f g : Y ⟶ X<VAR>h : f = g<VAR>hf : S.sieve.arrows f<GOAL>↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := g, hf := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>x y : CategoryTheory.Meq P S<VAR>h : ∀ (I : S.Arrow), ↑x I = ↑y I<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>x : CategoryTheory.Meq P S<VAR>I : S.Relation<GOAL>(P.map I.r.g₁.op) (↑x ((S.index P).fstTo I)) = (P.map I.r.g₂.op) (↑x ((S.index P).sndTo I))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S T : J.Cover X<VAR>x : CategoryTheory.Meq P T<VAR>e : S ⟶ T<VAR>I : S.Arrow<GOAL>↑(x.refine e) I = ↑x { Y := I.Y, f := I.f, hf := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>Y X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>x : CategoryTheory.Meq P S<VAR>f : Y ⟶ X<VAR>I : ((J.pullback f).obj S).Arrow<GOAL>↑(x.pullback f) I = ↑x { Y := I.Y, f := CategoryTheory.CategoryStruct.comp I.f f, hf := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>Y X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S T : J.Cover X<VAR>h : S ⟶ T<VAR>f : Y ⟶ X<VAR>x : CategoryTheory.Meq P T<GOAL>(x.pullback f).refine ((J.pullback f).map h) = (x.refine h).pullback f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>x : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))<VAR>I : S.Arrow<GOAL>↑(CategoryTheory.Meq.mk S x) I = (P.map I.f.op) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>x : (CategoryTheory.forget D).obj (CategoryTheory.Limits.multiequalizer (S.index P))<VAR>I : S.Arrow<GOAL>↑((CategoryTheory.Meq.equiv P S) x) I = (CategoryTheory.Limits.Multiequalizer.ι (S.index P) I) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>x : CategoryTheory.Meq P S<VAR>I : S.Arrow<GOAL>(CategoryTheory.Limits.Multiequalizer.ι (S.index P) I) ((CategoryTheory.Meq.equiv P S).symm x) = ↑x I
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>Y X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>x : CategoryTheory.Meq P S<VAR>f : Y ⟶ X<GOAL>((J.plusObj P).map f.op) (CategoryTheory.GrothendieckTopology.Plus.mk x) = CategoryTheory.GrothendieckTopology.Plus.mk (x.pullback f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>x : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))<GOAL>((J.toPlus P).app (Opposite.op X)) x = CategoryTheory.GrothendieckTopology.Plus.mk (CategoryTheory.Meq.mk S x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>x : CategoryTheory.Meq P S<VAR>I : S.Arrow<GOAL>((J.toPlus P).app (Opposite.op I.Y)) (↑x I) = ((J.plusObj P).map I.f.op) (CategoryTheory.GrothendieckTopology.Plus.mk x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>x : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))<GOAL>((J.toPlus P).app (Opposite.op X)) x = CategoryTheory.GrothendieckTopology.Plus.mk (CategoryTheory.Meq.mk ⊤ x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>x : (CategoryTheory.forget D).obj ((J.plusObj P).obj (Opposite.op X))<GOAL>∃ S y, x = CategoryTheory.GrothendieckTopology.Plus.mk y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S T : J.Cover X<VAR>x : CategoryTheory.Meq P S<VAR>y : CategoryTheory.Meq P T<GOAL>CategoryTheory.GrothendieckTopology.Plus.mk x = CategoryTheory.GrothendieckTopology.Plus.mk y ↔ ∃ W h1 h2, x.refine h1 = y.refine h2
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>S : J.Cover X<VAR>x y : (CategoryTheory.forget D).obj ((J.plusObj P).obj (Opposite.op X))<VAR>h : ∀ (I : S.Arrow), ((J.plusObj P).map I.f.op) x = ((J.plusObj P).map I.f.op) y<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<GOAL>Function.Injective ⇑((J.toPlus P).app (Opposite.op X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<VAR>s : CategoryTheory.Meq (J.plusObj P) S<GOAL>∃ t, CategoryTheory.Meq.mk S t = s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (CategoryTheory.forget D).obj (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<GOAL>CategoryTheory.Presheaf.IsSheaf J (J.plusObj P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>CategoryTheory.Presheaf.IsSheaf J (J.plusObj (J.plusObj P))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>J.sheafifyMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (J.sheafify P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<GOAL>J.sheafifyMap (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyMap γ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp η (J.toSheafify Q) = CategoryTheory.CategoryStruct.comp (J.toSheafify P) (J.sheafifyMap η)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(J.sheafification D).obj P = J.sheafify P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<GOAL>(J.sheafification D).map η = J.sheafifyMap η
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(J.toSheafification D).app P = J.toSheafify P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>CategoryTheory.IsIso (J.toSheafify P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>(J.isoSheafify hP).hom = J.toSheafify P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>hQ : CategoryTheory.Presheaf.IsSheaf J Q<GOAL>CategoryTheory.CategoryStruct.comp (J.toSheafify P) (J.sheafifyLift η hQ) = η
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>hQ : CategoryTheory.Presheaf.IsSheaf J Q<VAR>γ : J.sheafify P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp (J.toSheafify P) γ = η → γ = J.sheafifyLift η hQ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>(J.isoSheafify hP).inv = J.sheafifyLift (CategoryTheory.CategoryStruct.id P) hP
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η γ : J.sheafify P ⟶ Q<VAR>hQ : CategoryTheory.Presheaf.IsSheaf J Q<VAR>h : CategoryTheory.CategoryStruct.comp (J.toSheafify P) η = CategoryTheory.CategoryStruct.comp (J.toSheafify P) γ<GOAL>η = γ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>hR : CategoryTheory.Presheaf.IsSheaf J R<GOAL>CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyLift γ hR) = J.sheafifyLift (CategoryTheory.CategoryStruct.comp η γ) hR
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>CategoryTheory.Presheaf.IsSheaf J (J.sheafify P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<GOAL>∀ {X Y : CategoryTheory.Functor Cᵒᵖ D} (η : X ⟶ Y), ((CategoryTheory.plusPlusSheaf J D).map η).val = J.sheafifyMap η