Documentation Verification Report

NaturalTransformation

📁 Source: Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

Statistics

Metric	Count
Definitions `hom`, `homMk`, `instCategory`, `isoMk`, `isoOfComponents`, `IsMonoidal`	6
Theorems `instIsMonoidalCounit`, `instIsMonoidalUnit`, `instIsMonoidalCounit`, `instIsMonoidalUnit`, `natTransIsMonoidal_of_transport`, `instIsMonoidalInvFunctor`, `isMonoidal`, `comp_hom`, `comp_hom_assoc`, `homMk_hom`, `hom_ext`, `hom_ext_iff`, `id_hom`, `isoMk_hom`, `isoMk_inv`, `isoOfComponents_hom_hom_app`, `isoOfComponents_inv_hom_app`, `comp`, `hcomp`, `id`, `instHomFunctorAssociator`, `instHomFunctorLeftUnitor`, `instHomFunctorRightUnitor`, `tensor`, `tensor_assoc`, `unit`, `unit_assoc`, `whiskerLeft`, `whiskerRight`, `instIsMonoidalProdProd'`	30
Total	36

CategoryTheory.Adjunction.Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsMonoidalCounit` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Equivalence.functor` `CategoryTheory.Functor.id` `CategoryTheory.Equivalence.counit` `CategoryTheory.Functor.LaxMonoidal.comp` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `CategoryTheory.Functor.LaxMonoidal.id`	—	`CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalCounit`
`instIsMonoidalUnit` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.functor` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Equivalence.unit` `CategoryTheory.Functor.LaxMonoidal.id` `CategoryTheory.Functor.LaxMonoidal.comp` `CategoryTheory.Functor.Monoidal.toLaxMonoidal`	—	`CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalUnit`

CategoryTheory.Adjunction.IsMonoidal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsMonoidalCounit` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.counit` `CategoryTheory.Functor.LaxMonoidal.comp` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `CategoryTheory.Functor.LaxMonoidal.id`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Adjunction.map_ε_comp_counit_app_unit` `CategoryTheory.Functor.Monoidal.ε_η` `CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor` `CategoryTheory.Functor.Monoidal.μ_δ_assoc` `CategoryTheory.Category.comp_id`
`instIsMonoidalUnit` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.LaxMonoidal.id` `CategoryTheory.Functor.LaxMonoidal.comp` `CategoryTheory.Functor.Monoidal.toLaxMonoidal`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Adjunction.unit_app_unit_comp_map_η` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.Monoidal.map_η_ε` `CategoryTheory.Category.comp_id` `CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ_assoc` `CategoryTheory.Functor.Monoidal.map_δ_μ`

CategoryTheory.Functor.Monoidal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natTransIsMonoidal_of_transport` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `toLaxMonoidal` `transport`	—	`CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.MonoidalCategory.id_whiskerRight` `CategoryTheory.Category.id_comp`

CategoryTheory.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsMonoidalInvFunctor` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	`CategoryTheory.NatTrans.IsMonoidal.unit` `CategoryTheory.Category.assoc` `hom_inv_id_app` `CategoryTheory.Category.comp_id` `CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.NatIso.hom_app_isIso` `inv_hom_id_app` `CategoryTheory.NatTrans.IsMonoidal.tensor` `CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.MonoidalCategory.id_whiskerRight` `CategoryTheory.Category.id_comp`

CategoryTheory.LaxMonoidalFunctor

Definitions

