ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>F G : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op)<VAR>x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows<VAR>hx : x.Compatible<VAR>Y : C<VAR>g : Y ⟶ X<VAR>Z : C<VAR>p : Z ⟶ Y<VAR>hp : S.arrows (CategoryTheory.CategoryStruct.comp p g)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.PresheafHom.IsSheafFor.app hG x hx g) (G.map p.op) = CategoryTheory.CategoryStruct.comp (F.map p.op) ((x (CategoryTheory.CategoryStruct.comp p g) hp).app (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Z))))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>F G : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op)<GOAL>CategoryTheory.Presieve.IsSheafFor (CategoryTheory.presheafHom F G) S.arrows
<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>F G : CategoryTheory.Functor Cᵒᵖ A<VAR>hG : CategoryTheory.Presheaf.IsSheaf J G<GOAL>CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.presheafHom F G)
<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>F G : CategoryTheory.Sheaf J A<VAR>φ : F ⟶ G<VAR>X : Cᵒᵖ<GOAL>↑((CategoryTheory.sheafHomSectionsEquiv F G).symm φ) X = (J.overPullback A (Opposite.unop X)).map φ
<VAR>V : Type u<VAR>Quiver V<VAR>X Y : CategoryTheory.Paths (Quiver.Symmetrify V)<VAR>p q : X ⟶ Y<GOAL>CategoryTheory.Quotient.CompClosure CategoryTheory.Groupoid.Free.redStep p q → CategoryTheory.Quotient.CompClosure CategoryTheory.Groupoid.Free.redStep (Quiver.Path.reverse p) (Quiver.Path.reverse q)
<VAR>V : Type u<VAR>Quiver V<VAR>X Y : CategoryTheory.Paths (Quiver.Symmetrify V)<VAR>p : X ⟶ Y<GOAL>Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Groupoid.Free.redStep) (CategoryTheory.CategoryStruct.comp p (Quiver.Path.reverse p)) = Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Groupoid.Free.redStep) (CategoryTheory.CategoryStruct.id X)
<VAR>V : Type u<VAR>Quiver V<VAR>X Y : CategoryTheory.Paths (Quiver.Symmetrify V)<VAR>p : X ⟶ Y<GOAL>Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Groupoid.Free.redStep) (CategoryTheory.CategoryStruct.comp (Quiver.Path.reverse p) p) = Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Groupoid.Free.redStep) (CategoryTheory.CategoryStruct.id Y)
<VAR>V : Type u<VAR>Quiver V<GOAL>CategoryTheory.Groupoid.Free.of V = Quiver.Symmetrify.of ⋙q CategoryTheory.Paths.of ⋙q (CategoryTheory.Quotient.functor CategoryTheory.Groupoid.Free.redStep).toPrefunctor
<VAR>V : Type u<VAR>Quiver V<VAR>V' : Type u'<VAR>CategoryTheory.Groupoid V'<VAR>φ : V ⥤q V'<GOAL>CategoryTheory.Groupoid.Free.of V ⋙q (CategoryTheory.Groupoid.Free.lift φ).toPrefunctor = φ
<VAR>V : Type u<VAR>Quiver V<VAR>V' : Type u'<VAR>CategoryTheory.Groupoid V'<VAR>φ : V ⥤q V'<VAR>Φ : CategoryTheory.Functor (CategoryTheory.FreeGroupoid V) V'<VAR>hΦ : CategoryTheory.Groupoid.Free.of V ⋙q Φ.toPrefunctor = φ<GOAL>Φ = CategoryTheory.Groupoid.Free.lift φ
<VAR>V : Type u<VAR>Quiver V<GOAL>CategoryTheory.freeGroupoidFunctor (𝟭q V) = CategoryTheory.Functor.id (CategoryTheory.FreeGroupoid V)
<VAR>V : Type u<VAR>Quiver V<VAR>V' : Type u'<VAR>Quiver V'<VAR>V'' : Type u''<VAR>Quiver V''<VAR>φ : V ⥤q V'<VAR>φ' : V' ⥤q V''<GOAL>CategoryTheory.freeGroupoidFunctor (φ ⋙q φ') = (CategoryTheory.freeGroupoidFunctor φ).comp (CategoryTheory.freeGroupoidFunctor φ')
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : CategoryTheory.Core C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor D C<VAR>self : CategoryTheory.IsSkeletonOf C D F<GOAL>CategoryTheory.Skeletal D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor D C<VAR>self : CategoryTheory.IsSkeletonOf C D F<GOAL>F.IsEquivalence
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F₁ F₂ : CategoryTheory.Functor D C<VAR>Quiver.IsThin C<VAR>hC : CategoryTheory.Skeletal C<VAR>hF : F₁ ≅ F₂<GOAL>F₁ = F₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>Quiver.IsThin C<VAR>hC : CategoryTheory.Skeletal C<GOAL>CategoryTheory.Skeletal (CategoryTheory.Functor D C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : CategoryTheory.InducedCategory C Quotient.out} (f : X ⟶ Y), (CategoryTheory.fromSkeleton C).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ (a : Quotient (CategoryTheory.isIsomorphicSetoid C)), (CategoryTheory.fromSkeleton C).obj a = a.out
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.Skeletal (CategoryTheory.Skeleton C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.IsSkeletonOf C (CategoryTheory.Skeleton C) (CategoryTheory.fromSkeleton C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.toThinSkeleton C).map f = CategoryTheory.homOfLE ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>a : C<GOAL>(CategoryTheory.toThinSkeleton C).obj a = Quotient.mk' a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.ThinSkeleton C<GOAL>∀ (a : X ⟶ Y), (CategoryTheory.ThinSkeleton.map F).map a = Quotient.recOnSubsingleton₂ (motive := fun x x_1 => (x ⟶ x_1) → (Quotient.map F.obj ⋯ x ⟶ Quotient.map F.obj ⋯ x_1)) X Y (fun x y k => CategoryTheory.homOfLE ⋯) a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>∀ (a : Quotient (CategoryTheory.isIsomorphicSetoid C)), (CategoryTheory.ThinSkeleton.map F).obj a = Quotient.map F.obj ⋯ a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>F.comp (CategoryTheory.toThinSkeleton D) = (CategoryTheory.toThinSkeleton C).comp (CategoryTheory.ThinSkeleton.map F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<GOAL>∀ (a : CategoryTheory.ThinSkeleton C), (CategoryTheory.ThinSkeleton.map₂ F).obj a = CategoryTheory.ThinSkeleton.map₂Functor F a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<GOAL>∀ {X Y : CategoryTheory.ThinSkeleton C} (a : X ⟶ Y), (CategoryTheory.ThinSkeleton.map₂ F).map a = CategoryTheory.ThinSkeleton.map₂NatTrans F a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Quiver.IsThin C<VAR>x y : CategoryTheory.ThinSkeleton C<GOAL>∀ (a : x ⟶ y), (CategoryTheory.ThinSkeleton.fromThinSkeleton C).map a = Quotient.recOnSubsingleton₂ (motive := fun x x_1 => (x ⟶ x_1) → (Quotient.out x ⟶ Quotient.out x_1)) x y (fun X Y f => CategoryTheory.CategoryStruct.comp (Nonempty.some ⋯).hom (CategoryTheory.CategoryStruct.comp (Nonempty.some ⋯) (Nonempty.some ⋯).inv)) a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Quiver.IsThin C<GOAL>∀ (a : Quotient (CategoryTheory.isIsomorphicSetoid C)), (CategoryTheory.ThinSkeleton.fromThinSkeleton C).obj a = a.out
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Quiver.IsThin C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ X<GOAL>X ≈ Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Quiver.IsThin C<GOAL>CategoryTheory.Skeletal (CategoryTheory.ThinSkeleton C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>Quiver.IsThin C<VAR>F : CategoryTheory.Functor E D<VAR>G : CategoryTheory.Functor D C<GOAL>CategoryTheory.ThinSkeleton.map (F.comp G) = (CategoryTheory.ThinSkeleton.map F).comp (CategoryTheory.ThinSkeleton.map G)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Quiver.IsThin C<GOAL>CategoryTheory.ThinSkeleton.map (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.ThinSkeleton C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>Quiver.IsThin C<VAR>F₁ F₂ : CategoryTheory.Functor D C<VAR>h : F₁ ≅ F₂<GOAL>CategoryTheory.ThinSkeleton.map F₁ = CategoryTheory.ThinSkeleton.map F₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Quiver.IsThin C<GOAL>CategoryTheory.IsSkeletonOf C (CategoryTheory.ThinSkeleton C) (CategoryTheory.ThinSkeleton.fromThinSkeleton C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>self : J.PreservesSheafification F<GOAL>J.W ≤ J.W.inverseImage ((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>J.PreservesSheafification F<VAR>P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A<VAR>f : P₁ ⟶ P₂<VAR>hf : J.W f<GOAL>J.W (CategoryTheory.whiskerRight f F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>J.PreservesSheafification F<VAR>CategoryTheory.HasWeakSheafify J B<GOAL>J.W.IsInvertedBy (((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>CategoryTheory.HasWeakSheafify J B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>X : CategoryTheory.Functor Cᵒᵖ A<GOAL>(CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F).app X = (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J X) F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>CategoryTheory.HasWeakSheafify J B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>J.PreservesSheafification F<VAR>X : CategoryTheory.Functor Cᵒᵖ A<GOAL>(CategoryTheory.presheafToSheafCompComposeAndSheafifyIso J F).inv.app X = (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J X) F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)<VAR>adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A<VAR>G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)<VAR>adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B<GOAL>J.PreservesSheafification F ↔ ∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.IsIso (G₂.map (CategoryTheory.whiskerRight (adj₁.unit.app P) F))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)<VAR>adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A<VAR>G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)<VAR>adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B<VAR>J.HasSheafCompose F<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((CategoryTheory.sheafToPresheaf J B).map ((CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P)) = CategoryTheory.whiskerRight (adj₁.unit.app P) F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)<VAR>adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A<VAR>G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)<VAR>adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B<VAR>J.HasSheafCompose F<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>α : G₂.obj (P.comp F) ⟶ (CategoryTheory.sheafCompose J F).obj (G₁.obj P)<VAR>hα : CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((CategoryTheory.sheafToPresheaf J B).map α) = CategoryTheory.whiskerRight (adj₁.unit.app P) F<GOAL>α = (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)<VAR>adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A<VAR>G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)<VAR>adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B<VAR>J.HasSheafCompose F<GOAL>J.PreservesSheafification F ↔ CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} A<VAR>CategoryTheory.Category.{u_3, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>J.HasSheafCompose F<VAR>J.PreservesSheafification F<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) (CategoryTheory.sheafifyComposeIso J F P).hom = CategoryTheory.whiskerRight (CategoryTheory.toSheafify J P) F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} A<VAR>CategoryTheory.Category.{u_3, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify J B<VAR>J.HasSheafCompose F<VAR>J.PreservesSheafification F<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J P) F) (CategoryTheory.sheafifyComposeIso J F P).inv = CategoryTheory.toSheafify J (P.comp F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_3<VAR>E : Type u_4<VAR>CategoryTheory.Category.{max v u, u_3} D<VAR>CategoryTheory.Category.{max v u, u_4} E<VAR>F : CategoryTheory.Functor D E<VAR>∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D<VAR>∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>(X : C) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.ConcreteCategory E<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>(CategoryTheory.forget E).ReflectsIsomorphisms<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(CategoryTheory.sheafToPresheaf J E).map ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E)).app P) = (J.sheafifyCompIso F P).inv
<VAR>α β : Type u<GOAL>(α ⟶ β) = (α → β)
<VAR>X : Type u<GOAL>CategoryTheory.CategoryStruct.id X = id
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f g = g ∘ f
<VAR>X : Type u<VAR>x : X<GOAL>CategoryTheory.CategoryStruct.id X x = x
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : X<GOAL>CategoryTheory.CategoryStruct.comp f g x = g (f x)
<VAR>X Y : Type u<VAR>f : X ≅ Y<VAR>x : X<GOAL>f.inv (f.hom x) = x
<VAR>X Y : Type u<VAR>f : X ≅ Y<VAR>y : Y<GOAL>f.hom (f.inv y) = y
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : CategoryTheory.Functor J (Type w)<VAR>s : ↑F.sections<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f (↑s j) = ↑s j'
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : CategoryTheory.Functor J (Type w)<VAR>x y : ↑F.sections<GOAL>x = y ↔ ∀ (j : J), ↑x j = ↑y j
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : CategoryTheory.Functor J (Type w)<GOAL>(CategoryTheory.Functor.sectionsFunctor J).obj F = ↑F.sections
<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F G : CategoryTheory.Functor J (Type w)<VAR>φ : F ⟶ G<VAR>x : ↑F.sections<VAR>j : J<GOAL>↑((CategoryTheory.Functor.sectionsFunctor J).map φ x) j = φ.app j (↑x j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>a : F.obj X<GOAL>F.map (CategoryTheory.CategoryStruct.comp f g) a = F.map g (F.map f a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X : C<VAR>a : F.obj X<GOAL>F.map (CategoryTheory.CategoryStruct.id X) a = a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>X Y : C<VAR>σ : F ⟶ G<VAR>f : X ⟶ Y<VAR>x : F.obj X<GOAL>σ.app Y (F.map f x) = G.map f (σ.app X x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G H : CategoryTheory.Functor C (Type w)<VAR>X : C<VAR>σ : F ⟶ G<VAR>τ : G ⟶ H<VAR>x : F.obj X<GOAL>(CategoryTheory.CategoryStruct.comp σ τ).app X x = τ.app X (σ.app X x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X Y Z : C<VAR>p : X = Y<VAR>q : Y = Z<VAR>x : F.obj X<GOAL>F.map (CategoryTheory.eqToHom q) (F.map (CategoryTheory.eqToHom p) x) = F.map (CategoryTheory.eqToHom ⋯) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>σ : F ⟶ G<VAR>D : Type u'<VAR>𝒟 : CategoryTheory.Category.{u', u'} D<VAR>I J : CategoryTheory.Functor D C<VAR>ρ : I ⟶ J<VAR>W : D<VAR>x : (I.comp F).obj W<GOAL>(ρ ◫ σ).app W x = G.map (ρ.app W) (σ.app (I.obj W) x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X Y : C<VAR>f : X ≅ Y<VAR>x : F.obj X<GOAL>F.map f.inv (F.map f.hom x) = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C (Type w)<VAR>X Y : C<VAR>f : X ≅ Y<VAR>y : F.obj Y<GOAL>F.map f.hom (F.map f.inv y) = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>α : F ≅ G<VAR>X : C<VAR>x : F.obj X<GOAL>α.inv.app X (α.hom.app X x) = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C (Type w)<VAR>α : F ≅ G<VAR>X : C<VAR>x : G.obj X<GOAL>α.hom.app X (α.inv.app X x) = x
<VAR>X : Type u<GOAL>CategoryTheory.uliftFunctor.{v, u}.obj X = ULift.{v, u} X
<VAR>X Y : Type u<VAR>f : X ⟶ Y<VAR>x : ULift.{v, u} X<GOAL>CategoryTheory.uliftFunctor.{v, u}.map f x = { down := f x.down }
<VAR>X : Type u<VAR>x y : X<GOAL>CategoryTheory.homOfElement x = CategoryTheory.homOfElement y ↔ x = y
<VAR>X Y : Type u<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono f ↔ Function.Injective f
<VAR>X Y : Type u<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.Mono f<GOAL>Function.Injective f
<VAR>X Y : Type u<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ Function.Surjective f
<VAR>X Y : Type u<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.Epi f<GOAL>Function.Surjective f
<VAR>m : Type u → Type v<VAR>Functor m<VAR>LawfulFunctor m<GOAL>(CategoryTheory.ofTypeFunctor m).obj = m
<VAR>m : Type u → Type v<VAR>Functor m<VAR>LawfulFunctor m<VAR>α β : Type u<VAR>f : α → β<GOAL>(CategoryTheory.ofTypeFunctor m).map f = Functor.map f
<VAR>X Y : Type u<VAR>e : X ≃ Y<GOAL>e.toIso.hom = ⇑e
<VAR>X Y : Type u<VAR>e : X ≃ Y<GOAL>e.toIso.inv = ⇑e.symm
<VAR>X Y : Type u<VAR>i : X ≅ Y<GOAL>⇑i.toEquiv = i.hom
<VAR>X Y : Type u<VAR>i : X ≅ Y<GOAL>⇑i.toEquiv.symm = i.inv
<VAR>X : Type u<GOAL>(CategoryTheory.Iso.refl X).toEquiv = Equiv.refl X
<VAR>X Y Z : Type u<VAR>f : X ≅ Y<VAR>g : Y ≅ Z<GOAL>(f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv
<VAR>X Y : Type u<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f ↔ Function.Bijective f
<VAR>X Y : Type u<VAR>i : X ≅ Y<GOAL>equivIsoIso.inv i = i.toEquiv
<VAR>X Y : Type u<VAR>e : X ≃ Y<GOAL>equivIsoIso.hom e = e.toIso
<VAR>X Y : Type u<VAR>e : X ≃ Y<GOAL>equivEquivIso e = e.toIso
<VAR>X Y : Type u<VAR>e : X ≅ Y<GOAL>equivEquivIso.symm e = e.toEquiv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>G : C ⥤ D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>self : G.IsCocontinuous J K<VAR>U : C<VAR>S : CategoryTheory.Sieve (G.obj U)<GOAL>S ∈ K.sieves (G.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J.sieves U
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>G : C ⥤ D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCocontinuous J K<VAR>U : C<VAR>S : CategoryTheory.Sieve (G.obj U)<VAR>hS : S ∈ K.sieves (G.obj U)<GOAL>CategoryTheory.Sieve.functorPullback G S ∈ J.sieves U
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>G : C ⥤ D<VAR>G' : D ⥤ E<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>L : CategoryTheory.GrothendieckTopology E<VAR>G.IsCocontinuous J K<VAR>G'.IsCocontinuous K L<GOAL>(G ⋙ G').IsCocontinuous J L