Trifunctor

📁 Source: Mathlib/CategoryTheory/Functor/Trifunctor.lean

Statistics

Metric	Count
Definitions bifunctorComp₁₂, bifunctorComp₁₂Functor, bifunctorComp₁₂FunctorMap, bifunctorComp₁₂FunctorObj, bifunctorComp₁₂Obj, bifunctorComp₂₃, bifunctorComp₂₃Functor, bifunctorComp₂₃FunctorMap, bifunctorComp₂₃FunctorObj, bifunctorComp₂₃Obj	10
Theorems bifunctorComp₁₂FunctorMap_app_app_app_app, bifunctorComp₁₂FunctorObj_map_app_app_app, bifunctorComp₁₂FunctorObj_obj, bifunctorComp₁₂Functor_map, bifunctorComp₁₂Functor_obj, bifunctorComp₁₂Obj_map_app, bifunctorComp₁₂Obj_obj_map, bifunctorComp₁₂Obj_obj_obj, bifunctorComp₁₂_map_app_app, bifunctorComp₁₂_obj, bifunctorComp₂₃FunctorMap_app_app_app_app, bifunctorComp₂₃FunctorObj_map_app_app_app, bifunctorComp₂₃FunctorObj_obj, bifunctorComp₂₃Functor_map, bifunctorComp₂₃Functor_obj, bifunctorComp₂₃Obj_map_app, bifunctorComp₂₃Obj_obj_map, bifunctorComp₂₃Obj_obj_obj, bifunctorComp₂₃_map_app_app, bifunctorComp₂₃_obj	20
Total	30

CategoryTheory

Definitions