Name	Category	Theorems
`homMk` 📖	CompOp	3 math math: `isoMk_inv`, `homMk_hom`, `isoMk_hom`
`instCategory` 📖	CompOp	47 math math: `TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux`, `CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse`, `CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_hom_app`, `CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app`, `CategoryTheory.LaxBraidedFunctor.comp_hom`, `CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_app`, `isoOfComponents_inv_hom_app`, `CategoryTheory.LaxBraidedFunctor.forget_map`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app`, `isoMk_inv`, `CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_hom_app`, `CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app`, `CategoryTheory.Functor.mapCommMonFunctor_map_app`, `CategoryTheory.LaxBraidedFunctor.comp_hom_assoc`, `CategoryTheory.Functor.mapMonFunctor_obj`, `isoOfComponents_hom_hom_app`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one`, `CategoryTheory.Functor.mapMonFunctor_map_app_hom`, `CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso`, `CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom`, `CategoryTheory.LaxBraidedFunctor.homMk_hom_hom`, `CategoryTheory.LaxBraidedFunctor.forget_obj`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv`, `CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor`, `CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_app`, `comp_hom`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_IsMon_Hom`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map`, `isoMk_hom`, `CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app`, `comp_hom_assoc`, `CategoryTheory.LaxBraidedFunctor.id_hom`, `TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul`, `CategoryTheory.LaxBraidedFunctor.hom_ext_iff`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj`, `TannakaDuality.FiniteGroup.equivHom_surjective`, `TannakaDuality.FiniteGroup.equivHom_injective`, `id_hom`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app`, `TannakaDuality.FiniteGroup.equivHom_apply`
`isoMk` 📖	CompOp	2 math math: `isoMk_inv`, `isoMk_hom`
`isoOfComponents` 📖	CompOp	3 math math: `isoOfComponents_inv_hom_app`, `isoOfComponents_hom_hom_app`, `TannakaDuality.FiniteGroup.equivHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.LaxMonoidalFunctor` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `toFunctor`	—	—
`comp_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `toFunctor` `Hom.hom` `CategoryTheory.LaxMonoidalFunctor` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_hom`
`homMk_hom` 📖	mathematical	—	`Hom.hom` `homMk`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	—
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`id_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.LaxMonoidalFunctor` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `toFunctor`	—	—
`isoMk_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.LaxMonoidalFunctor` `instCategory` `isoMk` `homMk` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `toFunctor`	—	—
`isoMk_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.LaxMonoidalFunctor` `instCategory` `isoMk` `homMk` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `toFunctor`	—	—
`isoOfComponents_hom_hom_app` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `toFunctor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.LaxMonoidal.ε` `laxMonoidal` `CategoryTheory.Iso.hom`	`CategoryTheory.NatTrans.app` `Hom.hom` `CategoryTheory.LaxMonoidalFunctor` `instCategory` `isoOfComponents`	—	—
`isoOfComponents_inv_hom_app` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `toFunctor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.LaxMonoidal.ε` `laxMonoidal` `CategoryTheory.Iso.hom`	`CategoryTheory.NatTrans.app` `Hom.hom` `CategoryTheory.Iso.inv` `CategoryTheory.LaxMonoidalFunctor` `instCategory` `isoOfComponents`	—	—

CategoryTheory.LaxMonoidalFunctor.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	25 math math: `TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular`, `CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_hom_app`, `CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app`, `CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_app`, `CategoryTheory.LaxMonoidalFunctor.isoOfComponents_inv_hom_app`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app`, `CategoryTheory.LaxMonoidalFunctor.homMk_hom`, `CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_hom_app`, `CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app`, `CategoryTheory.Functor.mapCommMonFunctor_map_app`, `CategoryTheory.LaxMonoidalFunctor.isoOfComponents_hom_hom_app`, `CategoryTheory.LaxMonoidalFunctor.hom_ext_iff`, `CategoryTheory.Functor.mapMonFunctor_map_app_hom`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app`, `CategoryTheory.LaxBraidedFunctor.homMk_hom_hom`, `CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_app`, `CategoryTheory.LaxMonoidalFunctor.comp_hom`, `CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app`, `isMonoidal`, `CategoryTheory.LaxMonoidalFunctor.comp_hom_assoc`, `CategoryTheory.LaxBraidedFunctor.id_hom`, `TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp`, `CategoryTheory.LaxBraidedFunctor.hom_ext_iff`, `CategoryTheory.LaxMonoidalFunctor.id_hom`, `CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMonoidal` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.LaxMonoidalFunctor.toFunctor` `hom` `CategoryTheory.LaxMonoidalFunctor.laxMonoidal`	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
`IsMonoidal` 📖	CompData	22 math math: `IsMonoidal.instHomFunctorAssociator`, `CategoryTheory.Functor.Monoidal.natTransIsMonoidal_of_transport`, `CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported`, `instIsMonoidalProdProd'`, `CategoryTheory.Discrete.monoidalFunctorComp_isMonoidal`, `CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported`, `CategoryTheory.Localization.Monoidal.lifting_isMonoidal`, `IsMonoidal.of_cartesianMonoidalCategory`, `CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit`, `CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit`, `IsMonoidal.hcomp`, `CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalUnit`, `IsMonoidal.comp`, `IsMonoidal.whiskerRight`, `IsMonoidal.id`, `IsMonoidal.instHomFunctorRightUnitor`, `IsMonoidal.instHomFunctorLeftUnitor`, `CategoryTheory.Discrete.addMonoidalFunctorComp_isMonoidal`, `CategoryTheory.Iso.instIsMonoidalInvFunctor`, `CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal`, `CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalCounit`, `IsMonoidal.whiskerLeft`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsMonoidalProdProd'` 📖	mathematical	—	`IsMonoidal` `CategoryTheory.prod'` `CategoryTheory.MonoidalCategory.prodMonoidal` `CategoryTheory.Functor.prod'` `prod'` `CategoryTheory.Functor.LaxMonoidal.prod'`	—	`CategoryTheory.Prod.hom_ext` `CategoryTheory.prod_comp_fst` `CategoryTheory.Functor.prod'_ε_fst` `prod'_app_fst` `IsMonoidal.unit` `CategoryTheory.prod_comp_snd` `CategoryTheory.Functor.prod'_ε_snd` `prod'_app_snd` `CategoryTheory.Functor.prod'_μ_fst` `IsMonoidal.tensor` `CategoryTheory.Functor.prod'_μ_snd`

