ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>adj : L ⊣ R<VAR>i : L.comp R ≅ CategoryTheory.Functor.id C<GOAL>CategoryTheory.IsIso adj.unit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>adj : L ⊣ R<VAR>j : R.comp L ≅ CategoryTheory.Functor.id D<GOAL>CategoryTheory.IsIso adj.counit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<VAR>X : D<GOAL>((CategoryTheory.Monad.comparison h).obj X).a = R.map (h.counit.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<VAR>X : D<GOAL>((CategoryTheory.Monad.comparison h).obj X).A = R.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>∀ {X Y : D} (f : X ⟶ Y), ((CategoryTheory.Monad.comparison h).map f).f = R.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<VAR>X : D<GOAL>(CategoryTheory.Monad.comparisonForget h).hom.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.Monad.comparison h).comp h.toMonad.forget).obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<VAR>X : D<GOAL>(CategoryTheory.Monad.comparisonForget h).inv.app X = CategoryTheory.CategoryStruct.id (R.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>L.comp (CategoryTheory.Monad.comparison h) = h.toMonad.free
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Comonad.comparison h).map f).f = L.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<VAR>X : C<GOAL>((CategoryTheory.Comonad.comparison h).obj X).a = L.map (h.unit.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<VAR>X : C<GOAL>((CategoryTheory.Comonad.comparison h).obj X).A = L.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<VAR>X : C<GOAL>(CategoryTheory.Comonad.comparisonForget h).inv.app X = CategoryTheory.CategoryStruct.id (L.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<VAR>X : C<GOAL>(CategoryTheory.Comonad.comparisonForget h).hom.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.Comonad.comparison h).comp h.toComonad.forget).obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>R.comp (CategoryTheory.Comonad.comparison h) = h.toComonad.cofree
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>R : CategoryTheory.Functor D C<VAR>self : CategoryTheory.MonadicRightAdjoint R<GOAL>(CategoryTheory.Monad.comparison CategoryTheory.MonadicRightAdjoint.adj).IsEquivalence
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>self : CategoryTheory.ComonadicLeftAdjoint L<GOAL>(CategoryTheory.Comonad.comparison CategoryTheory.ComonadicLeftAdjoint.adj).IsEquivalence
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>R : CategoryTheory.Functor D C<VAR>R.Full<VAR>L : CategoryTheory.Functor C D<VAR>adj : L ⊣ R<GOAL>(CategoryTheory.Monad.comparison adj).Full
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>R : CategoryTheory.Functor D C<VAR>R.Full<VAR>L : CategoryTheory.Functor C D<VAR>adj : R ⊣ L<GOAL>(CategoryTheory.Comonad.comparison adj).Full
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>P.RespectsIso<VAR>hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P (CategoryTheory.Limits.pullback.fst f g)<GOAL>P.StableUnderBaseChange
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderBaseChange<GOAL>P.RespectsIso
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>X Y S : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>CategoryTheory.Limits.HasPullback f g<VAR>H : P g<GOAL>P (CategoryTheory.Limits.pullback.fst f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>X Y S : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>CategoryTheory.Limits.HasPullback f g<VAR>H : P f<GOAL>P (CategoryTheory.Limits.pullback.snd f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>S S' : C<VAR>f : S' ⟶ S<VAR>X : CategoryTheory.Over S<VAR>H : P X.hom<GOAL>P ((CategoryTheory.Over.pullback f).obj X).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>S S' : C<VAR>f : S' ⟶ S<VAR>X Y : CategoryTheory.Over S<VAR>g : X ⟶ Y<VAR>H : P g.left<GOAL>P ((CategoryTheory.Over.pullback f).map g).left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>P.IsStableUnderComposition<VAR>S X X' Y Y' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S<VAR>g' : Y' ⟶ S<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>h₁ : P i₁<VAR>h₂ : P i₂<VAR>e₁ : f = CategoryTheory.CategoryStruct.comp i₁ f'<VAR>e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g'<GOAL>P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>P.RespectsIso<VAR>hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P (CategoryTheory.Limits.pushout.inr f g)<GOAL>P.StableUnderCobaseChange
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderCobaseChange<GOAL>P.RespectsIso
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderCobaseChange<VAR>A B A' : C<VAR>f : A ⟶ A'<VAR>g : A ⟶ B<VAR>CategoryTheory.Limits.HasPushout f g<VAR>H : P g<GOAL>P (CategoryTheory.Limits.pushout.inl f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderCobaseChange<VAR>A B A' : C<VAR>f : A ⟶ A'<VAR>g : A ⟶ B<VAR>CategoryTheory.Limits.HasPushout f g<VAR>H : P f<GOAL>P (CategoryTheory.Limits.pushout.inr f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderCobaseChange<GOAL>P.op.StableUnderBaseChange
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>hP : P.StableUnderCobaseChange<GOAL>P.unop.StableUnderBaseChange
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderBaseChange<GOAL>P.op.StableUnderCobaseChange
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>hP : P.StableUnderBaseChange<GOAL>P.unop.StableUnderCobaseChange
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>hW : W.IsStableUnderLimitsOfShape J<VAR>X Y : CategoryTheory.Functor J C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>hf : W.functorCategory J f<GOAL>W (CategoryTheory.Limits.lim.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>J : Type u_1<VAR>W.RespectsIso<VAR>CategoryTheory.Limits.HasProductsOfShape J C<VAR>hW : ∀ (X₁ X₂ : J → C) (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Pi.map f)<GOAL>W.IsStableUnderProductsOfShape J
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.IsStableUnderFiniteProducts<VAR>J : Type<VAR>Finite J<GOAL>W.IsStableUnderProductsOfShape J
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>J : Type<VAR>Finite J<VAR>W.IsStableUnderFiniteProducts<GOAL>W.IsStableUnderProductsOfShape J
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>P : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>P.diagonal f ↔ P (CategoryTheory.Limits.pullback.diagonal f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>P : CategoryTheory.MorphismProperty C<VAR>P.IsStableUnderComposition<VAR>P.RespectsIso<VAR>hP'' : P.StableUnderBaseChange<GOAL>P.diagonal.IsStableUnderComposition
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>P.RespectsIso<GOAL>P.diagonal.StableUnderBaseChange
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<GOAL>P.universally.StableUnderBaseChange
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<GOAL>P.universally ≤ P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<GOAL>P.universally = P ↔ P.StableUnderBaseChange
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>hP : P.StableUnderBaseChange<GOAL>P.universally = P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>Monotone CategoryTheory.MorphismProperty.universally
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>j : J<GOAL>(CategoryTheory.Monad.ForgetCreatesLimits.γ D).app j = (D.obj j).a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>X : J<GOAL>(CategoryTheory.Monad.ForgetCreatesLimits.newCone D c).π.app X = CategoryTheory.CategoryStruct.comp (T.map (c.π.app X)) (D.obj X).a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).A = c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).a = t.lift (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).pt = CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>j : J<GOAL>((CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).π.app j).f = c.π.app j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>s : CategoryTheory.Limits.Cone D<GOAL>((CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit D c t).lift s).f = t.lift (T.forget.mapCone s)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>CategoryTheory.Limits.HasLimit (D.comp T.forget)<GOAL>CategoryTheory.Limits.HasLimit D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>j : J<GOAL>CategoryTheory.Monad.ForgetCreatesColimits.γ.app j = (D.obj j).a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<GOAL>(CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).pt = c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<GOAL>(CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).ι = CategoryTheory.CategoryStruct.comp CategoryTheory.Monad.ForgetCreatesColimits.γ c.ι
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<VAR>CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (T.map (c.ι.app j)) (CategoryTheory.Monad.ForgetCreatesColimits.lambda c t) = CategoryTheory.CategoryStruct.comp (D.obj j).a (c.ι.app j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<VAR>CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<GOAL>(CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).A = c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<VAR>CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<GOAL>(CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).a = CategoryTheory.Monad.ForgetCreatesColimits.lambda c t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<VAR>CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<VAR>j : J<GOAL>((CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).ι.app j).f = c.ι.app j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<VAR>CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<GOAL>(CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).pt = CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<VAR>CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<VAR>s : CategoryTheory.Limits.Cocone D<GOAL>((CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit c t).desc s).f = t.desc (T.forget.mapCocone s)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.Limits.PreservesColimitsOfShape J T.toFunctor<VAR>D : CategoryTheory.Functor J T.Algebra<VAR>CategoryTheory.Limits.HasColimit (D.comp T.forget)<GOAL>CategoryTheory.Limits.HasColimit D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : CategoryTheory.Functor J D<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasLimit (F.comp R)<VAR>CategoryTheory.Reflective R<GOAL>CategoryTheory.Limits.HasLimit F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective R<GOAL>CategoryTheory.Limits.HasLimitsOfShape J D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C<VAR>CategoryTheory.Reflective R<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective R<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<GOAL>CategoryTheory.Limits.HasColimitsOfShape J D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective R<VAR>CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C<GOAL>CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>j : J<GOAL>(CategoryTheory.Comonad.ForgetCreatesColimits'.γ D).app j = (D.obj j).a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>X : J<GOAL>(CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone D c).ι.app X = CategoryTheory.CategoryStruct.comp (D.obj X).a (T.map (c.ι.app X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint D c t).A = c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint D c t).a = t.desc (CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone D c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<GOAL>(CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone D c t).pt = CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint D c t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<VAR>j : J<GOAL>((CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone D c t).ι.app j).f = c.ι.app j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cocone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsColimit c<VAR>s : CategoryTheory.Limits.Cocone D<GOAL>((CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit D c t).desc s).f = t.desc (T.forget.mapCocone s)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>CategoryTheory.Limits.HasColimit (D.comp T.forget)<GOAL>CategoryTheory.Limits.HasColimit D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>j : J<GOAL>CategoryTheory.Comonad.ForgetCreatesLimits'.γ.app j = (D.obj j).a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<GOAL>(CategoryTheory.Comonad.ForgetCreatesLimits'.newCone c).pt = c.pt