ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>∀ {X Y : J} (f : X ⟶ Y), c.toCostructuredArrow.map f = CategoryTheory.CostructuredArrow.homMk f ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.HasColimit F<GOAL>∀ {X Y : J} (f : X ⟶ Y), (CategoryTheory.Limits.colimit.toCostructuredArrow F).map f = CategoryTheory.CostructuredArrow.homMk f ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.HasColimit F<VAR>j : J<GOAL>(CategoryTheory.Limits.colimit.toCostructuredArrow F).obj j = CategoryTheory.CostructuredArrow.mk (CategoryTheory.Limits.colimit.ι F j)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>X : J<GOAL>c.toCostructuredArrowCompProj.inv.app X = CategoryTheory.CategoryStruct.id X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>X : J<GOAL>c.toCostructuredArrowCompProj.hom.app X = CategoryTheory.CategoryStruct.id X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.proj F c.pt) = CategoryTheory.Functor.id J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>X : J<GOAL>c.toCostructuredArrowCompToOverCompForget.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>X : J<GOAL>c.toCostructuredArrowCompToOverCompForget.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>c.toCostructuredArrow.comp ((CategoryTheory.CostructuredArrow.toOver F c.pt).comp (CategoryTheory.Over.forget c.pt)) = F
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>j : J<GOAL>c.toOver.ι.app j = CategoryTheory.Over.homMk (c.ι.app j) ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>c.toOver.pt = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id c.pt)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.HasColimit F<VAR>j : J<GOAL>(CategoryTheory.Limits.colimit.toOver F).ι.app j = CategoryTheory.Over.homMk (CategoryTheory.Limits.colimit.ι F j) ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.HasColimit F<GOAL>(CategoryTheory.Limits.colimit.toOver F).pt = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit F))
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>c.mapCoconeToOver.inv.hom = CategoryTheory.CategoryStruct.id c.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>c.mapCoconeToOver.hom.hom = CategoryTheory.CategoryStruct.id c.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<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 : D<VAR>G : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F X)<GOAL>(CategoryTheory.Limits.Cocone.fromCostructuredArrow F G).pt = X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<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 : D<VAR>G : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F X)<VAR>j : J<GOAL>(CategoryTheory.Limits.Cocone.fromCostructuredArrow F G).ι.app j = (G.obj j).hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>K : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone K<VAR>F : CategoryTheory.Functor C D<VAR>X : D<VAR>f : F.obj c.pt ⟶ X<GOAL>(c.toCostructuredArrowCocone F f).pt = CategoryTheory.CostructuredArrow.mk f
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>K : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone K<VAR>F : CategoryTheory.Functor C D<VAR>X : D<VAR>f : F.obj c.pt ⟶ X<VAR>j : J<GOAL>(c.toCostructuredArrowCocone F f).ι.app j = CategoryTheory.CostructuredArrow.homMk (c.ι.app j) ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>(CategoryTheory.Limits.Cocone.toStructuredArrow F).obj c = CategoryTheory.StructuredArrow.mk c.ι
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cocone.toStructuredArrow F).map f = CategoryTheory.StructuredArrow.homMk f.hom ⋯
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)<GOAL>((CategoryTheory.Limits.Cocone.fromStructuredArrow F).obj c).ι = c.hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)<GOAL>((CategoryTheory.Limits.Cocone.fromStructuredArrow F).obj c).pt = c.right
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocone.fromStructuredArrow F).map f).hom = f.right
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.obj c).left.as = PUnit.unit
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.obj c).hom = c.ι
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).inverse.obj c).ι = c.hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).inverse.obj c).pt = c.right
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>X : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.map f).left = CategoryTheory.CategoryStruct.id { as := PUnit.unit }
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).inverse.map f).hom = f.right
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.map f).right = f.hom
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.obj c).right = c.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<GOAL>CategoryTheory.Limits.HasColimit F ↔ CategoryTheory.Limits.HasInitial (CategoryTheory.Limits.Cocone F)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C ↔ (CategoryTheory.Functor.const J).IsRightAdjoint
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>hc.descCoconeMorphism s = (c.isColimitEquivIsInitial hc).to s
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor J C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsInitial c<VAR>s : CategoryTheory.Limits.Cocone F<GOAL>hc.to s = (c.isColimitEquivIsInitial.symm hc).descCoconeMorphism s
<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>X : D<VAR>self : F.EffectivePresentation X<GOAL>CategoryTheory.EffectiveEpi self.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>self : F.EffectivelyEnough<VAR>X : D<GOAL>Nonempty (F.EffectivePresentation X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>B X : C<VAR>f : X ⟶ B<VAR>CategoryTheory.Limits.HasPullback f f<VAR>hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)<GOAL>CategoryTheory.EffectiveEpi f
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>U : CategoryTheory.Functor B C<VAR>F : CategoryTheory.Functor C B<VAR>R : CategoryTheory.Functor A B<VAR>F' : CategoryTheory.Functor C A<VAR>adj₁ : F ⊣ U<VAR>adj₂ : F' ⊣ R.comp U<VAR>CategoryTheory.Limits.HasReflexiveCoequalizers A<VAR>(X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)<VAR>Y : A<VAR>X : B<GOAL>∀ (a : X ⟶ R.obj Y), (CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv R F' adj₁ adj₂ Y X).symm a = (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F'.map (U.map (adj₁.counit.app X))) (CategoryTheory.LiftAdjoint.otherMap R F' adj₁ adj₂ X))) Y).symm ⟨(adj₂.homEquiv (U.obj X) Y).symm (CategoryTheory.CategoryStruct.comp (adj₁.unit.app (U.obj X)) (U.map ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.LiftAdjoint.counitCoequalises adj₁ X) (R.obj Y)) a))), ⋯⟩
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>U : CategoryTheory.Functor B C<VAR>F : CategoryTheory.Functor C B<VAR>R : CategoryTheory.Functor A B<VAR>F' : CategoryTheory.Functor C A<VAR>adj₁ : F ⊣ U<VAR>adj₂ : F' ⊣ R.comp U<VAR>CategoryTheory.Limits.HasReflexiveCoequalizers A<VAR>(X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)<VAR>Y : A<VAR>X : B<GOAL>∀ (a : CategoryTheory.LiftAdjoint.constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y), (CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) a = (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.LiftAdjoint.counitCoequalises adj₁ X) (R.obj Y)).symm ⟨CategoryTheory.CategoryStruct.comp (F.map ((adj₂.homEquiv (U.obj X) Y) ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F'.map (U.map (adj₁.counit.app X))) (CategoryTheory.LiftAdjoint.otherMap R F' adj₁ adj₂ X))) Y) a))) (adj₁.counit.app (R.obj Y)), ⋯⟩
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>U : CategoryTheory.Functor B C<VAR>F : CategoryTheory.Functor C B<VAR>R : CategoryTheory.Functor A B<VAR>adj₁ : F ⊣ U<VAR>(X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)<VAR>CategoryTheory.Limits.HasReflexiveCoequalizers A<VAR>(R.comp U).IsRightAdjoint<GOAL>R.IsRightAdjoint
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>U : CategoryTheory.Functor B C<VAR>CategoryTheory.MonadicRightAdjoint U<VAR>R : CategoryTheory.Functor A B<VAR>CategoryTheory.Limits.HasReflexiveCoequalizers A<VAR>(R.comp U).IsRightAdjoint<GOAL>R.IsRightAdjoint
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>Q : CategoryTheory.Functor A B<VAR>V : CategoryTheory.Functor B D<VAR>U : CategoryTheory.Functor A C<VAR>R : CategoryTheory.Functor C D<VAR>comm : U.comp R ≅ Q.comp V<VAR>U.IsRightAdjoint<VAR>V.IsRightAdjoint<VAR>R.IsRightAdjoint<VAR>(X : B) → CategoryTheory.RegularEpi ((CategoryTheory.Adjunction.ofIsRightAdjoint V).counit.app X)<VAR>CategoryTheory.Limits.HasReflexiveCoequalizers A<GOAL>Q.IsRightAdjoint
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>Q : CategoryTheory.Functor A B<VAR>V : CategoryTheory.Functor B D<VAR>U : CategoryTheory.Functor A C<VAR>R : CategoryTheory.Functor C D<VAR>comm : U.comp R ≅ Q.comp V<VAR>U.IsRightAdjoint<VAR>CategoryTheory.MonadicRightAdjoint V<VAR>R.IsRightAdjoint<VAR>CategoryTheory.Limits.HasReflexiveCoequalizers A<GOAL>Q.IsRightAdjoint
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>Small.{v, u₂} K<VAR>j : J<VAR>G : J ⥤ K ⥤ Type v<VAR>x y : (G ⋙ CategoryTheory.Limits.lim).obj j<VAR>w : ∀ (k : K), CategoryTheory.Limits.limit.π (G.obj j) k x = CategoryTheory.Limits.limit.π (G.obj j) k y<GOAL>x = y
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>Small.{v, u₂} K<VAR>F : J × K ⥤ Type v<VAR>CategoryTheory.IsFiltered K<VAR>Finite J<GOAL>Function.Injective (CategoryTheory.Limits.colimitLimitToLimitColimit F)
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>Small.{v, u₂} K<VAR>CategoryTheory.FinCategory J<VAR>F : J × K ⥤ Type v<VAR>CategoryTheory.IsFiltered K<GOAL>Function.Surjective (CategoryTheory.Limits.colimitLimitToLimitColimit F)
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>Small.{v, u₂} K<VAR>CategoryTheory.FinCategory J<VAR>CategoryTheory.IsFiltered K<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.Limits.HasColimitsOfShape K C<VAR>CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget C)<VAR>F : J ⥤ K ⥤ C<VAR>a : K<VAR>b : J<GOAL>CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.limit F) a ≫ (CategoryTheory.Limits.colimitLimitIso F).hom ≫ CategoryTheory.Limits.limit.π (CategoryTheory.Limits.colimit F.flip) b = (CategoryTheory.Limits.limit.π F b).app a ≫ (CategoryTheory.Limits.colimit.ι F.flip a).app b
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (a : (CategoryTheory.yoneda.obj F).obj ((CategoryTheory.Functor.const J).op.obj X)) (X_1 : J), (F.cones.map f a).app X_1 = f.unop ≫ a.app X_1
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>X : Cᵒᵖ<GOAL>F.cones.obj X = ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<GOAL>∀ {X Y : C} (f : X ⟶ Y) (a : (CategoryTheory.coyoneda.obj (Opposite.op F)).obj ((CategoryTheory.Functor.const J).obj X)) (X_1 : J), (F.cocones.map f a).app X_1 = a.app X_1 ≫ f
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>X : C<GOAL>F.cocones.obj X = (F ⟶ (CategoryTheory.Functor.const J).obj X)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>∀ {X Y : J ⥤ C} (f : X ⟶ Y) (X_1 : Cᵒᵖ) (a : (CategoryTheory.yoneda.obj X).obj ((CategoryTheory.Functor.const J).op.obj X_1)) (X_2 : J), (((CategoryTheory.cones J C).map f).app X_1 a).app X_2 = a.app X_2 ≫ f.app X_2
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (a : (CategoryTheory.yoneda.obj F).obj ((CategoryTheory.Functor.const J).op.obj X)) (X_1 : J), (((CategoryTheory.cones J C).obj F).map f a).app X_1 = f.unop ≫ a.app X_1
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>X : Cᵒᵖ<GOAL>((CategoryTheory.cones J C).obj F).obj X = ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<GOAL>∀ {X Y : (J ⥤ C)ᵒᵖ} (f : X ⟶ Y) (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj ((CategoryTheory.Functor.const J).obj X_1)) (X_2 : J), (((CategoryTheory.cocones J C).map f).app X_1 a).app X_2 = f.unop.app X_2 ≫ a.app X_2
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : (J ⥤ C)ᵒᵖ<GOAL>∀ {X Y : C} (f : X ⟶ Y) (a : (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.unop F))).obj ((CategoryTheory.Functor.const J).obj X)) (X_1 : J), (((CategoryTheory.cocones J C).obj F).map f a).app X_1 = a.app X_1 ≫ f
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : (J ⥤ C)ᵒᵖ<VAR>X : C<GOAL>((CategoryTheory.cocones J C).obj F).obj X = (Opposite.unop F ⟶ (CategoryTheory.Functor.const J).obj X)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>c.π.app j ≫ F.map f = c.π.app j'
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ c.ι.app j' = c.ι.app j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cone.equiv F).hom c).snd = c.π
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : (X : Cᵒᵖ) × F.cones.obj X<GOAL>((CategoryTheory.Limits.Cone.equiv F).inv c).π = c.snd
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : (X : Cᵒᵖ) × F.cones.obj X<GOAL>((CategoryTheory.Limits.Cone.equiv F).inv c).pt = Opposite.unop c.fst
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<GOAL>((CategoryTheory.Limits.Cone.equiv F).hom c).fst = Opposite.op c.pt
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<VAR>X : Cᵒᵖ<VAR>f : (CategoryTheory.yoneda.obj c.pt ⋙ CategoryTheory.uliftFunctor.{u₁, v₃}).obj X<GOAL>c.extensions.app X f = (CategoryTheory.Functor.const J).map f.down ≫ c.π