ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>CategoryTheory.Projective Z<GOAL>(CategoryTheory.ProjectiveResolution.self Z).complex = (ChainComplex.single₀ C).obj Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X : C<VAR>πX : X ⟶ S<VAR>self : CategoryTheory.SmallObject.FunctorObjIndex f πX<GOAL>CategoryTheory.CategoryStruct.comp self.t πX = CategoryTheory.CategoryStruct.comp (f self.i) self.b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X : C<VAR>πX : X ⟶ S<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.ιFunctorObj f πX) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjLeft f πX) (CategoryTheory.SmallObject.ρFunctorObj f πX)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X : C<VAR>πX : X ⟶ S<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)<VAR>x : CategoryTheory.SmallObject.FunctorObjIndex f πX<GOAL>CategoryTheory.CategoryStruct.comp (f x.i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πX) x) (CategoryTheory.SmallObject.ρFunctorObj f πX)) = CategoryTheory.CategoryStruct.comp x.t (CategoryTheory.SmallObject.ιFunctorObj f πX)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X : C<VAR>πX : X ⟶ S<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX) (CategoryTheory.SmallObject.πFunctorObj f πX) = CategoryTheory.SmallObject.π'FunctorObj f πX
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X : C<VAR>πX : X ⟶ S<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) (CategoryTheory.SmallObject.πFunctorObj f πX) = πX
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X Y : C<VAR>πX : X ⟶ S<VAR>πY : Y ⟶ S<VAR>φ : X ⟶ Y<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C<VAR>hφ : CategoryTheory.CategoryStruct.comp φ πY = πX<VAR>i : I<VAR>t : A i ⟶ X<VAR>b : B i ⟶ S<VAR>w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b<VAR>t' : A i ⟶ Y<VAR>fac : CategoryTheory.CategoryStruct.comp t φ = t'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w }) (CategoryTheory.SmallObject.functorMapSrc f πX πY φ hφ) = CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjSrcFamily f πY) { i := i, t := t', b := b, w := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X Y : C<VAR>πX : X ⟶ S<VAR>πY : Y ⟶ S<VAR>φ : X ⟶ Y<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C<VAR>hφ : CategoryTheory.CategoryStruct.comp φ πY = πX<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMapSrc f πX πY φ hφ) (CategoryTheory.SmallObject.functorObjTop f πY) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX) φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X Y : C<VAR>πX : X ⟶ S<VAR>πY : Y ⟶ S<VAR>φ : X ⟶ Y<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C<VAR>hφ : CategoryTheory.CategoryStruct.comp φ πY = πX<VAR>i : I<VAR>t : A i ⟶ X<VAR>b : B i ⟶ S<VAR>w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b<VAR>t' : A i ⟶ Y<VAR>fac : CategoryTheory.CategoryStruct.comp t φ = t'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w }) (CategoryTheory.SmallObject.functorMapTgt f πX πY φ hφ) = CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πY) { i := i, t := t', b := b, w := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X Y : C<VAR>πX : X ⟶ S<VAR>πY : Y ⟶ S<VAR>φ : X ⟶ Y<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C<VAR>hφ : CategoryTheory.CategoryStruct.comp φ πY = πX<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjLeft f πX) (CategoryTheory.SmallObject.functorMapTgt f πX πY φ hφ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMapSrc f πX πY φ hφ) (CategoryTheory.SmallObject.functorObjLeft f πY)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X Y : C<VAR>πX : X ⟶ S<VAR>πY : Y ⟶ S<VAR>φ : X ⟶ Y<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C<VAR>hφ : CategoryTheory.CategoryStruct.comp φ πY = πX<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY) (CategoryTheory.SmallObject.functorObjLeft f πY)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMap f πX πY φ hφ) (CategoryTheory.SmallObject.πFunctorObj f πY) = CategoryTheory.SmallObject.πFunctorObj f πX
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S : C<VAR>X : C<VAR>πX : X ⟶ S<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)<GOAL>CategoryTheory.SmallObject.functorMap f πX πX (CategoryTheory.CategoryStruct.id X) ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.SmallObject.functorObj f πX)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X Y : C<VAR>πX : X ⟶ S<VAR>πY : Y ⟶ S<VAR>φ : X ⟶ Y<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C<VAR>hφ : CategoryTheory.CategoryStruct.comp φ πY = πX<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY) (CategoryTheory.SmallObject.functorObjLeft f πY)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) (CategoryTheory.SmallObject.functorMap f πX πY φ hφ) = CategoryTheory.CategoryStruct.comp φ (CategoryTheory.SmallObject.ιFunctorObj f πY)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X : C<VAR>πX : X ⟶ S<VAR>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)<VAR>i : I<VAR>t : A i ⟶ X<VAR>b : B i ⟶ S<VAR>sq : CategoryTheory.CommSq t (f i) πX b<GOAL>∃ l, CategoryTheory.CategoryStruct.comp (f i) l = CategoryTheory.CategoryStruct.comp t (CategoryTheory.SmallObject.ιFunctorObj f πX) ∧ CategoryTheory.CategoryStruct.comp l (CategoryTheory.SmallObject.πFunctorObj f πX) = b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S : C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>∀ {X : C} (πX : X ⟶ S), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>π : CategoryTheory.Over S<GOAL>(CategoryTheory.SmallObject.functor f S).obj π = CategoryTheory.Over.mk (CategoryTheory.SmallObject.πFunctorObj f π.hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S : C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>∀ {X : C} (πX : X ⟶ S), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>π₁ π₂ : CategoryTheory.Over S<VAR>φ : π₁ ⟶ π₂<GOAL>(CategoryTheory.SmallObject.functor f S).map φ = CategoryTheory.Over.homMk (CategoryTheory.SmallObject.functorMap f π₁.hom π₂.hom φ.left ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S : C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>∀ {X : C} (πX : X ⟶ S), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C<VAR>w : CategoryTheory.Over S<GOAL>(CategoryTheory.SmallObject.ε f S).app w = CategoryTheory.Over.homMk (CategoryTheory.SmallObject.ιFunctorObj f w.hom) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y : C<GOAL>EckmannHilton.IsUnital (fun x x_1 => CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y x x_1) 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y : C<GOAL>EckmannHilton.IsUnital (fun x x_1 => CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y x x_1) 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y : C<VAR>f g h k : X ⟶ Y<GOAL>CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y (CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y f g) (CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y h k) = CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y (CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y f h) (CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y g k)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>f + g = CategoryTheory.Limits.biprod.lift (𝟙 X) (𝟙 X) ≫ CategoryTheory.Limits.biprod.desc f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>f + g = CategoryTheory.Limits.biprod.lift f g ≫ CategoryTheory.Limits.biprod.desc (𝟙 Y) (𝟙 Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(f + g) ≫ h = f ≫ h + g ≫ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<GOAL>f ≫ (g + h) = f ≫ g + f ≫ h
<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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>X : C<VAR>W : (J.Cover X)ᵒᵖ<VAR>i : (Opposite.unop W).Arrow<GOAL>CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P X).hom.app W) (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (P.comp F)) i) = F.map (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) 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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<VAR>P : CategoryTheory.Functor Cᵒᵖ D<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ᵒᵖ<VAR>W : (J.Cover (Opposite.unop X))ᵒᵖ<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.colimit.ι (J.diagram P (Opposite.unop X)) W)) ((J.plusCompIso F P).hom.app X) = CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P (Opposite.unop X)).hom.app W) (CategoryTheory.Limits.colimit.ι (J.diagram (P.comp F) (Opposite.unop X)) W)
<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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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>F G : CategoryTheory.Functor D E<VAR>η : F ⟶ G<VAR>P : CategoryTheory.Functor Cᵒᵖ D<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>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ G<VAR>(X : C) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan G<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (J.plusObj P) η) (J.plusCompIso G P).hom = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (CategoryTheory.whiskerLeft 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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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>P : CategoryTheory.Functor Cᵒᵖ D<VAR>(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>(F : CategoryTheory.Functor D E) → (X : C) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<VAR>X : CategoryTheory.Functor D E<GOAL>(J.plusFunctorWhiskerLeftIso P).inv.app X = (J.plusCompIso X P).inv
<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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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>P : CategoryTheory.Functor Cᵒᵖ D<VAR>(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>(F : CategoryTheory.Functor D E) → (X : C) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<VAR>X : CategoryTheory.Functor D E<GOAL>(J.plusFunctorWhiskerLeftIso P).hom.app X = (J.plusCompIso X P).hom
<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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<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>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (J.plusMap η) F) (J.plusCompIso F Q).hom = CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (CategoryTheory.whiskerRight η 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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<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 : CategoryTheory.Functor Cᵒᵖ D<GOAL>(J.plusFunctorWhiskerRightIso F).inv.app X = (J.plusCompIso F X).inv
<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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<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 : CategoryTheory.Functor Cᵒᵖ D<GOAL>(J.plusFunctorWhiskerRightIso F).hom.app X = (J.plusCompIso F X).hom
<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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<VAR>P : CategoryTheory.Functor Cᵒᵖ D<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<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (J.toPlus P) F) (J.plusCompIso F P).hom = J.toPlus (P.comp 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>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} 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) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<VAR>P : CategoryTheory.Functor Cᵒᵖ D<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<GOAL>CategoryTheory.CategoryStruct.comp (J.toPlus (P.comp F)) (J.plusCompIso F P).inv = CategoryTheory.whiskerRight (J.toPlus P) F