CategoryTheory.NatTrans.IsMonoidal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`unit_assoc` `unit` `tensor_assoc` `tensor` `CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc`
`hcomp` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.hcomp` `CategoryTheory.Functor.LaxMonoidal.comp`	—	`CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality_assoc` `unit` `unit_assoc` `tensor_assoc` `CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc` `tensor`
`id` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.MonoidalCategory.id_whiskerRight` `CategoryTheory.Category.id_comp`
`instHomFunctorAssociator` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.LaxMonoidal.comp`	—	`CategoryTheory.Functor.map_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.MonoidalCategory.id_whiskerRight` `CategoryTheory.Category.id_comp`
`instHomFunctorLeftUnitor` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.leftUnitor` `CategoryTheory.Functor.LaxMonoidal.comp` `CategoryTheory.Functor.LaxMonoidal.id`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.MonoidalCategory.id_whiskerRight` `CategoryTheory.Category.id_comp`
`instHomFunctorRightUnitor` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.rightUnitor` `CategoryTheory.Functor.LaxMonoidal.comp` `CategoryTheory.Functor.LaxMonoidal.id`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.MonoidalCategory.id_whiskerRight`
`tensor` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxMonoidal.μ` `CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategoryStruct.tensorHom`	—	—
`tensor_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxMonoidal.μ` `CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategoryStruct.tensorHom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `tensor`
`unit` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxMonoidal.ε` `CategoryTheory.NatTrans.app`	—	—
`unit_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxMonoidal.ε` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `unit`
`whiskerLeft` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Functor.LaxMonoidal.comp`	—	`CategoryTheory.Functor.id_hcomp` `hcomp` `id`
`whiskerRight` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Functor.LaxMonoidal.comp`	—	`CategoryTheory.Functor.hcomp_id` `hcomp` `id`

---

← Back to Index