ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<VAR>η : A ⟶ B<VAR>CategoryTheory.IsIso η<VAR>s : CategoryTheory.Limits.Cocone (P.F.comp CategoryTheory.yoneda)<VAR>X : Cᵒᵖ<GOAL>∀ (a : (P.cocone.extend η).pt.obj X), ((P.extend η).isColimit.desc s).app X a = (P.coconeIsColimit.desc s).app X (CategoryTheory.inv (η.app X) a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<VAR>X : P.I<GOAL>(P.toCostructuredArrow.obj X).hom = P.cocone.ι.app X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<VAR>X : P.I<GOAL>(P.toCostructuredArrow.obj X).right.as = PUnit.unit
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<GOAL>∀ {X Y : P.I} (f : X ⟶ Y), (P.toCostructuredArrow.map f).left = P.F.map f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<VAR>X : P.I<GOAL>(P.toCostructuredArrow.obj X).left = P.F.obj X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(CategoryTheory.Limits.IndObjectPresentation.yoneda X).F = CategoryTheory.Functor.fromPUnit X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(CategoryTheory.Limits.IndObjectPresentation.yoneda X).I = CategoryTheory.Discrete PUnit.{v + 1}
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>(CategoryTheory.Limits.IndObjectPresentation.yoneda X).ℐ = CategoryTheory.discreteCategory PUnit.{v + 1}
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>s : CategoryTheory.Discrete PUnit.{v + 1}<GOAL>(CategoryTheory.Limits.IndObjectPresentation.yoneda X).ι.app s = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.fromPUnit X).comp CategoryTheory.yoneda).obj s)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>s : CategoryTheory.Limits.Cocone ((CategoryTheory.Functor.fromPUnit X).comp CategoryTheory.yoneda)<GOAL>(CategoryTheory.Limits.IndObjectPresentation.yoneda X).isColimit.desc s = s.ι.app { as := PUnit.unit }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>self : CategoryTheory.Limits.IsIndObject A<GOAL>Nonempty (CategoryTheory.Limits.IndObjectPresentation A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>P : CategoryTheory.Limits.IndObjectPresentation A<GOAL>CategoryTheory.Limits.IsIndObject A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>CategoryTheory.Limits.IsIndObject (CategoryTheory.yoneda.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : A ⟶ B<VAR>CategoryTheory.IsIso η<GOAL>CategoryTheory.Limits.IsIndObject A → CategoryTheory.Limits.IsIndObject B
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : A ⟶ B<VAR>CategoryTheory.IsIso η<GOAL>CategoryTheory.Limits.IsIndObject A ↔ CategoryTheory.Limits.IsIndObject B
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>h : CategoryTheory.Limits.IsIndObject A<GOAL>CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>h : CategoryTheory.Limits.IsIndObject A<GOAL>CategoryTheory.FinallySmall (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)<VAR>CategoryTheory.FinallySmall (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)<GOAL>CategoryTheory.Limits.IsIndObject A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>CategoryTheory.Limits.IsIndObject A ↔ CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) ∧ CategoryTheory.FinallySmall (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>K : CategoryTheory.Functor J (Type u)<VAR>c : CategoryTheory.Limits.Cocone K<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u})<VAR>s : Set c.pt<VAR>ls : Set lc.pt<GOAL>CategoryTheory.Limits.Types.descSet hc ls = s ↔ ∀ (j : J) (x : K.obj j), lc.ι.app j { down := x } ∈ ls ↔ c.ι.app j x ∈ s
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>K : CategoryTheory.Functor J (Type u)<VAR>c : CategoryTheory.Limits.Cocone K<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u})<VAR>x : lc.pt<VAR>j : J<VAR>y : K.obj j<GOAL>c.ι.app j y ∈ CategoryTheory.Limits.Types.descSet hc {x} ↔ lc.ι.app j { down := y } = x
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>K : CategoryTheory.Functor J (Type u)<VAR>c : CategoryTheory.Limits.Cocone K<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u})<GOAL>CategoryTheory.Limits.Types.descSet hc Set.univ = Set.univ
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>K : CategoryTheory.Functor J (Type u)<VAR>c : CategoryTheory.Limits.Cocone K<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u})<GOAL>⋃ x, CategoryTheory.Limits.Types.descSet hc {x} = Set.univ
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>K : CategoryTheory.Functor J (Type u)<VAR>c : CategoryTheory.Limits.Cocone K<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u})<GOAL>CategoryTheory.Limits.Types.descSet hc ∅ = ∅
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>K : CategoryTheory.Functor J (Type u)<VAR>c : CategoryTheory.Limits.Cocone K<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u})<VAR>x y : lc.pt<VAR>hn : x ≠ y<GOAL>CategoryTheory.Limits.Types.descSet hc {x} ∩ CategoryTheory.Limits.Types.descSet hc {y} = ∅
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>K : CategoryTheory.Functor J (Type u)<VAR>c : CategoryTheory.Limits.Cocone K<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u})<VAR>x : c.pt<GOAL>∃! y, x ∈ CategoryTheory.Limits.Types.descSet hc {y}
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>K : CategoryTheory.Functor J (Type u)<VAR>c : CategoryTheory.Limits.Cocone K<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u})<VAR>x : c.pt<VAR>y : lc.pt<GOAL>CategoryTheory.Limits.Types.descFun hc lc x = y ↔ x ∈ CategoryTheory.Limits.Types.descSet hc {y}
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} J<VAR>K : CategoryTheory.Functor J (Type u)<VAR>c : CategoryTheory.Limits.Cocone K<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u})<VAR>f : c.pt → lc.pt<GOAL>f = CategoryTheory.Limits.Types.descFun hc lc ↔ ∀ (j : J), f ∘ c.ι.app j = lc.ι.app j ∘ ULift.up
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>x y : (j : J) × F.obj j<GOAL>CategoryTheory.Limits.Types.Quot.Rel F x y → CategoryTheory.Limits.Types.FilteredColimit.Rel F x y
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>x y : (j : J) × F.obj j<GOAL>CategoryTheory.Limits.Types.FilteredColimit.Rel F x y → EqvGen (CategoryTheory.Limits.Types.Quot.Rel F) x y
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.IsFilteredOrEmpty J<GOAL>Equivalence (CategoryTheory.Limits.Types.FilteredColimit.Rel F)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.IsFilteredOrEmpty J<GOAL>CategoryTheory.Limits.Types.FilteredColimit.Rel F = EqvGen (CategoryTheory.Limits.Types.Quot.Rel F)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.IsFilteredOrEmpty J<VAR>CategoryTheory.Limits.HasColimit F<VAR>i j : J<VAR>xi : F.obj i<VAR>xj : F.obj j<GOAL>(CategoryTheory.Limits.Types.colimitCocone F).ι.app i xi = (CategoryTheory.Limits.Types.colimitCocone F).ι.app j xj ↔ CategoryTheory.Limits.Types.FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.IsFilteredOrEmpty J<VAR>CategoryTheory.Limits.HasColimit F<VAR>t : CategoryTheory.Limits.Cocone F<VAR>ht : CategoryTheory.Limits.IsColimit t<VAR>i j : J<VAR>xi : F.obj i<VAR>xj : F.obj j<GOAL>t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.IsFilteredOrEmpty J<VAR>CategoryTheory.Limits.HasColimit F<VAR>i j : J<VAR>xi : F.obj i<VAR>xj : F.obj j<GOAL>CategoryTheory.Limits.colimit.ι F i xi = CategoryTheory.Limits.colimit.ι F j xj ↔ ∃ k f g, F.map f xi = F.map g xj
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>J : Type v₂<VAR>CategoryTheory.SmallCategory J<VAR>K : J ⥤ C<VAR>X : C<VAR>Y : J<GOAL>(CategoryTheory.ProdPreservesConnectedLimits.γ₂ X).app Y = CategoryTheory.Limits.prod.snd
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>J : Type v₂<VAR>CategoryTheory.SmallCategory J<VAR>K : J ⥤ C<VAR>X : C<VAR>Y : J<GOAL>(CategoryTheory.ProdPreservesConnectedLimits.γ₁ X).app Y = CategoryTheory.Limits.prod.fst
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>J : Type v₂<VAR>CategoryTheory.SmallCategory J<VAR>X : C<VAR>K : J ⥤ C<VAR>s : CategoryTheory.Limits.Cone (K ⋙ CategoryTheory.Limits.prod.functor.obj X)<GOAL>(CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).pt = s.pt
<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>J : Type v₂<VAR>CategoryTheory.SmallCategory J<VAR>X : C<VAR>K : J ⥤ C<VAR>s : CategoryTheory.Limits.Cone (K ⋙ CategoryTheory.Limits.prod.functor.obj X)<GOAL>(CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).π = s.π ≫ CategoryTheory.ProdPreservesConnectedLimits.γ₂ X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>X_1 : CategoryTheory.Discrete PEmpty.{1}<GOAL>(CategoryTheory.Limits.asEmptyCone X).π.app X_1 = id (CategoryTheory.Discrete.casesOn X_1 fun as => ⋯.elim)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.Limits.asEmptyCone X).pt = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.Limits.asEmptyCocone X).pt = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>X_1 : CategoryTheory.Discrete PEmpty.{1}<GOAL>(CategoryTheory.Limits.asEmptyCocone X).ι.app X_1 = id (CategoryTheory.Discrete.casesOn X_1 fun as => ⋯.elim)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.IsTerminal X<VAR>f g : Y ⟶ X<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Z : C<VAR>t : CategoryTheory.Limits.IsTerminal Z<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>f ≫ t.from Y = t.from X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>t : CategoryTheory.Limits.IsTerminal X<GOAL>t.from X = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.IsInitial X<VAR>f g : X ⟶ Y<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>t : CategoryTheory.Limits.IsInitial X<VAR>Y Z : C<VAR>f : Y ⟶ Z<GOAL>t.to Y ≫ f = t.to Z
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>t : CategoryTheory.Limits.IsInitial X<GOAL>t.to X = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.IsTerminal X<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsSplitMono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.IsInitial X<VAR>f : Y ⟶ X<GOAL>CategoryTheory.IsSplitEpi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.IsTerminal X<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : CategoryTheory.Limits.IsInitial X<VAR>f : Y ⟶ X<GOAL>CategoryTheory.Epi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T T' : C<VAR>hT : CategoryTheory.Limits.IsTerminal T<VAR>hT' : CategoryTheory.Limits.IsTerminal T'<GOAL>(hT.uniqueUpToIso hT').inv = hT.from T'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T T' : C<VAR>hT : CategoryTheory.Limits.IsTerminal T<VAR>hT' : CategoryTheory.Limits.IsTerminal T'<GOAL>(hT.uniqueUpToIso hT').hom = hT'.from T
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I I' : C<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>hI' : CategoryTheory.Limits.IsInitial I'<GOAL>(hI.uniqueUpToIso hI').hom = hI.to I'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I I' : C<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>hI' : CategoryTheory.Limits.IsInitial I'<GOAL>(hI.uniqueUpToIso hI').inv = hI'.to I
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F₁ : CategoryTheory.Discrete PEmpty.{w + 1} ⥤ C<VAR>F₂ : CategoryTheory.Discrete PEmpty.{w' + 1} ⥤ C<VAR>h : CategoryTheory.Limits.HasLimit F₁<GOAL>CategoryTheory.Limits.HasLimit F₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>h : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{w + 1}) C<GOAL>CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{w' + 1}) C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F₁ : CategoryTheory.Discrete PEmpty.{w + 1} ⥤ C<VAR>F₂ : CategoryTheory.Discrete PEmpty.{w' + 1} ⥤ C<VAR>h : CategoryTheory.Limits.HasColimit F₁<GOAL>CategoryTheory.Limits.HasColimit F₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>h : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete PEmpty.{w + 1}) C<GOAL>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete PEmpty.{w' + 1}) C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>h : (Y : C) → Unique (Y ⟶ X)<GOAL>CategoryTheory.Limits.HasTerminal C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>h : CategoryTheory.Limits.IsTerminal X<GOAL>CategoryTheory.Limits.HasTerminal C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>h : (Y : C) → Unique (X ⟶ Y)<GOAL>CategoryTheory.Limits.HasInitial C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>h : CategoryTheory.Limits.IsInitial X<GOAL>CategoryTheory.Limits.HasInitial C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>P : C<VAR>f g : P ⟶ ⊤_ C<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>P : C<VAR>f g : ⊥_ C ⟶ P<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>f ≫ CategoryTheory.Limits.terminal.from Q = CategoryTheory.Limits.terminal.from P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>CategoryTheory.Limits.initial.to P ≫ f = CategoryTheory.Limits.initial.to Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasInitial Cᵒᵖ<GOAL>CategoryTheory.Limits.HasTerminal C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasTerminal Cᵒᵖ<GOAL>CategoryTheory.Limits.HasInitial C
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>CategoryTheory.Limits.limitConstTerminal.hom = CategoryTheory.Limits.terminal.from (CategoryTheory.Limits.limit ((CategoryTheory.Functor.const J).obj (⊤_ C)))
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>j : J<GOAL>CategoryTheory.Limits.limitConstTerminal.inv ≫ CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j = CategoryTheory.Limits.terminal.from (⊤_ C)
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasInitial C<GOAL>CategoryTheory.Limits.colimitConstInitial.inv = CategoryTheory.Limits.initial.to (CategoryTheory.Limits.colimit ((CategoryTheory.Functor.const J).obj (⊥_ C)))
<VAR>J : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>j : J<GOAL>CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j ≫ CategoryTheory.Limits.colimitConstInitial.hom = CategoryTheory.Limits.initial.to (⊥_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : CategoryTheory.Limits.InitialMonoClass C<VAR>I : C<VAR>X : C<VAR>hI : CategoryTheory.Limits.IsInitial I<GOAL>CategoryTheory.Mono (hI.to X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.InitialMonoClass C<VAR>I X : C<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>f : I ⟶ X<GOAL>CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I : C<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>h : ∀ (X : C), CategoryTheory.Mono (hI.to X)<GOAL>CategoryTheory.Limits.InitialMonoClass C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>h : ∀ (X : C), CategoryTheory.Mono (CategoryTheory.Limits.initial.to X)<GOAL>CategoryTheory.Limits.InitialMonoClass C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>I T : C<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>hT : CategoryTheory.Limits.IsTerminal T<GOAL>CategoryTheory.Mono (hI.to T) → CategoryTheory.Limits.InitialMonoClass C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>h : CategoryTheory.Mono (CategoryTheory.Limits.initial.to (⊤_ C))<GOAL>CategoryTheory.Limits.InitialMonoClass C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>X : J<VAR>tX : CategoryTheory.Limits.IsInitial X<VAR>F : J ⥤ C<GOAL>(CategoryTheory.Limits.coneOfDiagramInitial tX F).pt = F.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>X : J<VAR>tX : CategoryTheory.Limits.IsInitial X<VAR>F : J ⥤ C<VAR>j : J<GOAL>(CategoryTheory.Limits.coneOfDiagramInitial tX F).π.app j = F.map (tX.to j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>X : J<VAR>hX : CategoryTheory.Limits.IsTerminal X<VAR>F : J ⥤ C<VAR>∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)<VAR>i : J<GOAL>(CategoryTheory.Limits.coneOfDiagramTerminal hX F).π.app i = CategoryTheory.inv (F.map (hX.from i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>X : J<VAR>hX : CategoryTheory.Limits.IsTerminal X<VAR>F : J ⥤ C<VAR>∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)<GOAL>(CategoryTheory.Limits.coneOfDiagramTerminal hX F).pt = F.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>X : J<VAR>tX : CategoryTheory.Limits.IsTerminal X<VAR>F : J ⥤ C<VAR>j : J<GOAL>(CategoryTheory.Limits.coconeOfDiagramTerminal tX F).ι.app j = F.map (tX.from j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>X : J<VAR>tX : CategoryTheory.Limits.IsTerminal X<VAR>F : J ⥤ C<GOAL>(CategoryTheory.Limits.coconeOfDiagramTerminal tX F).pt = F.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>X : J<VAR>hX : CategoryTheory.Limits.IsTerminal X<GOAL>CategoryTheory.IsIso (c.ι.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>X : J<VAR>hX : CategoryTheory.Limits.IsInitial X<VAR>F : J ⥤ C<VAR>∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)<VAR>i : J<GOAL>(CategoryTheory.Limits.coconeOfDiagramInitial hX F).ι.app i = CategoryTheory.inv (F.map (hX.to i))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>X : J<VAR>hX : CategoryTheory.Limits.IsInitial X<VAR>F : J ⥤ C<VAR>∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)<GOAL>(CategoryTheory.Limits.coconeOfDiagramInitial hX F).pt = F.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ C<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>X : J<VAR>hX : CategoryTheory.Limits.IsInitial X<GOAL>CategoryTheory.IsIso (c.π.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>j : J<VAR>I : CategoryTheory.Limits.IsInitial j<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>j : J<VAR>I : CategoryTheory.Limits.IsTerminal j<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<VAR>∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>j : J<VAR>I : CategoryTheory.Limits.IsTerminal j<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>j : J<VAR>I : CategoryTheory.Limits.IsInitial j<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>hX : CategoryTheory.Limits.IsTerminal X<VAR>hY : CategoryTheory.Limits.IsTerminal Y<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>hX : CategoryTheory.Limits.IsInitial X<VAR>hY : CategoryTheory.Limits.IsInitial Y<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f
<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.EssentiallySmall.{w₁, v₂, u₂} J<VAR>CategoryTheory.Limits.HasLimitsOfSize.{w₁, w₁, v₁, u₁} C<GOAL>CategoryTheory.Limits.HasLimitsOfShape J C
<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.EssentiallySmall.{w₁, v₂, u₂} J<VAR>CategoryTheory.Limits.HasColimitsOfSize.{w₁, w₁, v₁, u₁} C<GOAL>CategoryTheory.Limits.HasColimitsOfShape J C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>β : Type w₂<VAR>Small.{w₁, w₂} β<VAR>CategoryTheory.Limits.HasProducts C<GOAL>CategoryTheory.Limits.HasProductsOfShape β C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>β : Type w₂<VAR>Small.{w₁, w₂} β<VAR>CategoryTheory.Limits.HasCoproducts C<GOAL>CategoryTheory.Limits.HasCoproductsOfShape β C