Name	Category	Theorems
bifunctorComp₁₂ 📖	CompOp	34 math math: Functor.LaxMonoidal.ofBifunctor.secondMap₁_app_app_app, MonoidalCategory.curriedAssociatorNatIso_hom_app_app_app, Functor.LaxMonoidal.ofBifunctor.firstMap₃_app_app_app, MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_hom_app_app_app, HomologicalComplex.ι_mapBifunctorAssociatorX_hom, BraidedCategory.Hexagon.functor₃₁₂_map_app_app, Functor.OplaxMonoidal.ofBifunctor.firstMap₁_app_app_app, BraidedCategory.Hexagon.functor₁₃₂_map_app_app, bifunctorComp₁₂_map_app_app, GradedObject.ι_mapBifunctorAssociator_hom_assoc, GradedObject.HasGoodTrifunctor₁₂Obj.hasMap, MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_inv_app_app_app, HomologicalComplex.ι_mapBifunctorAssociatorX_hom_assoc, bifunctorComp₁₂_obj, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom, MonoidalCategory.MonoidalRightAction.actionAssocNatIso_inv_app_app_app, GradedObject.ι_mapBifunctorAssociator_hom, MonoidalCategory.curriedAssociatorNatIso_inv_app_app_app, bifunctorComp₁₂FunctorObj_obj, BraidedCategory.ofBifunctor.Reverse.secondMap₃_app_app_app, Functor.OplaxMonoidal.ofBifunctor.secondMap₁_app_app_app, bifunctorComp₁₂FunctorObj_map_app_app_app, BraidedCategory.ofBifunctor.Reverse.firstMap₃_app_app_app, Functor.bifunctorComp₁₂Iso_inv_app_app_app, Functor.LaxMonoidal.ofBifunctor.firstMap₂_app_app_app, Functor.bifunctorComp₁₂Iso_hom_app_app_app, BraidedCategory.Hexagon.functor₃₁₂_obj_map_app, GradedObject.ι_mapBifunctorAssociator_inv_assoc, MonoidalCategory.MonoidalRightAction.actionAssocNatIso_hom_app_app_app, Functor.OplaxMonoidal.ofBifunctor.firstMap₃_app_app_app, GradedObject.ι_mapBifunctorAssociator_inv, BraidedCategory.Hexagon.functor₁₃₂_obj_map_app, Localization.associator_hom_app_app_app, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom_assoc
bifunctorComp₁₂Functor 📖	CompOp	2 math math: bifunctorComp₁₂Functor_obj, bifunctorComp₁₂Functor_map
bifunctorComp₁₂FunctorMap 📖	CompOp	2 math math: bifunctorComp₁₂FunctorMap_app_app_app_app, bifunctorComp₁₂Functor_map
bifunctorComp₁₂FunctorObj 📖	CompOp	7 math math: Functor.OplaxMonoidal.ofBifunctor.firstMap₂_app_app_app, bifunctorComp₁₂FunctorMap_app_app_app_app, bifunctorComp₁₂Functor_obj, BraidedCategory.ofBifunctor.Forward.secondMap₁_app_app_app, Functor.LaxMonoidal.ofBifunctor.firstMap₁_app_app_app, bifunctorComp₁₂FunctorObj_obj, bifunctorComp₁₂FunctorObj_map_app_app_app
bifunctorComp₁₂Obj 📖	CompOp	7 math math: bifunctorComp₁₂Obj_obj_obj, bifunctorComp₁₂_map_app_app, BraidedCategory.Hexagon.functor₁₂₃_map_app_app, BraidedCategory.Hexagon.functor₂₁₃_map_app_app, bifunctorComp₁₂_obj, bifunctorComp₁₂Obj_obj_map, bifunctorComp₁₂Obj_map_app
bifunctorComp₂₃ 📖	CompOp	36 math math: BraidedCategory.Hexagon.functor₂₁₃'_map_app_app, Functor.LaxMonoidal.ofBifunctor.secondMap₁_app_app_app, BraidedCategory.ofBifunctor.Reverse.secondMap₁_app_app_app, MonoidalCategory.curriedAssociatorNatIso_hom_app_app_app, Functor.LaxMonoidal.ofBifunctor.firstMap₃_app_app_app, MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_hom_app_app_app, HomologicalComplex.ι_mapBifunctorAssociatorX_hom, bifunctorComp₂₃_obj, BraidedCategory.Hexagon.functor₂₃₁'_map_app_app, bifunctorComp₂₃_map_app_app, Functor.OplaxMonoidal.ofBifunctor.secondMap₃_app_app_app, BraidedCategory.Hexagon.functor₂₁₃'_obj_map_app, GradedObject.ι_mapBifunctorAssociator_hom_assoc, BraidedCategory.Hexagon.functor₃₁₂'_map_app_app, MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_inv_app_app_app, HomologicalComplex.ι_mapBifunctorAssociatorX_hom_assoc, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom, MonoidalCategory.MonoidalRightAction.actionAssocNatIso_inv_app_app_app, GradedObject.ι_mapBifunctorAssociator_hom, Functor.LaxMonoidal.ofBifunctor.secondMap₂_app_app_app, BraidedCategory.Hexagon.functor₂₃₁'_obj_map_app, MonoidalCategory.curriedAssociatorNatIso_inv_app_app_app, bifunctorComp₂₃FunctorObj_map_app_app_app, GradedObject.HasGoodTrifunctor₂₃Obj.hasMap, Functor.OplaxMonoidal.ofBifunctor.secondMap₁_app_app_app, bifunctorComp₂₃FunctorObj_obj, BraidedCategory.ofBifunctor.Reverse.firstMap₃_app_app_app, Functor.bifunctorComp₂₃Iso_hom_app_app_app, GradedObject.ι_mapBifunctorAssociator_inv_assoc, MonoidalCategory.MonoidalRightAction.actionAssocNatIso_hom_app_app_app, Functor.OplaxMonoidal.ofBifunctor.firstMap₃_app_app_app, GradedObject.ι_mapBifunctorAssociator_inv, BraidedCategory.Hexagon.functor₃₁₂'_obj_map_app, Localization.associator_hom_app_app_app, Functor.bifunctorComp₂₃Iso_inv_app_app_app, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom_assoc
bifunctorComp₂₃Functor 📖	CompOp	4 math math: BraidedCategory.ofBifunctor.Forward.secondMap₃_app_app_app, BraidedCategory.ofBifunctor.Reverse.firstMap₂_app_app_app, bifunctorComp₂₃Functor_map, bifunctorComp₂₃Functor_obj
bifunctorComp₂₃FunctorMap 📖	CompOp	2 math math: bifunctorComp₂₃Functor_map, bifunctorComp₂₃FunctorMap_app_app_app_app
bifunctorComp₂₃FunctorObj 📖	CompOp	7 math math: Functor.OplaxMonoidal.ofBifunctor.secondMap₂_app_app_app, BraidedCategory.ofBifunctor.Forward.firstMap₂_app_app_app, bifunctorComp₂₃FunctorObj_map_app_app_app, bifunctorComp₂₃Functor_obj, bifunctorComp₂₃FunctorObj_obj, bifunctorComp₂₃FunctorMap_app_app_app_app, Functor.LaxMonoidal.ofBifunctor.secondMap₃_app_app_app
bifunctorComp₂₃Obj 📖	CompOp	8 math math: BraidedCategory.Hexagon.functor₂₃₁_map_app_app, bifunctorComp₂₃_obj, bifunctorComp₂₃_map_app_app, bifunctorComp₂₃Obj_obj_obj, BraidedCategory.Hexagon.functor₁₃₂'_map_app_app, BraidedCategory.Hexagon.functor₁₂₃'_map_app_app, bifunctorComp₂₃Obj_map_app, bifunctorComp₂₃Obj_obj_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bifunctorComp₁₂FunctorMap_app_app_app_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category bifunctorComp₁₂FunctorObj bifunctorComp₁₂FunctorMap Functor.map	—	—
bifunctorComp₁₂FunctorObj_map_app_app_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category bifunctorComp₁₂ Functor.map bifunctorComp₁₂FunctorObj	—	—
bifunctorComp₁₂FunctorObj_obj 📖	mathematical	—	Functor.obj Functor Functor.category bifunctorComp₁₂FunctorObj bifunctorComp₁₂	—	—
bifunctorComp₁₂Functor_map 📖	mathematical	—	Functor.map Functor Functor.category bifunctorComp₁₂Functor bifunctorComp₁₂FunctorMap	—	—
bifunctorComp₁₂Functor_obj 📖	mathematical	—	Functor.obj Functor Functor.category bifunctorComp₁₂Functor bifunctorComp₁₂FunctorObj	—	—
bifunctorComp₁₂Obj_map_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.map bifunctorComp₁₂Obj	—	—
bifunctorComp₁₂Obj_obj_map 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category bifunctorComp₁₂Obj	—	—
bifunctorComp₁₂Obj_obj_obj 📖	mathematical	—	Functor.obj Functor Functor.category bifunctorComp₁₂Obj	—	—
bifunctorComp₁₂_map_app_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category bifunctorComp₁₂Obj Functor.map bifunctorComp₁₂	—	—
bifunctorComp₁₂_obj 📖	mathematical	—	Functor.obj Functor Functor.category bifunctorComp₁₂ bifunctorComp₁₂Obj	—	—
bifunctorComp₂₃FunctorMap_app_app_app_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category bifunctorComp₂₃FunctorObj bifunctorComp₂₃FunctorMap	—	—
bifunctorComp₂₃FunctorObj_map_app_app_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category bifunctorComp₂₃ Functor.map bifunctorComp₂₃FunctorObj	—	—
bifunctorComp₂₃FunctorObj_obj 📖	mathematical	—	Functor.obj Functor Functor.category bifunctorComp₂₃FunctorObj bifunctorComp₂₃	—	—
bifunctorComp₂₃Functor_map 📖	mathematical	—	Functor.map Functor Functor.category bifunctorComp₂₃Functor bifunctorComp₂₃FunctorMap	—	—
bifunctorComp₂₃Functor_obj 📖	mathematical	—	Functor.obj Functor Functor.category bifunctorComp₂₃Functor bifunctorComp₂₃FunctorObj	—	—
bifunctorComp₂₃Obj_map_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.map bifunctorComp₂₃Obj	—	—
bifunctorComp₂₃Obj_obj_map 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category bifunctorComp₂₃Obj	—	—
bifunctorComp₂₃Obj_obj_obj 📖	mathematical	—	Functor.obj Functor Functor.category bifunctorComp₂₃Obj	—	—
bifunctorComp₂₃_map_app_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category bifunctorComp₂₃Obj Functor.map bifunctorComp₂₃	—	—
bifunctorComp₂₃_obj 📖	mathematical	—	Functor.obj Functor Functor.category bifunctorComp₂₃ bifunctorComp₂₃Obj	—	—

---

← Back to Index