ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>X : A<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₀ eA e').unitIso.hom.app X = eA.unitIso.hom.app X ≫ eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X))
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₀ eA e').functor = eA.functor ⋙ e'.functor
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₀ eA e').inverse = e'.inverse ⋙ eA.inverse
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF).functor = F
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_7, u_2} A'<VAR>CategoryTheory.Category.{u_6, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF).inverse = e'.inverse ⋙ eA.inverse
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : B'<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso hF).inv.app X = e'.counitIso.inv.app X ≫ e'.functor.map (eA.counitIso.inv.app (e'.inverse.obj X)) ≫ hF.hom.app (eA.inverse.obj (e'.inverse.obj X))
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : B'<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso hF).hom.app X = hF.inv.app (eA.inverse.obj (e'.inverse.obj X)) ≫ e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj X)) ≫ e'.counitIso.hom.app X
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} A<VAR>CategoryTheory.Category.{u_7, u_2} A'<VAR>CategoryTheory.Category.{u_5, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF).counitIso = AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso hF
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : A<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso hF).inv.app X = eA.inverse.map (e'.inverse.map (hF.inv.app X)) ≫ eA.inverse.map (e'.unitIso.inv.app (eA.functor.obj X)) ≫ eA.unitIso.inv.app X
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : A<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso hF).hom.app X = eA.unitIso.hom.app X ≫ eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫ eA.inverse.map (e'.inverse.map (hF.hom.app X))
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_7, u_2} A'<VAR>CategoryTheory.Category.{u_6, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF).unitIso = AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso hF
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₂ eB hF).functor = F ⋙ eB.inverse
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_7, u_2} A'<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₂ eB hF).inverse = eB.functor ⋙ e'.inverse ⋙ eA.inverse
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : B<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso eB hF).hom.app X = eB.inverse.map (hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj X)))) ≫ eB.inverse.map (e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj X)))) ≫ eB.inverse.map (e'.counitIso.hom.app (eB.functor.obj X)) ≫ eB.unitIso.inv.app X
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : B<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso eB hF).inv.app X = eB.unitIso.hom.app X ≫ eB.inverse.map (e'.counitIso.inv.app (eB.functor.obj X)) ≫ eB.inverse.map (e'.functor.map (eA.counitIso.inv.app (e'.inverse.obj (eB.functor.obj X)))) ≫ eB.inverse.map (hF.hom.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj X))))
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} A<VAR>CategoryTheory.Category.{u_7, u_2} A'<VAR>CategoryTheory.Category.{u_5, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₂ eB hF).counitIso = AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso eB hF
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : A<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso eB hF).hom.app X = eA.unitIso.hom.app X ≫ eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫ eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫ eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X)))
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : A<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso eB hF).inv.app X = eA.inverse.map (e'.inverse.map (eB.counitIso.hom.app (F.obj X))) ≫ eA.inverse.map (e'.inverse.map (hF.inv.app X)) ≫ eA.inverse.map (e'.unitIso.inv.app (eA.functor.obj X)) ≫ eA.unitIso.inv.app X
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_7, u_2} A'<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence₂ eB hF).unitIso = AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso eB hF
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence hF hG).inverse = G
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_7, u_2} A'<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence hF hG).functor = F ⋙ eB.inverse
<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_2} A'<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>X : B<GOAL>AlgebraicTopology.DoldKan.Compatibility.τ₀.hom.app X = e'.counitIso.hom.app (eB.functor.obj X)
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>X : B<GOAL>(AlgebraicTopology.DoldKan.Compatibility.τ₁ hF hG η).hom.app X = e'.functor.map (hG.hom.app X) ≫ hF.hom.app (G.obj X) ≫ η.hom.app X
<VAR>A : Type u_1<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eB : B ≌ B'<VAR>F : A ⥤ B'<VAR>G : B ⥤ A<VAR>η : G ⋙ F ≅ eB.functor<VAR>X : B<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso η).hom.app X = eB.inverse.map (η.hom.app X) ≫ eB.unitIso.inv.app X
<VAR>A : Type u_1<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eB : B ≌ B'<VAR>F : A ⥤ B'<VAR>G : B ⥤ A<VAR>η : G ⋙ F ≅ eB.functor<VAR>X : B<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso η).inv.app X = eB.unitIso.hom.app X ≫ eB.inverse.map (η.inv.app X)
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_8, u_1} A<VAR>CategoryTheory.Category.{u_7, u_2} A'<VAR>CategoryTheory.Category.{u_6, u_3} B<VAR>CategoryTheory.Category.{u_5, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>hη : AlgebraicTopology.DoldKan.Compatibility.τ₀ = AlgebraicTopology.DoldKan.Compatibility.τ₁ hF hG η<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence hF hG).counitIso = AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso η
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : A<GOAL>(AlgebraicTopology.DoldKan.Compatibility.υ hF).inv.app X = e'.inverse.map (hF.inv.app X) ≫ e'.unitIso.inv.app (eA.functor.obj X)
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>X : A<GOAL>(AlgebraicTopology.DoldKan.Compatibility.υ hF).hom.app X = e'.unitIso.hom.app (eA.functor.obj X) ≫ e'.inverse.map (hF.hom.app X)
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>ε : eA.functor ≅ F ⋙ e'.inverse<VAR>X : A<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso hG ε).inv.app X = eA.unitIso.hom.app (G.obj (eB.inverse.obj (F.obj X))) ≫ eA.inverse.map (hG.inv.app (eB.inverse.obj (F.obj X))) ≫ eA.inverse.map (e'.inverse.map (eB.counitIso.hom.app (F.obj X))) ≫ eA.inverse.map (ε.inv.app X) ≫ eA.unitIso.inv.app X
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} A<VAR>CategoryTheory.Category.{u_6, u_2} A'<VAR>CategoryTheory.Category.{u_7, u_3} B<VAR>CategoryTheory.Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>ε : eA.functor ≅ F ⋙ e'.inverse<VAR>X : A<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso hG ε).hom.app X = eA.unitIso.hom.app X ≫ eA.inverse.map (ε.hom.app X) ≫ eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X))) ≫ eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X))) ≫ eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} A<VAR>CategoryTheory.Category.{u_5, u_2} A'<VAR>CategoryTheory.Category.{u_8, u_3} B<VAR>CategoryTheory.Category.{u_7, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>ε : eA.functor ≅ F ⋙ e'.inverse<VAR>hε : AlgebraicTopology.DoldKan.Compatibility.υ hF = ε<GOAL>(AlgebraicTopology.DoldKan.Compatibility.equivalence hF hG).unitIso = AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso hG ε
<VAR>j : ℕ<VAR>i : Fin (j + 2)<GOAL>AlgebraicTopology.DoldKan.Isδ₀ (SimplexCategory.δ i) ↔ i = 0
<VAR>n : ℕ<VAR>i : [n] ⟶ [n + 1]<VAR>CategoryTheory.Mono i<VAR>hi : AlgebraicTopology.DoldKan.Isδ₀ i<GOAL>i = SimplexCategory.δ 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>Δ : SimplexCategory<GOAL>AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (𝟙 Δ) = 𝟙 (K.X Δ.len)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>Δ Δ' : SimplexCategory<VAR>i : Δ' ⟶ Δ<VAR>CategoryTheory.Mono i<VAR>hi : AlgebraicTopology.DoldKan.Isδ₀ i<GOAL>AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i = K.d Δ.len Δ'.len
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ 0) = K.d (n + 1) n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>Δ Δ' : SimplexCategory<VAR>i : Δ' ⟶ Δ<VAR>CategoryTheory.Mono i<VAR>h₁ : Δ ≠ Δ'<VAR>h₂ : ¬AlgebraicTopology.DoldKan.Isδ₀ i<GOAL>AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' : SimplexCategory<VAR>i : Δ ⟶ Δ'<VAR>CategoryTheory.Mono i<GOAL>AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i ≫ f.f Δ.len = f.f Δ'.len ≫ AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K' i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i' : Δ'' ⟶ Δ'<VAR>i : Δ' ⟶ Δ<VAR>CategoryTheory.Mono i'<VAR>CategoryTheory.Mono i<GOAL>AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i ≫ AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i' = AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (i' ≫ i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<VAR>θ : Δ ⟶ Δ'<VAR>Δ'' : SimplexCategory<VAR>e : Opposite.unop Δ' ⟶ Δ''<VAR>i : Δ'' ⟶ Opposite.unop A.fst<VAR>CategoryTheory.Epi e<VAR>CategoryTheory.Mono i<VAR>fac : e ≫ i = θ.unop ≫ A.e<GOAL>CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A ≫ AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ = AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i ≫ CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (SimplicialObject.Splitting.IndexSet.mk e)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<VAR>θ : Δ ⟶ Δ'<GOAL>CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A ≫ AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ = AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (θ.unop ≫ A.e)) ≫ CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (A.pull θ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(AlgebraicTopology.DoldKan.Γ₀.obj K).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>∀ {X Y : SimplexCategoryᵒᵖ} (θ : X ⟶ Y), (AlgebraicTopology.DoldKan.Γ₀.obj K).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<VAR>θ : Δ ⟶ Δ'<VAR>Δ'' : SimplexCategory<VAR>e : Opposite.unop Δ' ⟶ Δ''<VAR>i : Δ'' ⟶ Opposite.unop A.fst<VAR>CategoryTheory.Epi e<VAR>CategoryTheory.Mono i<VAR>fac : e ≫ i = θ.unop ≫ A.e<GOAL>((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A ≫ (AlgebraicTopology.DoldKan.Γ₀.obj K).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i ≫ ((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (SimplicialObject.Splitting.IndexSet.mk e)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<VAR>θ : Δ ⟶ Δ'<GOAL>((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A ≫ (AlgebraicTopology.DoldKan.Γ₀.obj K).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (θ.unop ≫ A.e)) ≫ ((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (A.pull θ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategory<VAR>i : Δ' ⟶ Δ<VAR>CategoryTheory.Mono i<GOAL>((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ)) ≫ (AlgebraicTopology.DoldKan.Γ₀.obj K).map i.op = AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i ≫ ((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ'))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : ChainComplex C ℕ<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategory<VAR>e : Δ' ⟶ Δ<VAR>CategoryTheory.Epi e<GOAL>((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ)) ≫ (AlgebraicTopology.DoldKan.Γ₀.obj K).map e.op = ((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj (SimplicialObject.Splitting.IndexSet.mk e)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(AlgebraicTopology.DoldKan.Γ₀.map f).app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting K).desc Δ fun A => f.f (Opposite.unop A.fst).len ≫ ((AlgebraicTopology.DoldKan.Γ₀.splitting K').cofan Δ).inj A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<GOAL>(AlgebraicTopology.DoldKan.Γ₀'.map f).F = AlgebraicTopology.DoldKan.Γ₀.map f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>AlgebraicTopology.DoldKan.Γ₀'.obj K = SimplicialObject.Split.mk' (AlgebraicTopology.DoldKan.Γ₀.splitting K)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>i : ℕ<GOAL>(AlgebraicTopology.DoldKan.Γ₀'.map f).f i = f.f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(AlgebraicTopology.DoldKan.Γ₀.obj X).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ X Δ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<GOAL>∀ {X_1 Y : SimplexCategoryᵒᵖ} (θ : X_1 ⟶ Y), (AlgebraicTopology.DoldKan.Γ₀.obj X).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map X θ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>∀ {X Y : ChainComplex C ℕ} (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ), (AlgebraicTopology.DoldKan.Γ₀.map f).app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting X).desc Δ fun A => f.f (Opposite.unop A.fst).len ≫ ((AlgebraicTopology.DoldKan.Γ₀.splitting Y).cofan Δ).inj A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(AlgebraicTopology.DoldKan.Γ₂.obj P).p.app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting P.X).desc Δ fun A => P.p.f (Opposite.unop A.fst).len ≫ ((AlgebraicTopology.DoldKan.Γ₀.splitting P.X).cofan Δ).inj A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(AlgebraicTopology.DoldKan.Γ₂.obj P).X.obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ P.X Δ