ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<GOAL>CategoryTheory.map (fun F => CategoryTheory.Limits.limit F) α = CategoryTheory.Limits.lim.map α
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<GOAL>CategoryTheory.LaxMonoidal.ε = CategoryTheory.Limits.limit.lift ((CategoryTheory.Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun j => 𝟙 (((CategoryTheory.Functor.const J).obj (𝟙_ C)).obj j), naturality := ⋯ } }
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F G : J ⥤ C<GOAL>CategoryTheory.LaxMonoidal.μ F G = CategoryTheory.Limits.limit.lift (F ⊗ G) { pt := CategoryTheory.Limits.limit F ⊗ CategoryTheory.Limits.limit G, π := { app := fun j => CategoryTheory.Limits.limit.π F j ⊗ CategoryTheory.Limits.limit.π G j, naturality := ⋯ } }
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F : J ⥤ C<GOAL>CategoryTheory.Limits.limLax.obj F = CategoryTheory.Limits.limit F
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F : J ⥤ C<GOAL>CategoryTheory.Limits.limLax.obj F = CategoryTheory.Limits.lim.obj F
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<GOAL>CategoryTheory.Limits.limLax.map α = CategoryTheory.Limits.lim.map α
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<GOAL>CategoryTheory.Limits.limLax.ε = CategoryTheory.Limits.limit.lift ((CategoryTheory.Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun j => 𝟙 (((CategoryTheory.Functor.const J).obj (𝟙_ C)).obj j), naturality := ⋯ } }
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F G : J ⥤ C<GOAL>CategoryTheory.Limits.limLax.μ F G = CategoryTheory.Limits.limit.lift (F ⊗ G) { pt := CategoryTheory.Limits.limit F ⊗ CategoryTheory.Limits.limit G, π := { app := fun j => CategoryTheory.Limits.limit.π F j ⊗ CategoryTheory.Limits.limit.π G j, naturality := ⋯ } }
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D D)<VAR>X : C<VAR>e : F.obj X ≅ CategoryTheory.Functor.id D<VAR>Y : CategoryTheory.GradedObject J D<VAR>a : I × J<VAR>ha : a.1 = 0<GOAL>(CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).hom = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).hom).app (Y a.2)) (e.hom.app (Y a.2))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D D)<VAR>X : C<VAR>e : F.obj X ≅ CategoryTheory.Functor.id D<VAR>Y : CategoryTheory.GradedObject J D<VAR>a : I × J<VAR>ha : a.1 = 0<GOAL>(CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).inv = CategoryTheory.CategoryStruct.comp (e.inv.app (Y a.2)) ((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).inv).app (Y a.2))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D D)<VAR>X : C<VAR>e : F.obj X ≅ CategoryTheory.Functor.id D<VAR>(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y : CategoryTheory.GradedObject J D<VAR>j : J<GOAL>CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (e.hom.app (Y j))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D D)<VAR>X : C<VAR>e : F.obj X ≅ CategoryTheory.Functor.id D<VAR>(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y : CategoryTheory.GradedObject J D<GOAL>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D D)<VAR>X : C<VAR>e : F.obj X ≅ CategoryTheory.Functor.id D<VAR>(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y : CategoryTheory.GradedObject J D<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯) ((CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom j) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j)) (e.hom.app (Y j))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D D)<VAR>X : C<VAR>e : F.obj X ≅ CategoryTheory.Functor.id D<VAR>(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y : CategoryTheory.GradedObject J D<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p<VAR>j : J<GOAL>(CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv j = CategoryTheory.CategoryStruct.comp (e.inv.app (Y j)) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).inv).app (Y j)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D D)<VAR>X : C<VAR>e : F.obj X ≅ CategoryTheory.Functor.id D<VAR>(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y Y' : CategoryTheory.GradedObject J D<VAR>φ : Y ⟶ Y'<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap p<GOAL>CategoryTheory.CategoryStruct.comp φ (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D D)<VAR>X : C<VAR>e : F.obj X ≅ CategoryTheory.Functor.id D<VAR>(Y : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y Y' : CategoryTheory.GradedObject J D<VAR>φ : Y ⟶ Y'<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y).HasMap p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y').HasMap p<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ) (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom φ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor D (CategoryTheory.Functor C D)<VAR>Y : C<VAR>e : F.flip.obj Y ≅ CategoryTheory.Functor.id D<VAR>X : CategoryTheory.GradedObject J D<VAR>a : J × I<VAR>ha : a.2 = 0<GOAL>(CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha).hom = CategoryTheory.CategoryStruct.comp ((F.obj (X a.1)).map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 Y a.2 ha).hom) (e.hom.app (X a.1))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor D (CategoryTheory.Functor C D)<VAR>Y : C<VAR>e : F.flip.obj Y ≅ CategoryTheory.Functor.id D<VAR>X : CategoryTheory.GradedObject J D<VAR>a : J × I<VAR>ha : a.2 = 0<GOAL>(CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha).inv = CategoryTheory.CategoryStruct.comp (e.inv.app (X a.1)) ((F.obj (X a.1)).map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 Y a.2 ha).inv)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor D (CategoryTheory.Functor C D)<VAR>Y : C<VAR>e : F.flip.obj Y ≅ CategoryTheory.Functor.id D<VAR>(X : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X : CategoryTheory.GradedObject J D<VAR>j : J<GOAL>CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩ = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom) (e.hom.app (X j))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor D (CategoryTheory.Functor C D)<VAR>Y : C<VAR>e : F.flip.obj Y ≅ CategoryTheory.Functor.id D<VAR>(X : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X : CategoryTheory.GradedObject J D<GOAL>(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor D (CategoryTheory.Functor C D)<VAR>Y : C<VAR>e : F.flip.obj Y ≅ CategoryTheory.Functor.id D<VAR>(X : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X : CategoryTheory.GradedObject J D<VAR>(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯) ((CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom j) = CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom) (e.hom.app (X j))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor D (CategoryTheory.Functor C D)<VAR>Y : C<VAR>e : F.flip.obj Y ≅ CategoryTheory.Functor.id D<VAR>(X : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X : CategoryTheory.GradedObject J D<VAR>(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p<VAR>j : J<GOAL>(CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv j = CategoryTheory.CategoryStruct.comp (e.inv.app (X j)) (CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).inv) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor D (CategoryTheory.Functor C D)<VAR>Y : C<VAR>e : F.flip.obj Y ≅ CategoryTheory.Functor.id D<VAR>(X : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X X' : CategoryTheory.GradedObject J D<VAR>φ : X ⟶ X'<VAR>(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p<GOAL>CategoryTheory.CategoryStruct.comp φ (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>Zero I<VAR>DecidableEq I<VAR>CategoryTheory.Limits.HasInitial C<VAR>F : CategoryTheory.Functor D (CategoryTheory.Functor C D)<VAR>Y : C<VAR>e : F.flip.obj Y ≅ CategoryTheory.Functor.id D<VAR>(X : D) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X X' : CategoryTheory.GradedObject J D<VAR>φ : X ⟶ X'<VAR>(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap p<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y))) (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom φ
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₃ : Type u_3<VAR>J : Type u_4<VAR>Zero I₂<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>self : CategoryTheory.GradedObject.TriangleIndexData r π<VAR>i₁ : I₁<GOAL>self.p₁₂ (i₁, 0) = i₁
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₃ : Type u_3<VAR>J : Type u_4<VAR>Zero I₂<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>self : CategoryTheory.GradedObject.TriangleIndexData r π<VAR>i : I₁ × I₂ × I₃<GOAL>π (i.1, self.p₂₃ i.2) = r i
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₃ : Type u_3<VAR>J : Type u_4<VAR>Zero I₂<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>self : CategoryTheory.GradedObject.TriangleIndexData r π<VAR>i₃ : I₃<GOAL>self.p₂₃ (0, i₃) = i₃
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₃ : Type u_3<VAR>J : Type u_4<VAR>Zero I₂<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>self : CategoryTheory.GradedObject.TriangleIndexData r π<VAR>i : I₁ × I₂ × I₃<GOAL>π (self.p₁₂ (i.1, i.2.1), i.2.2) = r i
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₃ : Type u_3<VAR>J : Type u_4<VAR>Zero I₂<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : CategoryTheory.GradedObject.TriangleIndexData r π<VAR>i₁ : I₁<VAR>i₃ : I₃<GOAL>r (i₁, 0, i₃) = π (i₁, i₃)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>CategoryTheory.Category.{u_10, u_1} C₁<VAR>CategoryTheory.Category.{u_12, u_2} C₂<VAR>CategoryTheory.Category.{u_11, u_3} C₃<VAR>CategoryTheory.Category.{u_9, u_4} D<VAR>Zero I₂<VAR>DecidableEq I₂<VAR>CategoryTheory.Limits.HasInitial C₂<VAR>F₁ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁)<VAR>F₂ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₃)<VAR>G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₃ D)<VAR>associator : CategoryTheory.bifunctorComp₁₂ F₁ G ≅ CategoryTheory.bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ CategoryTheory.Functor.id C₁<VAR>e₂ : F₂.obj X₂ ≅ CategoryTheory.Functor.id C₃<VAR>(X₁ : C₁) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₁.obj X₁)<VAR>(X₃ : C₃) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : CategoryTheory.GradedObject.TriangleIndexData r π<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor F₁ I₁ I₂).obj X₁).obj ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>(((CategoryTheory.GradedObject.mapBifunctor F₂ I₂ I₃).obj ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₂ τ.p₂₃ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃)).HasMap π<VAR>CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃<VAR>CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), CategoryTheory.CategoryStruct.comp (((associator.hom.app X₁).app X₂).app X₃) ((G.obj X₁).map (e₂.hom.app X₃)) = (G.map (e₁.hom.app X₁)).app X₃<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃).hom (CategoryTheory.GradedObject.mapBifunctorMapMap G π (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom) = CategoryTheory.GradedObject.mapBifunctorMapMap G π (CategoryTheory.GradedObject.mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom (CategoryTheory.CategoryStruct.id X₃)
<VAR>W X Y Z : Type u<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>p : W ⊗ Y<GOAL>(f ⊗ g) p = (f p.1, g p.2)
<VAR>X : Type u<VAR>Y Z : Type u<VAR>f : Y ⟶ Z<VAR>p : X ⊗ Y<GOAL>(X ◁ f) p = (p.1, f p.2)
<VAR>Y Z : Type u<VAR>f : Y ⟶ Z<VAR>X : Type u<VAR>p : Y ⊗ X<GOAL>(f ▷ X) p = (f p.1, p.2)
<VAR>X : Type u<VAR>x : X<VAR>p : PUnit.{u + 1}<GOAL>(λ_ X).hom (p, x) = x
<VAR>X : Type u<VAR>x : X<GOAL>(λ_ X).inv x = (PUnit.unit, x)
<VAR>X : Type u<VAR>x : X<VAR>p : PUnit.{u + 1}<GOAL>(ρ_ X).hom (x, p) = x
<VAR>X : Type u<VAR>x : X<GOAL>(ρ_ X).inv x = (x, PUnit.unit)
<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<VAR>z : Z<GOAL>(α_ X Y Z).hom ((x, y), z) = (x, y, z)
<VAR>X Y Z : Type u<VAR>x : X<VAR>y : Y<VAR>z : Z<GOAL>(α_ X Y Z).inv (x, y, z) = ((x, y), z)
<VAR>X Y Z : Type u<VAR>x : (X ⊗ Y) ⊗ Z<GOAL>((α_ X Y Z).hom x).1 = x.1.1
<VAR>X Y Z : Type u<VAR>x : (X ⊗ Y) ⊗ Z<GOAL>((α_ X Y Z).hom x).2.1 = x.1.2
<VAR>X Y Z : Type u<VAR>x : (X ⊗ Y) ⊗ Z<GOAL>((α_ X Y Z).hom x).2.2 = x.2
<VAR>X Y Z : Type u<VAR>x : X ⊗ Y ⊗ Z<GOAL>((α_ X Y Z).inv x).1.1 = x.1
<VAR>X Y Z : Type u<VAR>x : X ⊗ Y ⊗ Z<GOAL>((α_ X Y Z).inv x).1.2 = x.2.1
<VAR>X Y Z : Type u<VAR>x : X ⊗ Y ⊗ Z<GOAL>((α_ X Y Z).inv x).2 = x.2.2
<VAR>X Y : Type u<VAR>x : X<VAR>y : Y<GOAL>(β_ X Y).hom (x, y) = (y, x)
<VAR>X Y : Type u<VAR>x : X<VAR>y : Y<GOAL>(β_ X Y).inv (y, x) = (x, y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : CategoryTheory.LaxMonoidalFunctor C D<VAR>self : CategoryTheory.MonoidalNatTrans F G<VAR>X Y : C<GOAL>F.μ X Y ≫ self.app (CategoryTheory.MonoidalCategory.tensorObj X Y) = CategoryTheory.MonoidalCategory.tensorHom (self.app X) (self.app Y) ≫ G.μ X Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : CategoryTheory.LaxMonoidalFunctor C D<VAR>self : CategoryTheory.MonoidalNatTrans F G<GOAL>F.ε ≫ self.app (𝟙_ C) = G.ε
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : CategoryTheory.LaxMonoidalFunctor C D<VAR>X : C<GOAL>(CategoryTheory.MonoidalNatTrans.id F).app X = 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G H : CategoryTheory.LaxMonoidalFunctor C D<VAR>α : CategoryTheory.MonoidalNatTrans F G<VAR>β : CategoryTheory.MonoidalNatTrans G H<VAR>X : C<GOAL>(α.vcomp β).app X = α.app X ≫ β.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G H : CategoryTheory.LaxMonoidalFunctor C D<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>(α ≫ β).toNatTrans = α.toNatTrans ≫ β.toNatTrans