ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : CategoryTheory.StrongOplaxNatTrans F G<VAR>a : B<VAR>a' : C<VAR>f : G.obj a ⟶ a'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.id a)).hom f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.id a)) f).hom (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapId a) f))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (η.app a)) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv f) (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) f).hom))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H : CategoryTheory.OplaxFunctor B C<VAR>η : CategoryTheory.StrongOplaxNatTrans F G<VAR>θ : CategoryTheory.StrongOplaxNatTrans G H<GOAL>∀ {a b : B} (f : a ⟶ b), ((η.vcomp θ).naturality f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (θ.app b)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).inv (θ.app b)) (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (θ.app b)).hom)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H : CategoryTheory.OplaxFunctor B C<VAR>η : CategoryTheory.StrongOplaxNatTrans F G<VAR>θ : CategoryTheory.StrongOplaxNatTrans G H<VAR>a : B<GOAL>(η.vcomp θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H : CategoryTheory.OplaxFunctor B C<VAR>η : CategoryTheory.StrongOplaxNatTrans F G<VAR>θ : CategoryTheory.StrongOplaxNatTrans G H<GOAL>∀ {a b : B} (f : a ⟶ b), ((η.vcomp θ).naturality f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (θ.app b)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (θ.app b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (θ.app b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).hom) (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).inv)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<GOAL>∀ {X Y Z : CategoryTheory.Pseudofunctor B C} (η : CategoryTheory.StrongOplaxNatTrans X.toOplax Y.toOplax) (θ : CategoryTheory.StrongOplaxNatTrans Y.toOplax Z.toOplax), CategoryTheory.CategoryStruct.comp η θ = η.vcomp θ
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<GOAL>CategoryTheory.CategoryStruct.id F = CategoryTheory.StrongOplaxNatTrans.id F.toOplax
<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>self : CategoryTheory.LaxMonoidalFunctor C D<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor (self.obj X)).hom = CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) self.ε ≫ self.μ X (𝟙_ C) ≫ self.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom
<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>self : CategoryTheory.LaxMonoidalFunctor C D<VAR>X Y : C<VAR>X' : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X') (self.map f) ≫ self.μ X' Y = self.μ X' X ≫ self.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f)
<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>self : CategoryTheory.LaxMonoidalFunctor C D<VAR>X Y Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (self.μ X Y) (self.obj Z) ≫ self.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≫ self.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator (self.obj X) (self.obj Y) (self.obj Z)).hom ≫ CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) (self.μ Y Z) ≫ self.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)
<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>self : CategoryTheory.LaxMonoidalFunctor C D<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (self.obj X)).hom = CategoryTheory.MonoidalCategory.whiskerRight self.ε (self.obj X) ≫ self.μ (𝟙_ C) X ≫ self.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom
<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>self : CategoryTheory.LaxMonoidalFunctor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (self.map f) (self.obj X') ≫ self.μ Y X' = self.μ X X' ≫ self.map (CategoryTheory.MonoidalCategory.whiskerRight f 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 : CategoryTheory.LaxMonoidalFunctor C D<VAR>X Y X' Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g) ≫ F.μ Y Y' = F.μ X X' ≫ F.map (CategoryTheory.MonoidalCategory.tensorHom f 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 : C ⥤ D<VAR>ε : 𝟙_ D ⟶ F.obj (𝟙_ C)<VAR>μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)<VAR>μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (CategoryTheory.MonoidalCategory.tensorHom f g) := by aesop_cat<VAR>associativity : ∀ (X Y Z : C), CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (𝟙 (F.obj Z)) ≫ μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≫ F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ CategoryTheory.MonoidalCategory.tensorHom (𝟙 (F.obj X)) (μ Y Z) ≫ μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z) := by aesop_cat<VAR>left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom ε (𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom := by aesop_cat<VAR>right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom (𝟙 (F.obj X)) ε ≫ μ X (𝟙_ C) ≫ F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom := by aesop_cat<VAR>X Y : C<GOAL>(CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).μ X Y = μ 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 : C ⥤ D<VAR>ε : 𝟙_ D ⟶ F.obj (𝟙_ C)<VAR>μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)<VAR>μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (CategoryTheory.MonoidalCategory.tensorHom f g) := by aesop_cat<VAR>associativity : ∀ (X Y Z : C), CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (𝟙 (F.obj Z)) ≫ μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≫ F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ CategoryTheory.MonoidalCategory.tensorHom (𝟙 (F.obj X)) (μ Y Z) ≫ μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z) := by aesop_cat<VAR>left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom ε (𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom := by aesop_cat<VAR>right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom (𝟙 (F.obj X)) ε ≫ μ X (𝟙_ C) ≫ F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom := by aesop_cat<GOAL>∀ {X Y : C} (a : X ⟶ Y), (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).map a = F.map a
<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 : C ⥤ D<VAR>ε : 𝟙_ D ⟶ F.obj (𝟙_ C)<VAR>μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)<VAR>μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (CategoryTheory.MonoidalCategory.tensorHom f g) := by aesop_cat<VAR>associativity : ∀ (X Y Z : C), CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (𝟙 (F.obj Z)) ≫ μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≫ F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ CategoryTheory.MonoidalCategory.tensorHom (𝟙 (F.obj X)) (μ Y Z) ≫ μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z) := by aesop_cat<VAR>left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom ε (𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom := by aesop_cat<VAR>right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom (𝟙 (F.obj X)) ε ≫ μ X (𝟙_ C) ≫ F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom := by aesop_cat<GOAL>(CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).ε = ε
<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 : C ⥤ D<VAR>ε : 𝟙_ D ⟶ F.obj (𝟙_ C)<VAR>μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)<VAR>μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (CategoryTheory.MonoidalCategory.tensorHom f g) := by aesop_cat<VAR>associativity : ∀ (X Y Z : C), CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (𝟙 (F.obj Z)) ≫ μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≫ F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ CategoryTheory.MonoidalCategory.tensorHom (𝟙 (F.obj X)) (μ Y Z) ≫ μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z) := by aesop_cat<VAR>left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom ε (𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom := by aesop_cat<VAR>right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.MonoidalCategory.tensorHom (𝟙 (F.obj X)) ε ≫ μ X (𝟙_ C) ≫ F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom := by aesop_cat<GOAL>∀ (a : C), (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).obj a = F.obj a
<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.MonoidalCategory.leftUnitor (F.obj X)).inv ≫ CategoryTheory.MonoidalCategory.whiskerRight F.ε (F.obj X) ≫ F.μ (𝟙_ C) X = F.map (CategoryTheory.MonoidalCategory.leftUnitor X).inv
<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.MonoidalCategory.rightUnitor (F.obj X)).inv ≫ CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) F.ε ≫ F.μ X (𝟙_ C) = F.map (CategoryTheory.MonoidalCategory.rightUnitor X).inv
<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 Y Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (F.μ Y Z) ≫ F.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z) ≫ F.map (CategoryTheory.MonoidalCategory.associator X Y Z).inv = (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ CategoryTheory.MonoidalCategory.whiskerRight (F.μ X Y) (F.obj Z) ≫ F.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z
<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>self : CategoryTheory.OplaxMonoidalFunctor C D<VAR>X Y Z : C<GOAL>self.δ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≫ CategoryTheory.MonoidalCategory.whiskerRight (self.δ X Y) (self.obj Z) ≫ (CategoryTheory.MonoidalCategory.associator (self.obj X) (self.obj Y) (self.obj Z)).hom = self.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom ≫ self.δ X (CategoryTheory.MonoidalCategory.tensorObj Y Z) ≫ CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) (self.δ Y Z)
<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>self : CategoryTheory.OplaxMonoidalFunctor C D<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (self.obj X)).inv = self.map (CategoryTheory.MonoidalCategory.leftUnitor X).inv ≫ self.δ (𝟙_ C) X ≫ CategoryTheory.MonoidalCategory.whiskerRight self.η (self.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>self : CategoryTheory.OplaxMonoidalFunctor C D<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor (self.obj X)).inv = self.map (CategoryTheory.MonoidalCategory.rightUnitor X).inv ≫ self.δ X (𝟙_ C) ≫ CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) self.η
<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>self : CategoryTheory.OplaxMonoidalFunctor C D<VAR>X Y : C<VAR>X' : C<VAR>f : X ⟶ Y<GOAL>self.δ X' X ≫ CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X') (self.map f) = self.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f) ≫ self.δ 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>self : CategoryTheory.OplaxMonoidalFunctor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' : C<GOAL>self.δ X X' ≫ CategoryTheory.MonoidalCategory.whiskerRight (self.map f) (self.obj X') = self.map (CategoryTheory.MonoidalCategory.whiskerRight f X') ≫ self.δ Y 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 : CategoryTheory.OplaxMonoidalFunctor C D<VAR>X Y X' Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>F.δ X X' ≫ CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g) = F.map (CategoryTheory.MonoidalCategory.tensorHom f g) ≫ F.δ Y 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 : CategoryTheory.OplaxMonoidalFunctor C D<VAR>X : C<GOAL>F.δ (𝟙_ C) X ≫ CategoryTheory.MonoidalCategory.whiskerRight F.η (F.obj X) ≫ (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom
<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.OplaxMonoidalFunctor C D<VAR>X : C<GOAL>F.δ X (𝟙_ C) ≫ CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) F.η ≫ (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom
<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.OplaxMonoidalFunctor C D<VAR>X Y Z : C<GOAL>F.δ X (CategoryTheory.MonoidalCategory.tensorObj Y Z) ≫ CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (F.δ Y Z) ≫ (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).inv = F.map (CategoryTheory.MonoidalCategory.associator X Y Z).inv ≫ F.δ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≫ CategoryTheory.MonoidalCategory.whiskerRight (F.δ X Y) (F.obj Z)
<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>self : CategoryTheory.MonoidalFunctor C D<GOAL>CategoryTheory.IsIso self.ε
<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>self : CategoryTheory.MonoidalFunctor C D<VAR>X Y : C<GOAL>CategoryTheory.IsIso (self.μ 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 : CategoryTheory.MonoidalFunctor C D<VAR>X Y : C<GOAL>F.toOplaxMonoidalFunctor.δ X Y = CategoryTheory.inv (F.μ 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 : CategoryTheory.MonoidalFunctor C D<GOAL>F.toOplaxMonoidalFunctor.η = CategoryTheory.inv F.ε
<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.MonoidalFunctor C D<GOAL>F.toOplaxMonoidalFunctor.toFunctor = F.toFunctor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.LaxMonoidalFunctor.id C).μ X Y = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj ((𝟭 C).obj X) ((𝟭 C).obj Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.LaxMonoidalFunctor.id C).ε = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.LaxMonoidalFunctor.id C).toFunctor = 𝟭 C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.OplaxMonoidalFunctor.id C).η = 𝟙 ((𝟭 C).obj (𝟙_ C))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.OplaxMonoidalFunctor.id C).δ X Y = 𝟙 ((𝟭 C).obj (CategoryTheory.MonoidalCategory.tensorObj X Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.OplaxMonoidalFunctor.id C).toFunctor = 𝟭 C
<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.MonoidalFunctor C D<VAR>X Y X' Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>F.map (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.inv (F.μ X X') ≫ CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g) ≫ F.μ Y 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 : CategoryTheory.MonoidalFunctor C D<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<GOAL>F.map (CategoryTheory.MonoidalCategory.whiskerLeft X f) = CategoryTheory.inv (F.μ X Y) ≫ CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (F.map f) ≫ F.μ X Z
<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.MonoidalFunctor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>F.map (CategoryTheory.MonoidalCategory.whiskerRight f Z) = CategoryTheory.inv (F.μ X Z) ≫ CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj Z) ≫ F.μ Y Z
<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.MonoidalFunctor C D<VAR>X : C<GOAL>F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom = CategoryTheory.inv (F.μ (𝟙_ C) X) ≫ CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.inv F.ε) (F.obj X) ≫ (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom
<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.MonoidalFunctor C D<VAR>X : C<GOAL>F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom = CategoryTheory.inv (F.μ X (𝟙_ C)) ≫ CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (CategoryTheory.inv F.ε) ≫ (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom
<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.MonoidalFunctor C D<VAR>X Y : C<GOAL>(F.μIso X Y).hom = F.μ 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 : CategoryTheory.MonoidalFunctor C D<VAR>X Y : C<GOAL>(F.μIso X Y).inv ≫ F.μ X Y = 𝟙 (F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y))