Multifunctor

📁 Source: Mathlib/CategoryTheory/Monoidal/Braided/Multifunctor.lean

Statistics

Metric	Count
Definitions functor₁₂₃, functor₁₂₃', functor₁₃₂, functor₁₃₂', functor₂₁₃, functor₂₁₃', functor₂₃₁, functor₂₃₁', functor₃₁₂, functor₃₁₂', ofBifunctor, firstMap₂, firstMap₃, secondMap₁, secondMap₂, secondMap₃, firstMap₂, firstMap₃, secondMap₁, secondMap₂, secondMap₃, ofCurried	22
Theorems functor₁₂₃'_map_app_app, functor₁₂₃'_obj_map_app, functor₁₂₃'_obj_obj_map, functor₁₂₃'_obj_obj_obj, functor₁₂₃_map_app_app, functor₁₂₃_obj_map_app, functor₁₂₃_obj_obj_map, functor₁₂₃_obj_obj_obj, functor₁₃₂'_map_app_app, functor₁₃₂'_obj_map_app, functor₁₃₂'_obj_obj_map, functor₁₃₂'_obj_obj_obj, functor₁₃₂_map_app_app, functor₁₃₂_obj_map_app, functor₁₃₂_obj_obj_map, functor₁₃₂_obj_obj_obj, functor₂₁₃'_map_app_app, functor₂₁₃'_obj_map_app, functor₂₁₃'_obj_obj_map, functor₂₁₃'_obj_obj_obj, functor₂₁₃_map_app_app, functor₂₁₃_obj_map_app, functor₂₁₃_obj_obj_map, functor₂₁₃_obj_obj_obj, functor₂₃₁'_map_app_app, functor₂₃₁'_obj_map_app, functor₂₃₁'_obj_obj_map, functor₂₃₁'_obj_obj_obj, functor₂₃₁_map_app_app, functor₂₃₁_obj_map_app, functor₂₃₁_obj_obj_map, functor₂₃₁_obj_obj_obj, functor₃₁₂'_map_app_app, functor₃₁₂'_obj_map_app, functor₃₁₂'_obj_obj_map, functor₃₁₂'_obj_obj_obj, functor₃₁₂_map_app_app, functor₃₁₂_obj_map_app, functor₃₁₂_obj_obj_map, functor₃₁₂_obj_obj_obj, firstMap₂_app_app_app, firstMap₃_app_app_app, secondMap₁_app_app_app, secondMap₂_app_app_app, secondMap₃_app_app_app, firstMap₂_app_app_app, firstMap₃_app_app_app, secondMap₁_app_app_app, secondMap₂_app_app_app, secondMap₃_app_app_app	50
Total	72

CategoryTheory.BraidedCategory

Definitions

Name	Category	Theorems
ofBifunctor 📖	CompOp	—

CategoryTheory.BraidedCategory.Hexagon

Definitions

