ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>X : CategoryTheory.Functor C D<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>(((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).obj P).p = X.map P.p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>X : CategoryTheory.Functor C D<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>(((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).obj P).X = X.obj P.X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<GOAL>∀ {X Y : CategoryTheory.Functor C D} (f : X ⟶ Y) (P : CategoryTheory.Idempotents.Karoubi C), (((CategoryTheory.Idempotents.functorExtension₂ C D).map f).app P).f = CategoryTheory.CategoryStruct.comp (f.app P.X) (Y.map P.p)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>X : CategoryTheory.Functor C D<GOAL>∀ {X_1 Y : CategoryTheory.Idempotents.Karoubi C} (f : X_1 ⟶ Y), (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).map f).f = X.map f.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>X : CategoryTheory.Functor C D<GOAL>∀ (X_1 : C), (((CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso C D).inv.app X).app X_1).f = CategoryTheory.CategoryStruct.id (X.obj X_1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>X : CategoryTheory.Functor C D<GOAL>∀ (X_1 : C), (((CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso C D).hom.app X).app X_1).f = CategoryTheory.CategoryStruct.id (X.obj X_1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.IsIdempotentComplete D<GOAL>(CategoryTheory.Idempotents.karoubiUniversal₂ C D).functor = CategoryTheory.Idempotents.functorExtension₂ C D
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.IsIdempotentComplete D<GOAL>∀ {X Y : CategoryTheory.Functor C D} (f : X ⟶ Y) (X_1 : CategoryTheory.Idempotents.Karoubi C), ((CategoryTheory.Idempotents.functorExtension C D).map f).app X_1 = (CategoryTheory.Idempotents.toKaroubiEquivalence D).inverse.map (((CategoryTheory.Idempotents.functorExtension₂ C D).map f).app X_1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.IsIdempotentComplete D<VAR>X : CategoryTheory.Functor C D<GOAL>∀ (X_1 : CategoryTheory.Idempotents.Karoubi C), ((CategoryTheory.Idempotents.functorExtension C D).obj X).obj X_1 = (CategoryTheory.Idempotents.toKaroubiEquivalence D).inverse.obj (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).obj X_1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.IsIdempotentComplete D<VAR>X : CategoryTheory.Functor C D<GOAL>∀ {X_1 Y : CategoryTheory.Idempotents.Karoubi C} (f : X_1 ⟶ Y), ((CategoryTheory.Idempotents.functorExtension C D).obj X).map f = (CategoryTheory.Idempotents.toKaroubiEquivalence D).inverse.map (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.IsIdempotentComplete D<GOAL>(CategoryTheory.Idempotents.karoubiUniversal C D).functor = CategoryTheory.Idempotents.functorExtension C D
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.IsIdempotentComplete D<VAR>F G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D<VAR>τ : (CategoryTheory.Idempotents.toKaroubi C).comp F ⟶ (CategoryTheory.Idempotents.toKaroubi C).comp G<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>(((CategoryTheory.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) D).obj (CategoryTheory.Idempotents.toKaroubi C)).preimage τ).app P = CategoryTheory.CategoryStruct.comp (F.map P.decompId_i) (CategoryTheory.CategoryStruct.comp (τ.app P.X) (G.map P.decompId_p))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>B : C<GOAL>((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).op.map (CategoryTheory.preadditiveYoneda.obj B)).Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>A : Cᵒᵖ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<VAR>x : Opposite.unop A ⟶ (CategoryTheory.shiftFunctor C n₀).obj T.obj₃<GOAL>((CategoryTheory.preadditiveCoyoneda.obj A).homologySequenceδ T n₀ n₁ h) x = CategoryTheory.CategoryStruct.comp x (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n₀).map T.mor₃) ((CategoryTheory.shiftFunctorAdd' C 1 n₀ n₁ ⋯).inv.app T.obj₁))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_5} C₅<VAR>CategoryTheory.Category.{u_12, u_6} C₆<VAR>T₁ : CategoryTheory.Functor C₁ C₂<VAR>T₂ : CategoryTheory.Functor C₂ C₃<VAR>V₁ : CategoryTheory.Functor C₁ C₄<VAR>V₂ : CategoryTheory.Functor C₂ C₅<VAR>V₃ : CategoryTheory.Functor C₃ C₆<VAR>B₁ : CategoryTheory.Functor C₄ C₅<VAR>B₂ : CategoryTheory.Functor C₅ C₆<VAR>CategoryTheory.CatCommSq T₁ V₁ V₂ B₁<VAR>CategoryTheory.CatCommSq T₂ V₂ V₃ B₂<VAR>X : C₁<GOAL>CategoryTheory.CatCommSq.iso'.inv.app X = CategoryTheory.CategoryStruct.comp (B₂.map ((CategoryTheory.CatCommSq.iso T₁ V₁ V₂ B₁).inv.app X)) ((CategoryTheory.CatCommSq.iso T₂ V₂ V₃ B₂).inv.app (T₁.obj X))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_5} C₅<VAR>CategoryTheory.Category.{u_12, u_6} C₆<VAR>T₁ : CategoryTheory.Functor C₁ C₂<VAR>T₂ : CategoryTheory.Functor C₂ C₃<VAR>V₁ : CategoryTheory.Functor C₁ C₄<VAR>V₂ : CategoryTheory.Functor C₂ C₅<VAR>V₃ : CategoryTheory.Functor C₃ C₆<VAR>B₁ : CategoryTheory.Functor C₄ C₅<VAR>B₂ : CategoryTheory.Functor C₅ C₆<VAR>CategoryTheory.CatCommSq T₁ V₁ V₂ B₁<VAR>CategoryTheory.CatCommSq T₂ V₂ V₃ B₂<VAR>X : C₁<GOAL>CategoryTheory.CatCommSq.iso'.hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T₂ V₂ V₃ B₂).hom.app (T₁.obj X)) (B₂.map ((CategoryTheory.CatCommSq.iso T₁ V₁ V₂ B₁).hom.app X))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_5} C₅<VAR>CategoryTheory.Category.{u_12, u_6} C₆<VAR>L₁ : CategoryTheory.Functor C₁ C₂<VAR>L₂ : CategoryTheory.Functor C₂ C₃<VAR>H₁ : CategoryTheory.Functor C₁ C₄<VAR>H₂ : CategoryTheory.Functor C₂ C₅<VAR>H₃ : CategoryTheory.Functor C₃ C₆<VAR>R₁ : CategoryTheory.Functor C₄ C₅<VAR>R₂ : CategoryTheory.Functor C₅ C₆<VAR>CategoryTheory.CatCommSq H₁ L₁ R₁ H₂<VAR>CategoryTheory.CatCommSq H₂ L₂ R₂ H₃<VAR>X : C₁<GOAL>CategoryTheory.CatCommSq.iso'.inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso H₂ L₂ R₂ H₃).inv.app (L₁.obj X)) (R₂.map ((CategoryTheory.CatCommSq.iso H₁ L₁ R₁ H₂).inv.app X))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>CategoryTheory.Category.{u_11, u_5} C₅<VAR>CategoryTheory.Category.{u_12, u_6} C₆<VAR>L₁ : CategoryTheory.Functor C₁ C₂<VAR>L₂ : CategoryTheory.Functor C₂ C₃<VAR>H₁ : CategoryTheory.Functor C₁ C₄<VAR>H₂ : CategoryTheory.Functor C₂ C₅<VAR>H₃ : CategoryTheory.Functor C₃ C₆<VAR>R₁ : CategoryTheory.Functor C₄ C₅<VAR>R₂ : CategoryTheory.Functor C₅ C₆<VAR>CategoryTheory.CatCommSq H₁ L₁ R₁ H₂<VAR>CategoryTheory.CatCommSq H₂ L₂ R₂ H₃<VAR>X : C₁<GOAL>CategoryTheory.CatCommSq.iso'.hom.app X = CategoryTheory.CategoryStruct.comp (R₂.map ((CategoryTheory.CatCommSq.iso H₁ L₁ R₁ H₂).hom.app X)) ((CategoryTheory.CatCommSq.iso H₂ L₂ R₂ H₃).hom.app (L₁.obj X))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>T : C₁ ≌ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : C₃ ≌ C₄<GOAL>∀ (x : CategoryTheory.CatCommSq T.functor L R B.functor) (X : C₂), CategoryTheory.CatCommSq.iso'.hom.app X = CategoryTheory.CategoryStruct.comp (B.unitIso.hom.app (L.obj (T.inverse.obj X))) (CategoryTheory.CategoryStruct.comp (B.inverse.map ((CategoryTheory.CatCommSq.iso T.functor L R B.functor).inv.app (T.inverse.obj X))) (B.inverse.map (R.map (T.counitIso.hom.app X))))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>T : C₁ ≌ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : C₃ ≌ C₄<GOAL>∀ (x : CategoryTheory.CatCommSq T.functor L R B.functor) (X : C₂), CategoryTheory.CatCommSq.iso'.inv.app X = CategoryTheory.CategoryStruct.comp (B.inverse.map (R.map (T.counitIso.inv.app X))) (CategoryTheory.CategoryStruct.comp (B.inverse.map ((CategoryTheory.CatCommSq.iso T.functor L R B.functor).hom.app (T.inverse.obj X))) (B.unitIso.inv.app (L.obj (T.inverse.obj X))))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_9, u_2} C₂<VAR>CategoryTheory.Category.{u_10, u_3} C₃<VAR>CategoryTheory.Category.{u_7, u_4} C₄<VAR>T : C₁ ≌ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : C₃ ≌ C₄<VAR>h : CategoryTheory.CatCommSq T.functor L R B.functor<GOAL>CategoryTheory.CatCommSq.hInv T.symm R L B.symm (CategoryTheory.CatCommSq.hInv T L R B h) = h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<GOAL>∀ (x : CategoryTheory.CatCommSq T L.functor R.functor B) (X : C₃), CategoryTheory.CatCommSq.iso'.hom.app X = CategoryTheory.CategoryStruct.comp (R.inverse.map (B.map (L.counitIso.inv.app X))) (CategoryTheory.CategoryStruct.comp (R.inverse.map ((CategoryTheory.CatCommSq.iso T L.functor R.functor B).inv.app (L.inverse.obj X))) (R.unitIso.inv.app (T.obj (L.inverse.obj X))))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>CategoryTheory.Category.{u_10, u_4} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<GOAL>∀ (x : CategoryTheory.CatCommSq T L.functor R.functor B) (X : C₃), CategoryTheory.CatCommSq.iso'.inv.app X = CategoryTheory.CategoryStruct.comp (R.unitIso.hom.app (T.obj (L.inverse.obj X))) (CategoryTheory.CategoryStruct.comp (R.inverse.map ((CategoryTheory.CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj X))) (R.inverse.map (B.map (L.counitIso.hom.app X))))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_9, u_2} C₂<VAR>CategoryTheory.Category.{u_10, u_3} C₃<VAR>CategoryTheory.Category.{u_7, u_4} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>h : CategoryTheory.CatCommSq T L.functor R.functor B<GOAL>CategoryTheory.CatCommSq.vInv B L.symm R.symm T (CategoryTheory.CatCommSq.vInv T L R B h) = h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsSeparating 𝒢.op ↔ CategoryTheory.IsCoseparating 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsCoseparating 𝒢.op ↔ CategoryTheory.IsSeparating 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set Cᵒᵖ<GOAL>CategoryTheory.IsCoseparating 𝒢.unop ↔ CategoryTheory.IsSeparating 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set Cᵒᵖ<GOAL>CategoryTheory.IsSeparating 𝒢.unop ↔ CategoryTheory.IsCoseparating 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsDetecting 𝒢.op ↔ CategoryTheory.IsCodetecting 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsCodetecting 𝒢.op ↔ CategoryTheory.IsDetecting 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set Cᵒᵖ<GOAL>CategoryTheory.IsDetecting 𝒢.unop ↔ CategoryTheory.IsCodetecting 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set Cᵒᵖ<GOAL>CategoryTheory.IsCodetecting 𝒢.unop ↔ CategoryTheory.IsDetecting 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsDetecting 𝒢<GOAL>CategoryTheory.IsSeparating 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsCodetecting 𝒢 → CategoryTheory.IsCoseparating 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Balanced C<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsSeparating 𝒢<GOAL>CategoryTheory.IsDetecting 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Balanced C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsCoseparating 𝒢 → CategoryTheory.IsCodetecting 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>CategoryTheory.Balanced C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsDetecting 𝒢 ↔ CategoryTheory.IsSeparating 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>CategoryTheory.Balanced C<VAR>𝒢 : Set C<GOAL>CategoryTheory.IsCodetecting 𝒢 ↔ CategoryTheory.IsCoseparating 𝒢
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsSeparating 𝒢<VAR>ℋ : Set C<VAR>h𝒢ℋ : 𝒢 ⊆ ℋ<GOAL>CategoryTheory.IsSeparating ℋ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsCoseparating 𝒢<VAR>ℋ : Set C<VAR>h𝒢ℋ : 𝒢 ⊆ ℋ<GOAL>CategoryTheory.IsCoseparating ℋ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsDetecting 𝒢<VAR>ℋ : Set C<VAR>h𝒢ℋ : 𝒢 ⊆ ℋ<GOAL>CategoryTheory.IsDetecting ℋ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsCodetecting 𝒢<VAR>ℋ : Set C<VAR>h𝒢ℋ : 𝒢 ⊆ ℋ<GOAL>CategoryTheory.IsCodetecting ℋ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>h : CategoryTheory.IsSeparating ∅<GOAL>Quiver.IsThin C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Quiver.IsThin C<GOAL>CategoryTheory.IsSeparating ∅
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>h : CategoryTheory.IsCoseparating ∅<GOAL>Quiver.IsThin C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>Quiver.IsThin C<GOAL>CategoryTheory.IsCoseparating ∅
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>h : CategoryTheory.IsDetecting ∅<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso f<GOAL>CategoryTheory.IsDetecting ∅
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>h : CategoryTheory.IsCodetecting ∅<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso f<GOAL>CategoryTheory.IsCodetecting ∅
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<VAR>∀ (A : C), CategoryTheory.Limits.HasCoproduct fun f => ↑f.fst<GOAL>CategoryTheory.IsSeparating 𝒢 ↔ ∀ (A : C), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc Sigma.snd)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<VAR>∀ (A : C), CategoryTheory.Limits.HasProduct fun f => ↑f.fst<GOAL>CategoryTheory.IsCoseparating 𝒢 ↔ ∀ (A : C), CategoryTheory.Mono (CategoryTheory.Limits.Pi.lift Sigma.snd)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.WellPowered C<VAR>CategoryTheory.Limits.HasLimits C<VAR>𝒢 : Set C<VAR>Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : CategoryTheory.IsCoseparating 𝒢<GOAL>CategoryTheory.Limits.HasInitial C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.WellPowered Cᵒᵖ<VAR>CategoryTheory.Limits.HasColimits C<VAR>𝒢 : Set C<VAR>Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : CategoryTheory.IsSeparating 𝒢<GOAL>CategoryTheory.Limits.HasTerminal C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsDetecting 𝒢<VAR>X : C<VAR>P Q : CategoryTheory.Subobject X<VAR>h₁ : P ≤ Q<VAR>h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f<GOAL>P = Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsDetecting 𝒢<VAR>X : C<VAR>P Q : CategoryTheory.Subobject X<VAR>h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f → Q.Factors f<GOAL>P ⊓ Q = P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsDetecting 𝒢<VAR>X : C<VAR>P Q : CategoryTheory.Subobject X<VAR>h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f<GOAL>P = Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>𝒢 : Set C<VAR>Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : CategoryTheory.IsDetecting 𝒢<GOAL>CategoryTheory.WellPowered C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsCoseparating 𝒢<GOAL>CategoryTheory.IsCoseparating ((CategoryTheory.StructuredArrow.proj S T).obj ⁻¹' 𝒢)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : CategoryTheory.Functor C D<VAR>T : D<VAR>𝒢 : Set C<VAR>h𝒢 : CategoryTheory.IsSeparating 𝒢<GOAL>CategoryTheory.IsSeparating ((CategoryTheory.CostructuredArrow.proj S T).obj ⁻¹' 𝒢)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsSeparator (Opposite.op G) ↔ CategoryTheory.IsCoseparator G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsCoseparator (Opposite.op G) ↔ CategoryTheory.IsSeparator G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : Cᵒᵖ<GOAL>CategoryTheory.IsCoseparator (Opposite.unop G) ↔ CategoryTheory.IsSeparator G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : Cᵒᵖ<GOAL>CategoryTheory.IsSeparator (Opposite.unop G) ↔ CategoryTheory.IsCoseparator G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsDetector (Opposite.op G) ↔ CategoryTheory.IsCodetector G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsCodetector (Opposite.op G) ↔ CategoryTheory.IsDetector G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : Cᵒᵖ<GOAL>CategoryTheory.IsCodetector (Opposite.unop G) ↔ CategoryTheory.IsDetector G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : Cᵒᵖ<GOAL>CategoryTheory.IsDetector (Opposite.unop G) ↔ CategoryTheory.IsCodetector G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>G : C<GOAL>CategoryTheory.IsDetector G → CategoryTheory.IsSeparator G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>G : C<GOAL>CategoryTheory.IsCodetector G → CategoryTheory.IsCoseparator G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Balanced C<VAR>G : C<GOAL>CategoryTheory.IsSeparator G → CategoryTheory.IsDetector G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Balanced C<VAR>G : C<GOAL>CategoryTheory.IsCoseparator G → CategoryTheory.IsCodetector G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) → f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsSeparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) → f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) → f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsCoseparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) → f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsDetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h', CategoryTheory.CategoryStruct.comp h' f = h) → CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsDetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h', CategoryTheory.CategoryStruct.comp h' f = h) → CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsCodetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h', CategoryTheory.CategoryStruct.comp f h' = h) → CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsCodetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h', CategoryTheory.CategoryStruct.comp f h' = h) → CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsSeparator G ↔ (CategoryTheory.coyoneda.obj (Opposite.op G)).Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsCoseparator G ↔ (CategoryTheory.yoneda.obj G).Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<VAR>∀ (A : C), CategoryTheory.Limits.HasCoproduct fun x => G<GOAL>CategoryTheory.IsSeparator G ↔ ∀ (A : C), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun f => f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<VAR>∀ (A : C), CategoryTheory.Limits.HasProduct fun x => G<GOAL>CategoryTheory.IsCoseparator G ↔ ∀ (A : C), CategoryTheory.Mono (CategoryTheory.Limits.Pi.lift fun f => f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>G H : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct G H<GOAL>CategoryTheory.IsSeparator (G ⨿ H) ↔ CategoryTheory.IsSeparating {G, H}