ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>R' : CategoryTheory.Presieve X<VAR>h : R' ≤ R<GOAL>(CategoryTheory.Presieve.FamilyOfElements.restrict h p).map φ = CategoryTheory.Presieve.FamilyOfElements.restrict h (p.map φ)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>R.hasPullbacks<GOAL>x.Compatible ↔ x.PullbackCompatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R₁ R₂ : CategoryTheory.Presieve X<VAR>h : R₁ ≤ R₂<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R₂<GOAL>x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.restrict h x).Compatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>hx : x.Compatible<GOAL>x.sieveExtend.Compatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X Y : C<VAR>R : CategoryTheory.Presieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>t : x.Compatible<VAR>f : Y ⟶ X<VAR>hf : R f<GOAL>x.sieveExtend f ⋯ = x f hf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>t : x.Compatible<GOAL>CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x.sieveExtend = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P S.arrows<GOAL>x.Compatible ↔ x.SieveCompatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P S.arrows<VAR>t : x.Compatible<GOAL>x.SieveCompatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows<VAR>t : x.Compatible<GOAL>(CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x).sieveExtend = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x₁ x₂ : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows<VAR>t₁ : x₁.Compatible<VAR>t₂ : x₂.Compatible<GOAL>CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₁ = CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₂ → x₁ = x₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : { x // x.Compatible }<GOAL>↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible x) = (↑x).sieveExtend
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : { x // x.Compatible }<GOAL>↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible.symm x) = CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ ↑x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X Y : C<VAR>S : CategoryTheory.Sieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P S.arrows<VAR>t : x.Compatible<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>x (CategoryTheory.CategoryStruct.comp g f) ⋯ = P.map g.op (x f hf)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor D C<VAR>Z : D<VAR>T : CategoryTheory.Presieve (F.obj Z)<VAR>x : CategoryTheory.Presieve.FamilyOfElements P T<VAR>h : x.Compatible<GOAL>(CategoryTheory.Presieve.FamilyOfElements.functorPullback F x).Compatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X Y : C<VAR>S : CategoryTheory.Sieve X<VAR>f : Y ⟶ X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P S.arrows<VAR>h : x.Compatible<GOAL>(CategoryTheory.Presieve.FamilyOfElements.pullback f x).Compatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<GOAL>CategoryTheory.Presieve.FamilyOfElements.compPresheafMap (CategoryTheory.CategoryStruct.id P) x = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P Q U : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>f : P ⟶ Q<VAR>g : Q ⟶ U<GOAL>CategoryTheory.Presieve.FamilyOfElements.compPresheafMap g (CategoryTheory.Presieve.FamilyOfElements.compPresheafMap f x) = CategoryTheory.Presieve.FamilyOfElements.compPresheafMap (CategoryTheory.CategoryStruct.comp f g) x
<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>f : P ⟶ Q<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>h : x.Compatible<GOAL>(CategoryTheory.Presieve.FamilyOfElements.compPresheafMap f x).Compatible
<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>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>t : P.obj (Opposite.op X)<VAR>f : P ⟶ Q<VAR>h : x.IsAmalgamation t<GOAL>(CategoryTheory.Presieve.FamilyOfElements.compPresheafMap f x).IsAmalgamation (f.app (Opposite.op X) t)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>h : ∃ t, x.IsAmalgamation t<GOAL>x.Compatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R₁ R₂ : CategoryTheory.Presieve X<VAR>h : R₁ ≤ R₂<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R₂<VAR>t : P.obj (Opposite.op X)<VAR>ht : x.IsAmalgamation t<GOAL>(CategoryTheory.Presieve.FamilyOfElements.restrict h x).IsAmalgamation t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>t : P.obj (Opposite.op X)<VAR>ht : x.IsAmalgamation t<GOAL>x.sieveExtend.IsAmalgamation t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>hR : CategoryTheory.Presieve.IsSeparatedFor P R<VAR>t₁ t₂ : P.obj (Opposite.op X)<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P.map f.op t₁ = P.map f.op t₂<GOAL>t₁ = t₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<GOAL>CategoryTheory.Presieve.IsSeparatedFor P R ↔ CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.generate R).arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<GOAL>CategoryTheory.Presieve.IsSeparatedFor P ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>x : S.functor ⟶ P<VAR>g : CategoryTheory.yoneda.obj X ⟶ P<GOAL>CategoryTheory.CategoryStruct.comp S.functorInclusion g = x ↔ (↑(CategoryTheory.Presieve.natTransEquivCompatibleFamily x)).IsAmalgamation (CategoryTheory.yonedaEquiv g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<GOAL>CategoryTheory.Presieve.IsSheafFor P S.arrows ↔ CategoryTheory.Presieve.YonedaSheafCondition P S
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>h : CategoryTheory.Presieve.IsSheafFor P S.arrows<VAR>f : S.functor ⟶ P<GOAL>CategoryTheory.CategoryStruct.comp S.functorInclusion (h.extend f) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>h : CategoryTheory.Presieve.IsSheafFor P S.arrows<VAR>f : S.functor ⟶ P<VAR>t : CategoryTheory.yoneda.obj X ⟶ P<VAR>ht : CategoryTheory.CategoryStruct.comp S.functorInclusion t = f<GOAL>t = h.extend f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>h : CategoryTheory.Presieve.IsSheafFor P S.arrows<VAR>t₁ t₂ : CategoryTheory.yoneda.obj X ⟶ P<VAR>ht : CategoryTheory.CategoryStruct.comp S.functorInclusion t₁ = CategoryTheory.CategoryStruct.comp S.functorInclusion t₂<GOAL>t₁ = t₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<GOAL>(CategoryTheory.Presieve.IsSeparatedFor P R ∧ ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔ CategoryTheory.Presieve.IsSheafFor P R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>t : CategoryTheory.Presieve.IsSeparatedFor P R<GOAL>(∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) → CategoryTheory.Presieve.IsSheafFor P R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<GOAL>CategoryTheory.Presieve.IsSheafFor P R → CategoryTheory.Presieve.IsSeparatedFor P R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>t : CategoryTheory.Presieve.IsSheafFor P R<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>hx : x.Compatible<GOAL>x.IsAmalgamation (t.amalgamate x hx)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X Y : C<VAR>R : CategoryTheory.Presieve X<VAR>t : CategoryTheory.Presieve.IsSheafFor P R<VAR>x : CategoryTheory.Presieve.FamilyOfElements P R<VAR>hx : x.Compatible<VAR>f : Y ⟶ X<VAR>Hf : R f<GOAL>P.map f.op (t.amalgamate x hx) = x f Hf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<GOAL>CategoryTheory.Presieve.IsSheafFor P R ↔ CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.generate R).arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<GOAL>CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton (CategoryTheory.CategoryStruct.id X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<GOAL>CategoryTheory.Presieve.IsSheafFor P ⊤.arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>P' : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>i : P ≅ P'<GOAL>CategoryTheory.Presieve.IsSheafFor P R → CategoryTheory.Presieve.IsSheafFor P' R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>S : CategoryTheory.Sieve X<VAR>R : CategoryTheory.Presieve X<VAR>h : S.arrows ≤ R<VAR>hS : CategoryTheory.Presieve.IsSheafFor P S.arrows<VAR>trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f S).arrows<GOAL>CategoryTheory.Presieve.IsSheafFor P R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>S : CategoryTheory.Sieve X<VAR>R : CategoryTheory.Presieve X<VAR>h : S.arrows ≤ R<VAR>trans : ∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows<GOAL>CategoryTheory.Presieve.IsSheafFor P R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.ofArrows X π)<VAR>t : P.obj (Opposite.op B)<GOAL>x.IsAmalgamation t ↔ ∀ (i : I), P.map (π i).op t = x (π i) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>x : (i : I) → P.obj (Opposite.op (X i))<VAR>hx : CategoryTheory.Presieve.Arrows.Compatible P π x<GOAL>∃ x', ∀ (i : I), x' (π i) ⋯ = x i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>x : (i : I) → P.obj (Opposite.op (X i))<VAR>hx : CategoryTheory.Presieve.Arrows.Compatible P π x<VAR>i : I<GOAL>hx.familyOfElements (π i) ⋯ = x i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>x : (i : I) → P.obj (Opposite.op (X i))<VAR>hx : CategoryTheory.Presieve.Arrows.Compatible P π x<GOAL>hx.familyOfElements.Compatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<GOAL>CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>(CategoryTheory.Presieve.ofArrows X π).hasPullbacks<VAR>x : (i : I) → P.obj (Opposite.op (X i))<GOAL>CategoryTheory.Presieve.Arrows.Compatible P π x ↔ CategoryTheory.Presieve.Arrows.PullbackCompatible P π x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>(CategoryTheory.Presieve.ofArrows X π).hasPullbacks<GOAL>CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.PullbackCompatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>self : CategoryTheory.Pretopology C<VAR>X : C<VAR>S : CategoryTheory.Presieve X<VAR>Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y<GOAL>S ∈ self.coverings X → (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ self.coverings Y) → S.bind Ti ∈ self.coverings X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>self : CategoryTheory.Pretopology C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.Presieve.singleton f ∈ self.coverings X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>self : CategoryTheory.Pretopology C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S : CategoryTheory.Presieve X<GOAL>S ∈ self.coverings X → CategoryTheory.Presieve.pullbackArrows f S ∈ self.coverings Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>K₁ K₂ : CategoryTheory.Pretopology C<GOAL>K₁ ≤ K₂ ↔ K₁.coverings ≤ K₂.coverings
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>K : CategoryTheory.Pretopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ (CategoryTheory.Pretopology.toGrothendieck C K).sieves X ↔ ∃ R ∈ K.coverings X, R ≤ S.arrows
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>CategoryTheory.Pretopology.toGrothendieck C ⊥ = ⊥
<VAR>α : Type u<GOAL>∀ (x : Type u) (f : x ⟶ α), (CategoryTheory.discreteSieve α).arrows f = ∃ x_1, ∀ (y : x), f y = x_1
<VAR>α : Type u<GOAL>CategoryTheory.discreteSieve α ∈ CategoryTheory.typesGrothendieckTopology.sieves α
<VAR>α : Type u<GOAL>CategoryTheory.Sieve.generate (CategoryTheory.discretePresieve α) ∈ CategoryTheory.typesGrothendieckTopology.sieves α
<VAR>α : Type u<GOAL>CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology (CategoryTheory.yoneda.obj α)
<GOAL>∀ {X Y : Type u} (f : X ⟶ Y), (CategoryTheory.yoneda'.map f).val = CategoryTheory.yoneda.map f
<VAR>α : Type u<GOAL>(CategoryTheory.yoneda'.obj α).val = CategoryTheory.yoneda.obj α
<GOAL>CategoryTheory.yoneda'.comp (CategoryTheory.sheafOfTypesToPresheaf CategoryTheory.typesGrothendieckTopology) = CategoryTheory.yoneda
<VAR>S : CategoryTheory.Functor Type uᵒᵖ (Type u)<VAR>hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S<VAR>α : Type u<VAR>f : α → S.obj (Opposite.op PUnit.{u + 1})<GOAL>CategoryTheory.eval S α (CategoryTheory.typesGlue S hs α f) = f
<VAR>S : CategoryTheory.Functor Type uᵒᵖ (Type u)<VAR>hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (Opposite.op α)<GOAL>CategoryTheory.typesGlue S hs α (CategoryTheory.eval S α s) = s
<VAR>S : CategoryTheory.Functor Type uᵒᵖ (Type u)<VAR>hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (Opposite.op α)<VAR>x : α<GOAL>(CategoryTheory.evalEquiv S hs α) s x = CategoryTheory.eval S α s x
<VAR>S : CategoryTheory.Functor Type uᵒᵖ (Type u)<VAR>hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S<VAR>α : Type u<VAR>f : α → S.obj (Opposite.op PUnit.{u + 1})<GOAL>(CategoryTheory.evalEquiv S hs α).symm f = CategoryTheory.typesGlue S hs α f
<VAR>S : CategoryTheory.Functor Type uᵒᵖ (Type u)<VAR>α β : Type u<VAR>f : β ⟶ α<VAR>s : S.obj (Opposite.op α)<VAR>x : β<GOAL>CategoryTheory.eval S β (S.map f.op s) x = CategoryTheory.eval S α s (f x)
<VAR>S : CategoryTheory.Functor Type uᵒᵖ (Type u)<VAR>hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S<VAR>X : Type uᵒᵖ<GOAL>∀ (a : S.obj X), (CategoryTheory.equivYoneda S hs).hom.app X a = (CategoryTheory.evalEquiv S hs (Opposite.unop X)) a
<VAR>S : CategoryTheory.Functor Type uᵒᵖ (Type u)<VAR>hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S<VAR>X : Type uᵒᵖ<GOAL>∀ (a : (CategoryTheory.yoneda.obj (S.obj (Opposite.op PUnit.{u + 1}))).obj X), (CategoryTheory.equivYoneda S hs).inv.app X a = (CategoryTheory.evalEquiv S hs (Opposite.unop X)).symm a
<VAR>S : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology<GOAL>(CategoryTheory.equivYoneda' S).hom.val = (CategoryTheory.equivYoneda S.val ⋯).hom
<VAR>S : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology<GOAL>(CategoryTheory.equivYoneda' S).inv.val = (CategoryTheory.equivYoneda S.val ⋯).inv
<VAR>S₁ S₂ : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology<VAR>f : S₁ ⟶ S₂<VAR>α : Type u<VAR>s : S₁.val.obj (Opposite.op α)<VAR>x : α<GOAL>CategoryTheory.eval S₂.val α (f.val.app (Opposite.op α) s) x = f.val.app (Opposite.op PUnit.{u + 1}) (CategoryTheory.eval S₁.val α s x)
<GOAL>∀ {X Y : Type u} (f : X ⟶ Y) (Y_1 : Type uᵒᵖ) (g : ((fun X => { obj := fun Y => Opposite.unop Y ⟶ X, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp f.unop g, map_id := ⋯, map_comp := ⋯ }) X).obj Y_1) (a : Opposite.unop Y_1), (CategoryTheory.typeEquiv.functor.map f).val.app Y_1 g a = f (g a)
<VAR>α : Type u<VAR>Y : Type uᵒᵖ<GOAL>(CategoryTheory.typeEquiv.functor.obj α).val.obj Y = (Opposite.unop Y ⟶ α)
<VAR>X : Type u<GOAL>∀ (a : (CategoryTheory.Functor.id (Type u)).obj X), CategoryTheory.typeEquiv.unitIso.hom.app X a = CategoryTheory.CategoryStruct.comp ((CategoryTheory.evalEquiv (CategoryTheory.yoneda.obj X) ⋯ PUnit.{u + 1}) fun x => a) fun f => f PUnit.unit
<VAR>X : Type u<GOAL>∀ (a : (CategoryTheory.yoneda'.comp ((CategoryTheory.sheafOfTypesToPresheaf CategoryTheory.typesGrothendieckTopology).comp ((CategoryTheory.evaluation Type uᵒᵖ (Type u)).obj (Opposite.op PUnit.{u + 1})))).obj X), CategoryTheory.typeEquiv.unitIso.inv.app X a = (CategoryTheory.evalEquiv (CategoryTheory.yoneda.obj X) ⋯ PUnit.{u + 1}).symm (CategoryTheory.CategoryStruct.comp a fun x x_1 => x) PUnit.unit
<GOAL>∀ {X Y : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology} (f : X ⟶ Y) (a : ((CategoryTheory.evaluation Type uᵒᵖ (Type u)).obj (Opposite.op PUnit.{u + 1})).obj ((CategoryTheory.sheafOfTypesToPresheaf CategoryTheory.typesGrothendieckTopology).obj X)), CategoryTheory.typeEquiv.inverse.map f a = f.val.app (Opposite.op PUnit.{u + 1}) a
<VAR>X : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology<GOAL>∀ (X_1 : Type uᵒᵖ) (a : X.val.obj X_1), (CategoryTheory.typeEquiv.counitIso.inv.app X).val.app X_1 a = (CategoryTheory.evalEquiv X.val ⋯ (Opposite.unop X_1)) a
<VAR>X : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology<GOAL>∀ (X_1 : Type uᵒᵖ) (a : (CategoryTheory.yoneda.obj (X.val.obj (Opposite.op PUnit.{u + 1}))).obj X_1), (CategoryTheory.typeEquiv.counitIso.hom.app X).val.app X_1 a = (CategoryTheory.evalEquiv X.val ⋯ (Opposite.unop X_1)).symm a
<VAR>α : Type u<GOAL>∀ {X Y : Type uᵒᵖ} (f : X ⟶ Y) (g : Opposite.unop X ⟶ α) (a : Opposite.unop Y), (CategoryTheory.typeEquiv.functor.obj α).val.map f g a = g (f.unop a)
<VAR>X : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology<GOAL>CategoryTheory.typeEquiv.inverse.obj X = X.val.obj (Opposite.op PUnit.{u + 1})
<GOAL>CategoryTheory.Sheaf.Subcanonical CategoryTheory.typesGrothendieckTopology
<GOAL>CategoryTheory.typesGrothendieckTopology = CategoryTheory.Sheaf.canonicalTopology (Type u)
<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>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Preregular C<VAR>F G : Cᵒᵖ ⥤ D<VAR>f : F ⟶ G<GOAL>CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f ↔ ∀ (X : C) (y : (CategoryTheory.forget D).obj (G.obj (Opposite.op X))), ∃ X' φ, ∃ (_ : CategoryTheory.EffectiveEpi φ), ∃ x, (f.app (Opposite.op X')) x = (G.map (Opposite.op φ)) y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>CategoryTheory.Limits.PreservesFiniteProducts F<VAR>CategoryTheory.Limits.PreservesFiniteProducts G<VAR>h : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.extensiveTopology C) f<VAR>X : C<GOAL>Function.Surjective (f.app (Opposite.op 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>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ D<VAR>f : F ⟶ G<VAR>CategoryTheory.Limits.PreservesFiniteProducts F<VAR>CategoryTheory.Limits.PreservesFiniteProducts G<VAR>CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)<GOAL>CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.extensiveTopology C) f ↔ ∀ (X : C), Function.Surjective ⇑(f.app (Opposite.op 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>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.FinitaryExtensive C<VAR>F G : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) D<VAR>f : F ⟶ G<VAR>CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)<GOAL>CategoryTheory.Sheaf.IsLocallySurjective f ↔ ∀ (X : C), Function.Surjective ⇑(f.val.app (Opposite.op X))