ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<GOAL>(CategoryTheory.MonoOver.imageMonoOver f).arrow = CategoryTheory.Limits.image.ι f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>CategoryTheory.Limits.HasImages C<VAR>f : CategoryTheory.Over X<GOAL>CategoryTheory.MonoOver.image.obj f = CategoryTheory.MonoOver.imageMonoOver f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>CategoryTheory.Limits.HasImages C<VAR>f g : CategoryTheory.Over X<VAR>k : f ⟶ g<GOAL>CategoryTheory.MonoOver.image.map k = (CategoryTheory.MonoOver.forget X).preimage (CategoryTheory.Over.homMk (CategoryTheory.Limits.image.lift (CategoryTheory.Limits.MonoFactorisation.mk (CategoryTheory.Limits.image g.hom) (CategoryTheory.Limits.image.ι g.hom) (CategoryTheory.CategoryStruct.comp k.left (CategoryTheory.Limits.factorThruImage g.hom)) ⋯)) ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryPreExtensive C<GOAL>CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.extensiveCoverage C ⊔ CategoryTheory.regularCoverage C) = CategoryTheory.coherentTopology C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preregular C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>(∃ Y π, CategoryTheory.EffectiveEpi π ∧ S.arrows π) → S ∈ (CategoryTheory.regularTopology C).sieves X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preregular C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ (CategoryTheory.regularTopology C).sieves X ↔ ∃ Y π, CategoryTheory.EffectiveEpi π ∧ S.arrows π
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>H : J.OneHypercoverFamily<VAR>self : H.IsGenerating<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>hS : S ∈ J.sieves X<GOAL>∃ E, ∃ (_ : H E), E.sieve₀ ≤ S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>H : J.OneHypercoverFamily<VAR>H.IsGenerating<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>hS : S ∈ J.sieves X<GOAL>∃ E, ∃ (_ : H E), E.sieve₀ ≤ S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>H.IsGenerating<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>hS : S ∈ J.sieves X<VAR>T : A<VAR>x y : T ⟶ P.obj (Opposite.op X)<VAR>h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → CategoryTheory.CategoryStruct.comp x (P.map f.op) = CategoryTheory.CategoryStruct.comp y (P.map f.op)<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>E : J.OneHypercover X<VAR>hE : H E<VAR>le : E.sieve₀ ≤ S<VAR>F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)<VAR>i : E.I₀<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F) (P.map (E.f i).op) = F.ι { Y := E.X i, f := E.f i, hf := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>H.IsGenerating<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>E : J.OneHypercover X<VAR>hE : H E<VAR>le : E.sieve₀ ≤ S<VAR>F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F) (P.map f.op) = F.ι { Y := Y, f := f, hf := hf }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>H.IsGenerating<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>J.IsGeneratedByOneHypercovers<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X Y : CategoryTheory.Grothendieck F<VAR>f g : X.Hom Y<VAR>w_base : f.base = g.base<VAR>w_fiber : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X : CategoryTheory.Grothendieck F<GOAL>X.id.fiber = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X : CategoryTheory.Grothendieck F<GOAL>X.id.base = CategoryTheory.CategoryStruct.id X.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X Y Z : CategoryTheory.Grothendieck F<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>(CategoryTheory.Grothendieck.comp f g).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map g.base).map f.fiber) g.fiber)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X Y Z : CategoryTheory.Grothendieck F<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>(CategoryTheory.Grothendieck.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X : CategoryTheory.Grothendieck F<GOAL>(CategoryTheory.CategoryStruct.id X).fiber = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X Y Z : CategoryTheory.Grothendieck F<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map g.base).map f.fiber) g.fiber)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X Y : CategoryTheory.Grothendieck F<VAR>f g : X ⟶ Y<VAR>h : f = g<GOAL>f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.fiber
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X : CategoryTheory.Grothendieck F<GOAL>(CategoryTheory.Grothendieck.forget F).obj X = X.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<VAR>X Y : CategoryTheory.Grothendieck F<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Grothendieck.forget F).map f = f.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F G : CategoryTheory.Functor C CategoryTheory.Cat<VAR>α : F ⟶ G<VAR>X Y : CategoryTheory.Grothendieck F<VAR>f : X ⟶ Y<GOAL>((CategoryTheory.Grothendieck.map α).map f).fiber = CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).app X.fiber) ((α.app Y.base).map f.fiber)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F G : CategoryTheory.Functor C CategoryTheory.Cat<VAR>α : F ⟶ G<VAR>X : CategoryTheory.Grothendieck F<GOAL>((CategoryTheory.Grothendieck.map α).obj X).base = X.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F G : CategoryTheory.Functor C CategoryTheory.Cat<VAR>α : F ⟶ G<VAR>X : CategoryTheory.Grothendieck F<GOAL>((CategoryTheory.Grothendieck.map α).obj X).fiber = (α.app X.base).obj X.fiber
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F G : CategoryTheory.Functor C CategoryTheory.Cat<VAR>α : F ⟶ G<VAR>X Y : CategoryTheory.Grothendieck F<VAR>f : X ⟶ Y<GOAL>((CategoryTheory.Grothendieck.map α).map f).base = f.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>F G : CategoryTheory.Functor C CategoryTheory.Cat<VAR>α : F ⟶ G<VAR>X : CategoryTheory.Grothendieck F<GOAL>(CategoryTheory.Grothendieck.map α).obj X = { base := X.base, fiber := (α.app X.base).obj X.fiber }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>F G : CategoryTheory.Functor C CategoryTheory.Cat<VAR>α : F ⟶ G<VAR>X Y : CategoryTheory.Grothendieck F<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Grothendieck.map α).map f = { base := f.base, fiber := CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).app X.fiber) ((α.app Y.base).map f.fiber) }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>F G : CategoryTheory.Functor C CategoryTheory.Cat<VAR>α : F ⟶ G<GOAL>(CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.forget G) = CategoryTheory.Grothendieck.forget F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>F : CategoryTheory.Functor C CategoryTheory.Cat<GOAL>CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (CategoryTheory.Grothendieck F))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>F G H : CategoryTheory.Functor C CategoryTheory.Cat<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.map β)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).fst = X.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).snd = X.fiber.as
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<GOAL>∀ {X Y : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X ⟶ Y), ↑((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).map f) = f.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : G.Elements<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).fiber.as = X.snd
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<GOAL>∀ {X Y : G.Elements} (f : X ⟶ Y), ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).map f).base = ↑f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : G.Elements<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).base = X.fst
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).snd = X.fiber.as
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).base = CategoryTheory.CategoryStruct.id X.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).fiber = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).fst = X.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<GOAL>∀ {X Y : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X ⟶ Y), ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.map f) = f.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).base = CategoryTheory.CategoryStruct.id X.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : G.Elements<GOAL>↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.inv.app X) = CategoryTheory.CategoryStruct.id X.fst
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : G.Elements<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).fiber.as = X.snd
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<GOAL>∀ {X Y : G.Elements} (f : X ⟶ Y), ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.map f).base = ↑f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : G.Elements<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).base = X.fst
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)<GOAL>((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).fiber = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>G : CategoryTheory.Functor C (Type w)<VAR>X : G.Elements<GOAL>↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.hom.app X) = CategoryTheory.CategoryStruct.id X.fst
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesFiniteEffectiveEpiFamilies<VAR>F.ReflectsFiniteEffectiveEpiFamilies<VAR>F.Full<VAR>F.Faithful<VAR>F.EffectivelyEnough<VAR>CategoryTheory.Precoherent D<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>(∃ α, ∃ (_ : Finite α), ∃ Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔ S ∈ (F.inducedTopology (CategoryTheory.coherentTopology D)).sieves X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesFiniteEffectiveEpiFamilies<VAR>F.ReflectsFiniteEffectiveEpiFamilies<VAR>F.Full<VAR>F.Faithful<VAR>F.EffectivelyEnough<VAR>CategoryTheory.Precoherent D<GOAL>CategoryTheory.coherentTopology C = F.inducedTopology (CategoryTheory.coherentTopology D)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesFiniteEffectiveEpiFamilies<VAR>F.ReflectsFiniteEffectiveEpiFamilies<VAR>F.Full<VAR>F.Faithful<VAR>F.EffectivelyEnough<VAR>CategoryTheory.Precoherent D<GOAL>CategoryTheory.CoverPreserving (CategoryTheory.coherentTopology C) (CategoryTheory.coherentTopology D) F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesEffectiveEpis<VAR>F.ReflectsEffectiveEpis<VAR>F.Full<VAR>F.Faithful<VAR>F.EffectivelyEnough<VAR>CategoryTheory.Preregular D<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>(∃ Y π, CategoryTheory.EffectiveEpi π ∧ S.arrows π) ↔ S ∈ (F.inducedTopology (CategoryTheory.regularTopology D)).sieves X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesEffectiveEpis<VAR>F.ReflectsEffectiveEpis<VAR>F.Full<VAR>F.Faithful<VAR>F.EffectivelyEnough<VAR>CategoryTheory.Preregular D<GOAL>CategoryTheory.regularTopology C = F.inducedTopology (CategoryTheory.regularTopology D)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesEffectiveEpis<VAR>F.ReflectsEffectiveEpis<VAR>F.Full<VAR>F.Faithful<VAR>F.EffectivelyEnough<VAR>CategoryTheory.Preregular D<GOAL>CategoryTheory.CoverPreserving (CategoryTheory.regularTopology C) (CategoryTheory.regularTopology D) F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryPreExtensive C<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F ∧ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F) ∧ CategoryTheory.regularTopology.EqualizerCondition F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<GOAL>∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A} (f : X ⟶ Y), (CategoryTheory.Presheaf.coherentExtensiveEquivalence.functor.map f).val = f.val
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<VAR>F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A<GOAL>(CategoryTheory.Presheaf.coherentExtensiveEquivalence.functor.obj F).val = F.val
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<GOAL>∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A} (f : X ⟶ Y), (CategoryTheory.Presheaf.coherentExtensiveEquivalence.inverse.map f).val = f.val
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<GOAL>CategoryTheory.Presheaf.coherentExtensiveEquivalence.counitIso = CategoryTheory.Iso.refl ({ obj := fun F => { val := F.val, cond := ⋯ }, map := fun {X Y} f => { val := f.val }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun F => { val := F.val, cond := ⋯ }, map := fun {X Y} f => { val := f.val }, map_id := ⋯, map_comp := ⋯ })
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<GOAL>CategoryTheory.Presheaf.coherentExtensiveEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<VAR>F : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A<GOAL>(CategoryTheory.Presheaf.coherentExtensiveEquivalence.inverse.obj F).val = F.val
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>s : CategoryTheory.Functor A B<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f<VAR>CategoryTheory.Limits.PreservesFiniteLimits s<VAR>hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>s : CategoryTheory.Functor A B<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f<VAR>CategoryTheory.Limits.ReflectsFiniteLimits s<VAR>hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>s : CategoryTheory.Functor A B<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<VAR>CategoryTheory.Limits.PreservesFiniteProducts s<VAR>hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>s : CategoryTheory.Functor A B<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>∀ (X : C), CategoryTheory.Projective X<VAR>CategoryTheory.Limits.ReflectsFiniteProducts s<VAR>hF : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P Q : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>p : CategoryTheory.Presieve.FamilyOfElements P R<VAR>φ : P ⟶ Q<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : R f<GOAL>p.map φ f hf = φ.app (Opposite.op Y) (p f hf)