Name	Category	Theorems
functor₁₂₃ 📖	CompOp	6 math math: functor₁₂₃_obj_obj_obj, functor₁₂₃_map_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁_app_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂_app_app_app, functor₁₂₃_obj_obj_map, functor₁₂₃_obj_map_app
functor₁₂₃' 📖	CompOp	6 math math: CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁_app_app_app, functor₁₂₃'_obj_map_app, functor₁₂₃'_obj_obj_obj, functor₁₂₃'_obj_obj_map, CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂_app_app_app, functor₁₂₃'_map_app_app
functor₁₃₂ 📖	CompOp	6 math math: functor₁₃₂_map_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₂_app_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃_app_app_app, functor₁₃₂_obj_obj_obj, functor₁₃₂_obj_map_app, functor₁₃₂_obj_obj_map
functor₁₃₂' 📖	CompOp	6 math math: CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁_app_app_app, functor₁₃₂'_obj_map_app, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₂_app_app_app, functor₁₃₂'_map_app_app, functor₁₃₂'_obj_obj_map, functor₁₃₂'_obj_obj_obj
functor₂₁₃ 📖	CompOp	6 math math: CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₂_app_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁_app_app_app, functor₂₁₃_map_app_app, functor₂₁₃_obj_map_app, functor₂₁₃_obj_obj_obj, functor₂₁₃_obj_obj_map
functor₂₁₃' 📖	CompOp	6 math math: CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃_app_app_app, functor₂₁₃'_map_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₂_app_app_app, functor₂₁₃'_obj_map_app, functor₂₁₃'_obj_obj_obj, functor₂₁₃'_obj_obj_map
functor₂₃₁ 📖	CompOp	6 math math: functor₂₃₁_map_app_app, functor₂₃₁_obj_obj_map, CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂_app_app_app, functor₂₃₁_obj_map_app, functor₂₃₁_obj_obj_obj, CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₃_app_app_app
functor₂₃₁' 📖	CompOp	6 math math: CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃_app_app_app, functor₂₃₁'_map_app_app, functor₂₃₁'_obj_obj_obj, functor₂₃₁'_obj_map_app, CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₃_app_app_app, functor₂₃₁'_obj_obj_map
functor₃₁₂ 📖	CompOp	6 math math: functor₃₁₂_map_app_app, functor₃₁₂_obj_obj_map, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃_app_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃_app_app_app, functor₃₁₂_obj_map_app, functor₃₁₂_obj_obj_obj
functor₃₁₂' 📖	CompOp	6 math math: functor₃₁₂'_map_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂_app_app_app, functor₃₁₂'_obj_obj_obj, functor₃₁₂'_obj_obj_map, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃_app_app_app, functor₃₁₂'_obj_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor₁₂₃'_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₂₃Obj CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₁₂₃' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom	—	CategoryTheory.MonoidalCategory.whiskerRight_tensor
functor₁₂₃'_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₁₂₃' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
functor₁₂₃'_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₁₂₃' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₁₂₃'_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₁₂₃' CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor₁₂₃_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₁₂Obj CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₁₂₃ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₁₂₃_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₁₂₃ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.whisker_assoc
functor₁₂₃_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₁₂₃ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.tensor_whiskerLeft
functor₁₂₃_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₁₂₃ CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor₁₃₂'_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₂₃Obj CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.Functor.map functor₁₃₂' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom	—	CategoryTheory.MonoidalCategory.whiskerRight_tensor
functor₁₃₂'_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.Functor.map functor₁₃₂' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₁₃₂'_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₁₃₂' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
functor₁₃₂'_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₁₃₂' CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor₁₃₂_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.bifunctorComp₁₂ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.flipFunctor CategoryTheory.Functor.map functor₁₃₂ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₁₃₂_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₁₂ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₁₃₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.tensor_whiskerLeft
functor₁₃₂_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₁₃₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.whisker_assoc
functor₁₃₂_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₁₃₂ CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor₂₁₃'_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₂₃ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₂₁₃' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
functor₂₁₃'_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₂₃ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₂₁₃' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom	—	CategoryTheory.MonoidalCategory.whiskerRight_tensor
functor₂₁₃'_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₂₁₃' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₂₁₃'_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₂₁₃' CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor₂₁₃_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₁₂Obj CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₂₁₃ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.whisker_assoc
functor₂₁₃_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.Functor.map functor₂₁₃ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₂₁₃_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₂₁₃ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.tensor_whiskerLeft
functor₂₁₃_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₂₁₃ CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor₂₃₁'_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.bifunctorComp₂₃ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₂₃₁' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₂₃₁'_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.bifunctorComp₂₃ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₂₃₁' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom	—	CategoryTheory.MonoidalCategory.whiskerRight_tensor
functor₂₃₁'_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₂₃₁' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
functor₂₃₁'_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₂₃₁' CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor₂₃₁_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₂₃Obj CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₂₃₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.tensor_whiskerLeft
functor₂₃₁_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₂₃₁ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₂₃₁_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₂₃₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.whisker_assoc
functor₂₃₁_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₂₃₁ CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor₃₁₂'_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.bifunctorComp₂₃ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.flipFunctor CategoryTheory.Functor.map functor₃₁₂' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
functor₃₁₂'_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.bifunctorComp₂₃ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₃₁₂' CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₃₁₂'_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₃₁₂' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom	—	CategoryTheory.MonoidalCategory.whiskerRight_tensor
functor₃₁₂'_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₃₁₂' CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
functor₃₁₂_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.bifunctorComp₁₂ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.flipFunctor CategoryTheory.Functor.map functor₃₁₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.whisker_assoc
functor₃₁₂_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip CategoryTheory.bifunctorComp₁₂ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.map functor₃₁₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv	—	CategoryTheory.MonoidalCategory.tensor_whiskerLeft
functor₃₁₂_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₃₁₂ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
functor₃₁₂_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functor₃₁₂ CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—

CategoryTheory.BraidedCategory.ofBifunctor.Forward

Definitions

Name	Category	Theorems
firstMap₂ 📖	CompOp	1 math math: firstMap₂_app_app_app
firstMap₃ 📖	CompOp	1 math math: firstMap₃_app_app_app
secondMap₁ 📖	CompOp	1 math math: secondMap₁_app_app_app
secondMap₂ 📖	CompOp	1 math math: secondMap₂_app_app_app
secondMap₃ 📖	CompOp	1 math math: secondMap₃_app_app_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
firstMap₂_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₂₃FunctorObj CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ firstMap₂ CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
firstMap₃_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' firstMap₃ CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.associator	—	—
secondMap₁_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₁₂FunctorObj CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ secondMap₁ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom	—	—
secondMap₂_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' secondMap₂ CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.associator	—	—
secondMap₃_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip₁₃ CategoryTheory.flipFunctor CategoryTheory.bifunctorComp₂₃Functor CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' secondMap₃ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom	—	—

CategoryTheory.BraidedCategory.ofBifunctor.Reverse

Definitions

Name	Category	Theorems
firstMap₂ 📖	CompOp	1 math math: firstMap₂_app_app_app
firstMap₃ 📖	CompOp	1 math math: firstMap₃_app_app_app
secondMap₁ 📖	CompOp	1 math math: secondMap₁_app_app_app
secondMap₂ 📖	CompOp	1 math math: secondMap₂_app_app_app
secondMap₃ 📖	CompOp	1 math math: secondMap₃_app_app_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
firstMap₂_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip₂₃ CategoryTheory.flipFunctor CategoryTheory.bifunctorComp₂₃Functor CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' firstMap₂ CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom	—	—
firstMap₃_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip₂₃ CategoryTheory.Functor.flip CategoryTheory.bifunctorComp₂₃ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.bifunctorComp₁₂ CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ firstMap₃ CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.associator	—	—
secondMap₁_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.bifunctorComp₂₃ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' secondMap₁ CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom	—	—
secondMap₂_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ secondMap₂ CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.associator	—	—
secondMap₃_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip₂₃ CategoryTheory.bifunctorComp₁₂ CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.flip CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ secondMap₃ CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom	—	—

CategoryTheory.SymmetricCategory

Definitions

Name	Category	Theorems
ofCurried 📖	CompOp	—

---

← Back to Index