ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(β_ (X ⊗ Y) Z).hom = (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(β_ X (Y ⊗ Z)).hom = (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(β_ (X ⊗ Y) Z).inv = (α_ Z X Y).inv ≫ (β_ X Z).inv ▷ Y ≫ (α_ X Z Y).hom ≫ X ◁ (β_ Y Z).inv ≫ (α_ X Y Z).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(β_ X (Y ⊗ Z)).inv = (α_ Y Z X).hom ≫ Y ◁ (β_ X Z).inv ≫ (α_ Y X Z).inv ≫ (β_ X Y).inv ▷ Z ≫ (α_ X Y Z).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X X' Y Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>(f ⊗ g) ≫ (β_ Y Y').hom = (β_ X X').hom ≫ (g ⊗ f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<GOAL>X ◁ f ≫ (β_ Z X).inv = (β_ Y X).inv ≫ f ▷ X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>f ▷ Z ≫ (β_ Z Y).inv = (β_ Z X).inv ≫ Z ◁ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X X' Y Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>(f ⊗ g) ≫ (β_ Y' Y).inv = (β_ X' X).inv ≫ (g ⊗ f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom = X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X = 𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ X Y Z).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Y) Z ≪≫ α_ Y X Z ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso Y (β_ X Z) ≪≫ (α_ Y Z X).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ Y Z) X ≪≫ α_ Z Y X = CategoryTheory.MonoidalCategory.whiskerLeftIso X (β_ Y Z) ≪≫ (α_ X Z Y).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Z) Y ≪≫ α_ Z X Y ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso Z (β_ X Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>α_ X Y Z ≪≫ β_ X (Y ⊗ Z) ≪≫ α_ Y Z X = CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Y) Z ≪≫ α_ Y X Z ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso Y (β_ X Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ X Y Z).symm ≪≫ β_ (X ⊗ Y) Z ≪≫ (α_ Z X Y).symm = CategoryTheory.MonoidalCategory.whiskerLeftIso X (β_ Y Z) ≪≫ (α_ X Z Y).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Z) Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ Y Z X).inv ≫ (β_ X (Y ⊗ Z)).inv ≫ (α_ X Y Z).inv = Y ◁ (β_ X Z).inv ≫ (α_ Y X Z).inv ≫ (β_ X Y).inv ▷ Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ Z X Y).hom ≫ (β_ (X ⊗ Y) Z).inv ≫ (α_ X Y Z).hom = (β_ X Z).inv ▷ Y ≫ (α_ X Z Y).hom ≫ X ◁ (β_ Y Z).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C = (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (λ_ X).hom ▷ 𝟙_ C = (ρ_ X).hom ▷ 𝟙_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom = X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (ρ_ X).hom = 𝟙_ C ◁ (λ_ X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (λ_ X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(β_ (𝟙_ C) X).hom = (λ_ X).hom ≫ (ρ_ X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(β_ (𝟙_ C) X).inv = (ρ_ X).hom ≫ (λ_ X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(β_ X (𝟙_ C)).hom = (ρ_ X).hom ≫ (λ_ X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(β_ X (𝟙_ C)).inv = (λ_ X).hom ≫ (ρ_ X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : CategoryTheory.SymmetricCategory C<VAR>X Y : C<GOAL>(β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.SymmetricCategory C<VAR>X Y : C<GOAL>(β_ Y X).hom = (β_ X Y).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>self : CategoryTheory.LaxBraidedFunctor C D<VAR>X Y : C<GOAL>self.μ X Y ≫ self.map (β_ X Y).hom = (β_ (self.obj X) (self.obj Y)).hom ≫ self.μ Y X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(CategoryTheory.LaxBraidedFunctor.id C).obj X = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>(CategoryTheory.LaxBraidedFunctor.id C).μ X Y = 𝟙 (X ⊗ Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.LaxBraidedFunctor.id C).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CategoryTheory.LaxBraidedFunctor.id C).ε = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>CategoryTheory.BraidedCategory E<VAR>F : CategoryTheory.LaxBraidedFunctor C D<VAR>G : CategoryTheory.LaxBraidedFunctor D E<GOAL>(F.comp G).ε = G.ε ≫ G.map F.ε
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>CategoryTheory.BraidedCategory E<VAR>F : CategoryTheory.LaxBraidedFunctor C D<VAR>G : CategoryTheory.LaxBraidedFunctor D E<GOAL>∀ {X Y : C} (f : X ⟶ Y), (F.comp G).map f = G.map (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>CategoryTheory.BraidedCategory E<VAR>F : CategoryTheory.LaxBraidedFunctor C D<VAR>G : CategoryTheory.LaxBraidedFunctor D E<VAR>X : C<GOAL>(F.comp G).obj X = G.obj (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>CategoryTheory.BraidedCategory E<VAR>F : CategoryTheory.LaxBraidedFunctor C D<VAR>G : CategoryTheory.LaxBraidedFunctor D E<VAR>X Y : C<GOAL>(F.comp G).μ X Y = G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F G : CategoryTheory.LaxBraidedFunctor C D<VAR>α β : F ⟶ G<VAR>w : ∀ (X : C), α.app X = β.app X<GOAL>α = β
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F G H : CategoryTheory.LaxBraidedFunctor C D<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>(α ≫ β).toNatTrans = α.toNatTrans ≫ β.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F G : CategoryTheory.LaxBraidedFunctor C D<VAR>i : F.toLaxMonoidalFunctor ≅ G.toLaxMonoidalFunctor<GOAL>(CategoryTheory.LaxBraidedFunctor.mkIso i).hom = i.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F G : CategoryTheory.LaxBraidedFunctor C D<VAR>i : F.toLaxMonoidalFunctor ≅ G.toLaxMonoidalFunctor<GOAL>(CategoryTheory.LaxBraidedFunctor.mkIso i).inv = i.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>self : CategoryTheory.BraidedFunctor C D<VAR>X Y : C<GOAL>self.map (β_ X Y).hom = CategoryTheory.inv (self.μ X Y) ≫ (β_ (self.obj X) (self.obj Y)).hom ≫ self.μ Y X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : CategoryTheory.BraidedFunctor C D<GOAL>(CategoryTheory.BraidedFunctor.toLaxBraidedFunctor C D F).toLaxMonoidalFunctor = F.toLaxMonoidalFunctor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.BraidedFunctor.id C).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>(CategoryTheory.BraidedFunctor.id C).μ X Y = 𝟙 (X ⊗ Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C<GOAL>(CategoryTheory.BraidedFunctor.id C).obj X = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CategoryTheory.BraidedFunctor.id C).ε = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>CategoryTheory.BraidedCategory E<VAR>F : CategoryTheory.BraidedFunctor C D<VAR>G : CategoryTheory.BraidedFunctor D E<GOAL>(F.comp G).ε = G.ε ≫ G.map F.ε
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>CategoryTheory.BraidedCategory E<VAR>F : CategoryTheory.BraidedFunctor C D<VAR>G : CategoryTheory.BraidedFunctor D E<VAR>X Y : C<GOAL>(F.comp G).μ X Y = G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>CategoryTheory.BraidedCategory E<VAR>F : CategoryTheory.BraidedFunctor C D<VAR>G : CategoryTheory.BraidedFunctor D E<GOAL>∀ {X Y : C} (f : X ⟶ Y), (F.comp G).map f = G.map (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>CategoryTheory.BraidedCategory E<VAR>F : CategoryTheory.BraidedFunctor C D<VAR>G : CategoryTheory.BraidedFunctor D E<VAR>X : C<GOAL>(F.comp G).obj X = G.obj (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F G : CategoryTheory.BraidedFunctor C D<VAR>α β : F ⟶ G<VAR>w : ∀ (X : C), α.app X = β.app X<GOAL>α = β
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F G H : CategoryTheory.BraidedFunctor C D<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>(α ≫ β).toNatTrans = α.toNatTrans ≫ β.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F G : CategoryTheory.BraidedFunctor C D<VAR>i : F.toMonoidalFunctor ≅ G.toMonoidalFunctor<GOAL>(CategoryTheory.BraidedFunctor.mkIso i).inv = i.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F G : CategoryTheory.BraidedFunctor C D<VAR>i : F.toMonoidalFunctor ≅ G.toMonoidalFunctor<GOAL>(CategoryTheory.BraidedFunctor.mkIso i).hom = i.hom
<VAR>M : Type u<VAR>CommMonoid M<VAR>N : Type u<VAR>CommMonoid N<VAR>F : M →* N<VAR>X Y : CategoryTheory.Discrete M<GOAL>(CategoryTheory.Discrete.braidedFunctor F).μ X Y = CategoryTheory.Discrete.eqToHom ⋯
<VAR>M : Type u<VAR>CommMonoid M<VAR>N : Type u<VAR>CommMonoid N<VAR>F : M →* N<VAR>X : CategoryTheory.Discrete M<GOAL>((CategoryTheory.Discrete.braidedFunctor F).obj X).as = F X.as
<VAR>M : Type u<VAR>CommMonoid M<VAR>N : Type u<VAR>CommMonoid N<VAR>F : M →* N<GOAL>(CategoryTheory.Discrete.braidedFunctor F).ε = CategoryTheory.Discrete.eqToHom ⋯
<VAR>M : Type u<VAR>CommMonoid M<VAR>N : Type u<VAR>CommMonoid N<VAR>F : M →* N<GOAL>∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y), (CategoryTheory.Discrete.braidedFunctor F).map f = CategoryTheory.Discrete.eqToHom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : U₁ ⟶ V₁<VAR>g₂ : U₂ ⟶ V₂<GOAL>((f₁ ⊗ f₂) ⊗ g₁ ⊗ g₂) ≫ CategoryTheory.tensor_μ C (Y₁, Y₂) (V₁, V₂) = CategoryTheory.tensor_μ C (X₁, X₂) (U₁, U₂) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>Z₁ Z₂ : C<GOAL>(f₁ ⊗ f₂) ▷ (Z₁ ⊗ Z₂) ≫ CategoryTheory.tensor_μ C (Y₁, Y₂) (Z₁, Z₂) = CategoryTheory.tensor_μ C (X₁, X₂) (Z₁, Z₂) ≫ (f₁ ▷ Z₁ ⊗ f₂ ▷ Z₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>Z₁ Z₂ : C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<GOAL>(Z₁ ⊗ Z₂) ◁ (f₁ ⊗ f₂) ≫ CategoryTheory.tensor_μ C (Z₁, Z₂) (Y₁, Y₂) = CategoryTheory.tensor_μ C (Z₁, Z₂) (X₁, X₂) ≫ (Z₁ ◁ f₁ ⊗ Z₂ ◁ f₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X₁ X₂ : C<GOAL>(λ_ (X₁ ⊗ X₂)).hom = (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ CategoryTheory.tensor_μ C (𝟙_ C, 𝟙_ C) (X₁, X₂) ≫ ((λ_ X₁).hom ⊗ (λ_ X₂).hom)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X₁ X₂ : C<GOAL>(ρ_ (X₁ ⊗ X₂)).hom = (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv ≫ CategoryTheory.tensor_μ C (X₁, X₂) (𝟙_ C, 𝟙_ C) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C<GOAL>CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂) ▷ (Z₁ ⊗ Z₂) ≫ CategoryTheory.tensor_μ C (X₁ ⊗ Y₁, X₂ ⊗ Y₂) (Z₁, Z₂) ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) = (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ (X₁ ⊗ X₂) ◁ CategoryTheory.tensor_μ C (Y₁, Y₂) (Z₁, Z₂) ≫ CategoryTheory.tensor_μ C (X₁, X₂) (Y₁ ⊗ Z₁, Y₂ ⊗ Z₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C × C<GOAL>(CategoryTheory.tensorMonoidal C).μ X Y = CategoryTheory.tensor_μ C X Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C × C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.tensorMonoidal C).map f = f.1 ⊗ f.2
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : C × C<GOAL>(CategoryTheory.tensorMonoidal C).obj X = X.1 ⊗ X.2
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CategoryTheory.tensorMonoidal C).ε = (λ_ (𝟙_ C)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X₁ X₂ : C<GOAL>(λ_ X₁).hom ⊗ (λ_ X₂).hom = CategoryTheory.tensor_μ C (𝟙_ C, X₁) (𝟙_ C, X₂) ≫ (λ_ (𝟙_ C)).hom ▷ (X₁ ⊗ X₂) ≫ (λ_ (X₁ ⊗ X₂)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X₁ X₂ : C<GOAL>(ρ_ X₁).hom ⊗ (ρ_ X₂).hom = CategoryTheory.tensor_μ C (X₁, 𝟙_ C) (X₂, 𝟙_ C) ≫ (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : C<GOAL>CategoryTheory.tensor_μ C (X₁ ⊗ X₂, X₃) (Y₁ ⊗ Y₂, Y₃) ≫ CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂) ▷ (X₃ ⊗ Y₃) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom = ((α_ X₁ X₂ X₃).hom ⊗ (α_ Y₁ Y₂ Y₃).hom) ≫ CategoryTheory.tensor_μ C (X₁, X₂ ⊗ X₃) (Y₁, Y₂ ⊗ Y₃) ≫ (X₁ ⊗ Y₁) ◁ CategoryTheory.tensor_μ C (X₂, X₃) (Y₂, Y₃)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>(β_ X Y).op = β_ (Opposite.op Y) (Opposite.op X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Cᵒᵖ<GOAL>(β_ X Y).unop = β_ (Opposite.unop Y) (Opposite.unop X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>(β_ X Y).hom.op = (β_ (Opposite.op Y) (Opposite.op X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Cᵒᵖ<GOAL>(β_ X Y).hom.unop = (β_ (Opposite.unop Y) (Opposite.unop X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>(β_ X Y).inv.op = (β_ (Opposite.op Y) (Opposite.op X)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Cᵒᵖ<GOAL>(β_ X Y).inv.unop = (β_ (Opposite.unop Y) (Opposite.unop X)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>(β_ X Y).mop = β_ { unmop := Y } { unmop := X }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Cᴹᵒᵖ<GOAL>(β_ X Y).unmop = β_ Y.unmop X.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : C<GOAL>(β_ X Y).hom.mop = (β_ { unmop := Y } { unmop := X }).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Cᴹᵒᵖ<GOAL>(β_ X Y).hom.unmop = (β_ Y.unmop X.unmop).hom