Basic

📁 Source: Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean

Statistics

Metric	Count
Definitions ofCartesianMonoidalCategory, CartesianMonoidalCategory, fullSubcategory, homEquivToProd, isLimitCartesianMonoidalCategoryOfPreservesLimits, ofChosenFiniteProducts, tensorHom, tensorObj, ofHasFiniteProducts, preservesTerminalIso, prodComparison, prodComparisonBifunctorNatIso, prodComparisonBifunctorNatTrans, prodComparisonIso, prodComparisonNatIso, prodComparisonNatTrans, tensorLeftIsoProd, tensorProductIsBinaryProduct, terminalComparison, toSemiCartesianMonoidalCategory, toSymmetricCategory, ofChosenFiniteProducts, ofChosenFiniteProducts, ofChosenFiniteProducts, SemiCartesianMonoidalCategory, fst, instUniqueHomTensorUnit, isTerminalTensorUnit, snd, toMonoidalCategory, toUnit	31
Theorems associator_hom_fst, associator_hom_fst_assoc, associator_hom_snd_fst, associator_hom_snd_fst_assoc, associator_hom_snd_snd, associator_hom_snd_snd_assoc, associator_inv_fst_fst, associator_inv_fst_fst_assoc, associator_inv_fst_snd, associator_inv_fst_snd_assoc, associator_inv_snd, associator_inv_snd_assoc, braiding_hom_fst, braiding_hom_fst_assoc, braiding_hom_snd, braiding_hom_snd_assoc, braiding_inv_fst, braiding_inv_fst_assoc, braiding_inv_snd, braiding_inv_snd_assoc, comp_lift, comp_lift_assoc, fullSubcategory_associator_hom_hom, fullSubcategory_associator_inv_hom, fullSubcategory_fst_hom, fullSubcategory_isTerminalTensorUnit_lift_hom, fullSubcategory_leftUnitor_hom_hom, fullSubcategory_leftUnitor_inv_hom, fullSubcategory_rightUnitor_hom_hom, fullSubcategory_rightUnitor_inv_hom, fullSubcategory_snd_hom, fullSubcategory_tensorHom_hom, fullSubcategory_tensorObj_obj, fullSubcategory_tensorProductIsBinaryProduct_lift_hom, fullSubcategory_tensorUnit_obj, fullSubcategory_whiskerLeft_hom, fullSubcategory_whiskerRight_hom, homEquivToProd_apply, homEquivToProd_symm_apply, hom_ext, hom_ext_iff, instHasFiniteProducts, instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison, instIsIsoFunctorProdComparisonNatTransOfProdComparison, instNonemptyBraidedCategory, instSubsingletonBraidedCategory, instSubsingletonSymmetricCategory, inv_prodComparison_map_fst, inv_prodComparison_map_fst_assoc, inv_prodComparison_map_snd, inv_prodComparison_map_snd_assoc, isIso_prodComparison_of_preservesLimit_pair, leftUnitor_hom, leftUnitor_inv_fst, leftUnitor_inv_fst_assoc, leftUnitor_inv_snd, leftUnitor_inv_snd_assoc, lift_braiding_hom, lift_braiding_hom_assoc, lift_braiding_inv, lift_braiding_inv_assoc, lift_comp_fst_snd, lift_fst, lift_fst_assoc, lift_fst_comp_snd_comp, lift_fst_snd, lift_leftUnitor_hom, lift_leftUnitor_hom_assoc, lift_lift_associator_hom, lift_lift_associator_hom_assoc, lift_lift_associator_inv, lift_lift_associator_inv_assoc, lift_map, lift_map_assoc, lift_rightUnitor_hom, lift_rightUnitor_hom_assoc, lift_snd, lift_snd_assoc, lift_snd_comp_fst_comp, lift_snd_comp_fst_comp_assoc, lift_snd_fst, lift_whiskerLeft, lift_whiskerLeft_assoc, lift_whiskerRight, lift_whiskerRight_assoc, map_toUnit_comp_terminalComparison, map_toUnit_comp_terminalComparison_assoc, mono_lift_of_mono_left, mono_lift_of_mono_right, associator_naturality, id_tensorHom_id, leftUnitor_naturality, pentagon, rightUnitor_naturality, tensorHom_comp_tensorHom, triangle, preservesLimit_empty_of_isIso_terminalComparison, preservesLimit_pair_of_isIso_prodComparison, preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison, preservesTerminalIso_comp, preservesTerminalIso_hom, preservesTerminalIso_id, prodComparisonBifunctorNatIso_hom, prodComparisonBifunctorNatIso_inv, prodComparisonBifunctorNatTrans_app, prodComparisonBifunctorNatTrans_comp, prodComparisonIso_comp, prodComparisonIso_hom, prodComparisonIso_id, prodComparisonNatIso_hom, prodComparisonNatIso_inv, prodComparisonNatTrans_app, prodComparisonNatTrans_comp, prodComparisonNatTrans_id, prodComparison_comp, prodComparison_fst, prodComparison_fst_assoc, prodComparison_id, prodComparison_inv_natural, prodComparison_inv_natural_assoc, prodComparison_inv_natural_whiskerLeft, prodComparison_inv_natural_whiskerLeft_assoc, prodComparison_inv_natural_whiskerRight, prodComparison_inv_natural_whiskerRight_assoc, prodComparison_natural, prodComparison_natural_assoc, prodComparison_natural_whiskerLeft, prodComparison_natural_whiskerLeft_assoc, prodComparison_natural_whiskerRight, prodComparison_natural_whiskerRight_assoc, prodComparison_snd, prodComparison_snd_assoc, rightUnitor_hom, rightUnitor_inv_fst, rightUnitor_inv_fst_assoc, rightUnitor_inv_snd, rightUnitor_inv_snd_assoc, tensorHom_fst, tensorHom_fst_assoc, tensorHom_snd, tensorHom_snd_assoc, tensorδ_fst, tensorδ_fst_assoc, tensorδ_snd, tensorδ_snd_assoc, tensorμ_fst, tensorμ_fst_assoc, tensorμ_snd, tensorμ_snd_assoc, terminalComparison_isIso_of_preservesLimits, whiskerLeft_fst, whiskerLeft_fst_assoc, whiskerLeft_snd, whiskerLeft_snd_assoc, whiskerLeft_toUnit_comp_rightUnitor_hom, whiskerLeft_toUnit_comp_rightUnitor_hom_assoc, whiskerRight_fst, whiskerRight_fst_assoc, whiskerRight_snd, whiskerRight_snd_assoc, whiskerRight_toUnit_comp_leftUnitor_hom, whiskerRight_toUnit_comp_leftUnitor_hom_assoc, instSubsingleton, associator_hom_def, associator_inv_def, lift_def, tensor_obj, toUnit_def, instPreservesFiniteProducts, instSubsingleton, lift_μ, lift_μ_assoc, nonempty_monoidal_iff_preservesFiniteProducts, toUnit_ε, toUnit_ε_assoc, ε_of_cartesianMonoidalCategory, μ_comp, μ_comp_assoc, μ_fst, μ_fst_assoc, μ_of_cartesianMonoidalCategory, μ_snd, μ_snd_assoc, instIsIsoδ, instIsIsoη, instSubsingleton, lift_δ, lift_δ_assoc, δ_fst, δ_fst_assoc, δ_of_cartesianMonoidalCategory, δ_snd, δ_snd_assoc, η_of_cartesianMonoidalCategory, of_cartesianMonoidalCategory, comp_toUnit, comp_toUnit_assoc, default_eq_toUnit, fst_def, snd_def, toUnit_unique, toUnit_unique_iff, toUnit_unit	203
Total	234

CategoryTheory

Definitions

Name	Category	Theorems
CartesianMonoidalCategory 📖	CompData	—
SemiCartesianMonoidalCategory 📖	CompData	—

CategoryTheory.BraidedCategory

Definitions

Name	Category	Theorems
ofCartesianMonoidalCategory 📖	CompOp	—

CategoryTheory.CartesianMonoidalCategory

Definitions

Name	Category	Theorems
fullSubcategory 📖	CompOp	20 math math: CategoryTheory.Functor.EssImageSubcategory.associator_inv_def, fullSubcategory_rightUnitor_hom_hom, fullSubcategory_leftUnitor_inv_hom, CategoryTheory.Functor.EssImageSubcategory.associator_hom_def, fullSubcategory_tensorObj_obj, fullSubcategory_snd_hom, fullSubcategory_isTerminalTensorUnit_lift_hom, fullSubcategory_fst_hom, fullSubcategory_associator_inv_hom, CategoryTheory.Functor.EssImageSubcategory.tensor_obj, fullSubcategory_tensorUnit_obj, CategoryTheory.Functor.EssImageSubcategory.toUnit_def, fullSubcategory_leftUnitor_hom_hom, fullSubcategory_associator_hom_hom, fullSubcategory_whiskerRight_hom, fullSubcategory_tensorProductIsBinaryProduct_lift_hom, fullSubcategory_whiskerLeft_hom, CategoryTheory.Functor.EssImageSubcategory.lift_def, fullSubcategory_tensorHom_hom, fullSubcategory_rightUnitor_inv_hom
homEquivToProd 📖	CompOp	3 math math: CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj_homEquiv, homEquivToProd_apply, homEquivToProd_symm_apply
isLimitCartesianMonoidalCategoryOfPreservesLimits 📖	CompOp	—
ofChosenFiniteProducts 📖	CompOp	—
ofHasFiniteProducts 📖	CompOp	6 math math: CategoryTheory.monoidalOfHasFiniteProducts.δ_eq, CategoryTheory.symmetricOfHasFiniteProducts_braiding_hom, CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoδ, CategoryTheory.symmetricOfHasFiniteProducts_braiding_inv, CategoryTheory.monoidalOfHasFiniteProducts.η_eq, CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoη
preservesTerminalIso 📖	CompOp	5 math math: CategoryTheory.Over.preservesTerminalIso_pullback, preservesTerminalIso_hom, preservesTerminalIso_comp, CategoryTheory.Functor.Monoidal.ε_of_cartesianMonoidalCategory, preservesTerminalIso_id
prodComparison 📖	CompOp	34 math math: prodComparison_snd, prodComparison_fst, CategoryTheory.prodComparison_iso, CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory, CategoryTheory.Functor.Monoidal.tensorObjComp_hom_app, CategoryTheory.IsSifted.factorization_prodComparison_colim, CategoryTheory.IsSifted.instIsIsoObjFunctorTypeColimTensorObjProdComparison, CategoryTheory.coev_expComparison, prodComparisonIso_hom, prodComparison_id, prodComparison_natural, prodComparison_natural_whiskerLeft_assoc, prodComparison_snd_assoc, prodComparison_natural_assoc, CategoryTheory.bijection_symm_apply_id, inv_prodComparison_map_fst_assoc, prodComparison_comp, inv_prodComparison_map_snd_assoc, prodComparison_natural_whiskerRight, prodComparison_natural_whiskerRight_assoc, CategoryTheory.uncurry_expComparison, prodComparison_inv_natural_whiskerLeft, prodComparison_inv_natural_whiskerRight_assoc, CategoryTheory.expComparison_ev, inv_prodComparison_map_snd, prodComparison_inv_natural, inv_prodComparison_map_fst, prodComparison_fst_assoc, prodComparison_inv_natural_whiskerRight, prodComparison_inv_natural_whiskerLeft_assoc, prodComparisonNatTrans_app, prodComparison_inv_natural_assoc, isIso_prodComparison_of_preservesLimit_pair, prodComparison_natural_whiskerLeft
prodComparisonBifunctorNatIso 📖	CompOp	2 math math: prodComparisonBifunctorNatIso_inv, prodComparisonBifunctorNatIso_hom
prodComparisonBifunctorNatTrans 📖	CompOp	5 math math: prodComparisonBifunctorNatIso_inv, prodComparisonBifunctorNatIso_hom, prodComparisonBifunctorNatTrans_app, prodComparisonBifunctorNatTrans_comp, instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison
prodComparisonIso 📖	CompOp	9 math math: prodComparisonIso_hom, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, CategoryTheory.Functor.Monoidal.tensorObjComp_inv_app, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', prodComparisonIso_comp, prodComparisonIso_id, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd'
prodComparisonNatIso 📖	CompOp	2 math math: prodComparisonNatIso_hom, prodComparisonNatIso_inv
prodComparisonNatTrans 📖	CompOp	7 math math: prodComparisonNatTrans_comp, prodComparisonNatIso_hom, prodComparisonNatTrans_id, prodComparisonNatIso_inv, instIsIsoFunctorProdComparisonNatTransOfProdComparison, prodComparisonBifunctorNatTrans_app, prodComparisonNatTrans_app
tensorLeftIsoProd 📖	CompOp	—
tensorProductIsBinaryProduct 📖	CompOp	1 math math: fullSubcategory_tensorProductIsBinaryProduct_lift_hom
terminalComparison 📖	CompOp	5 math math: CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory, map_toUnit_comp_terminalComparison_assoc, map_toUnit_comp_terminalComparison, terminalComparison_isIso_of_preservesLimits, preservesTerminalIso_hom
toSemiCartesianMonoidalCategory 📖	CompOp	844 math math: CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val, CategoryTheory.Grp.Hom.hom_div, CategoryTheory.Over.associator_hom_left_snd_fst_assoc, CategoryTheory.Grp.comp', CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor, CategoryTheory.Enriched.Functor.associator_inv_apply, CategoryTheory.GrpObj.lift_inv_comp_left, LightCondensed.free_internallyProjective_iff_tensor_condition, CategoryTheory.Over.μ_pullback_left_snd', CategoryTheory.Functor.natTransEquiv_apply_app, CategoryTheory.Grp.instIsIsoHomHomMon, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_fst_assoc, CategoryTheory.Functor.homObjEquiv_apply_app, CategoryTheory.Grp.homMk'_hom, prodComparison_snd, tensorδ_snd, CategoryTheory.CartesianCopyDiscard.instDeterministic, CategoryTheory.CommGrp.instFullCommMonForget₂CommMon, CategoryTheory.comonEquiv_unitIso, SSet.Truncated.tensor_map_apply_snd, Action.leftRegularTensorIso_inv_hom, CategoryTheory.Equivalence.mapGrp_counitIso, CategoryTheory.Functor.Monoidal.rightUnitor_inv_app, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_fst, AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral, CategoryTheory.Grp.Hom.hom_hom_zpow, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_map, CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst_assoc, CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, CategoryTheory.Over.associator_inv_left_snd, SSet.ι₀_snd_assoc, CategoryTheory.CommGrp.comm, CategoryTheory.instFullMonFunctorOppositeMonCatYonedaMon, CategoryTheory.SimplicialThickening.SimplicialCategory.comp_id, associator_inv_fst_fst, CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app_app, CategoryTheory.Functor.map_mul, CategoryTheory.zeroMul_hom, associator_hom_fst_assoc, prodComparison_fst, CategoryTheory.Functor.mapCommGrp_obj_grp_one, CategoryTheory.Functor.Monoidal.tensorHom_app_fst_assoc, associator_hom_snd_fst_assoc, CategoryTheory.Grp.id', CategoryTheory.Enriched.Functor.whiskerLeft_app_apply, CategoryTheory.GrpObj.lift_inv_right_eq, CategoryTheory.prodComparison_iso, SSet.iSup_subcomplexOfSimplex_prod_eq_top, CategoryTheory.Functor.FullyFaithful.mapGrp_preimage, CategoryTheory.Over.rightUnitor_inv_left_fst_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, CategoryTheory.Functor.OplaxMonoidal.δ_snd_assoc, tensorδ_snd_assoc, CategoryTheory.toOver_obj_hom, CategoryTheory.counit_eq_toUnit, CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj_homEquiv, CategoryTheory.μ_def, CategoryTheory.GrpObj.lift_inv_comp_left_assoc, lift_leftUnitor_hom_assoc, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, CategoryTheory.Functor.EssImageSubcategory.associator_inv_def, CategoryTheory.Grp.trivial_grp_inv, Action.diagonalSuccIsoTensorDiagonal_inv_hom, fullSubcategory_rightUnitor_hom_hom, CategoryTheory.Over.monObjMkPullbackSnd_mul, CategoryTheory.Functor.comp_mapGrp_mul, CategoryTheory.Over.whiskerLeft_left, whiskerLeft_toUnit_comp_rightUnitor_hom, SSet.instHasDimensionLETensorUnitOfNatNat, CategoryTheory.Grp.whiskerLeft_hom_hom, CategoryTheory.GrpObj.left_inv_assoc, CategoryTheory.Functor.mapGrp_id_mul, fullSubcategory_leftUnitor_inv_hom, CategoryTheory.MonObj.instIsMonHomOne, SSet.tensorHom_app_apply, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, CategoryTheory.MonObj.instIsMonHomToUnit, CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, instSubsingletonBraidedCategory, CategoryTheory.Over.grpObjMkPullbackSnd_one, associator_inv_snd, CategoryTheory.Functor.EssImageSubcategory.associator_hom_def, SSet.prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, SSet.Truncated.Edge.map_fst, fullSubcategory_tensorObj_obj, CategoryTheory.Over.grpObjMkPullbackSnd_mul, CategoryTheory.Functor.Monoidal.toUnit_ε_assoc, CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory, CategoryTheory.Grp.leftUnitor_hom_hom, CategoryTheory.CartesianCopyDiscard.instIsCommComonObjOfCartesian, CategoryTheory.Functor.Monoidal.whiskerRight_app_fst_assoc, braiding_hom_snd_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, whiskerRight_snd_assoc, CategoryTheory.comonEquiv_functor, CategoryTheory.CommGrp.toCommMon_X, CategoryTheory.Monoidal.whiskerRight_fst, CategoryTheory.MonObj.lift_comp_one_right, CategoryTheory.Functor.Monoidal.tensorObj_map, CategoryTheory.Functor.Monoidal.lift_μ_assoc, CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory, CategoryTheory.toOver_obj_left, CategoryTheory.Functor.Monoidal.tensorObjComp_hom_app, CategoryTheory.toOverPullbackIsoToOver_inv_app_left, associator_inv_fst_snd, CategoryTheory.Functor.OplaxMonoidal.δ_snd, CategoryTheory.Over.toUnit_left, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, fullSubcategory_snd_hom, CategoryTheory.Functor.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts, SSet.hasDimensionLT_prod, CategoryTheory.monoidalOfHasFiniteProducts.δ_eq, CategoryTheory.Over.braiding_inv_left, CategoryTheory.leftUnitor_hom_apply, SSet.RelativeMorphism.Homotopy.h₀_assoc, CategoryTheory.IsSifted.factorization_prodComparison_colim, CategoryTheory.Grp.ε_def, CategoryTheory.toOverUnit_map_left, CategoryTheory.Grp.rightUnitor_hom_hom_hom, SSet.prodStdSimplex.objEquiv_apply_fst, CategoryTheory.MonObj.ofRepresentableBy_one, CategoryTheory.GrpObj.lift_inv_comp_right, AddGrpCat.tensorObj_eq, CategoryTheory.IsSifted.instIsIsoObjFunctorTypeColimTensorObjProdComparison, CategoryTheory.sheafToPresheaf_μ, CategoryTheory.symmetricOfHasFiniteProducts_braiding_hom, fullSubcategory_isTerminalTensorUnit_lift_hom, CategoryTheory.comul_eq_lift, CategoryTheory.Over.leftUnitor_hom_left, CategoryTheory.Grp.lift_hom, tensorμ_fst_assoc, CategoryTheory.Over.isCommMonObj_mk_pullbackSnd, associator_hom_snd_snd_assoc, CategoryTheory.Over.tensorObj_ext_iff, prodComparisonBifunctorNatIso_inv, CategoryTheory.Grp.hom_mul, CategoryTheory.coev_expComparison, CategoryTheory.types_tensorUnit_def, CategoryTheory.frobeniusMorphism_mate, fullSubcategory_fst_hom, CategoryTheory.toOverIsoToOverUnit_inv_app_left, CategoryTheory.Functor.OplaxMonoidal.δ_fst_assoc, CategoryTheory.MonoidalClosedFunctor.comparison_iso, SSet.instFiniteTensorUnit, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_ext_iff, prodComparisonIso_hom, CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.Over.rightUnitor_inv_left_fst, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_snd_assoc, CategoryTheory.MonObj.lift_comp_one_right_assoc, lift_braiding_hom, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app, CategoryTheory.Grp.Hom.hom_zpow, braiding_inv_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_snd, CategoryTheory.equivToOverUnit_unitIso, CategoryTheory.Preadditive.instIsCommMonObj, instSubsingletonSymmetricCategory, CategoryTheory.GrpObj.one_inv_assoc, CategoryTheory.Functor.mapGrp_obj_grp_one, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, CategoryTheory.NatTrans.IsMonoidal.of_cartesianMonoidalCategory, CommGrpCat.μ_forget_apply, CategoryTheory.Cat.ihom_obj, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, SSet.Subcomplex.ofSimplexProd_eq_range, CategoryTheory.Over.whiskerRight_left_fst, SSet.Truncated.Edge.CompStruct.tensor_simplex_snd, CategoryTheory.Functor.homObjEquiv_symm_apply_app, CategoryTheory.Over.preservesTerminalIso_pullback, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, SSet.prodStdSimplex.objEquiv_δ_apply, CategoryTheory.Adjunction.mapCommGrp_unit, comp_lift, fullSubcategory_associator_inv_hom, CategoryTheory.Functor.mapGrp_id_one, CategoryTheory.Grp.associator_inv_hom_hom, CategoryTheory.Functor.Monoidal.μ_comp_assoc, CategoryTheory.GrpObj.η_whiskerRight_commutator_assoc, prodComparison_id, CategoryTheory.associator_inv_apply, CategoryTheory.GrpObj.lift_comp_inv_right_assoc, CategoryTheory.bijection_natural, lift_lift_associator_inv_assoc, CategoryTheory.Over.rightUnitor_inv_left_snd, CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_hom, SSet.Truncated.Edge.id_tensor_id, braiding_hom_fst, AlgebraicGeometry.instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, CategoryTheory.IsCommMonObj.ofRepresentableBy, CategoryTheory.Grp.Hom.hom_hom_div, lift_lift_associator_inv, CategoryTheory.Grp.leftUnitor_hom_hom_hom, SSet.prodStdSimplex.objEquiv_naturality, CategoryTheory.CommGrp.instIsIsoMonHomGrp, CategoryTheory.Sheaf.tensorProd_isSheaf, CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η, CategoryTheory.toOverUnit_obj_left, CategoryTheory.Functor.Monoidal.μ_fst_assoc, CategoryTheory.Grp.forget_map, tensorHom_fst, prodComparison_natural, CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_left, CategoryTheory.Mon.lift_hom, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_fst, CategoryTheory.IsCommMon.ofRepresentableBy, CategoryTheory.CommGrp.forget₂CommMon_map_hom, CategoryTheory.Functor.EssImageSubcategory.tensor_obj, CategoryTheory.essImage_yonedaMon, CategoryTheory.CommGrp.trivial_X, CategoryTheory.Over.whiskerRight_left_snd_assoc, CategoryTheory.MonObj.instIsMonHomSnd, prodComparison_natural_whiskerLeft_assoc, CategoryTheory.CommGrp.forget₂Grp_obj_mul, CategoryTheory.ChosenPullbacksAlong.Over.snd_eq_snd', lift_braiding_inv, tensorHom_snd_assoc, map_toUnit_comp_terminalComparison_assoc, SSet.instFiniteTensorObj, CategoryTheory.Adjunction.mapGrp_unit, CategoryTheory.Over.associator_inv_left_fst_fst_assoc, AlgebraicGeometry.Scheme.isCommMonObj_asOver_pullback, CategoryTheory.Functor.OplaxMonoidal.instSubsingleton, prodComparison_snd_assoc, CategoryTheory.Over.associator_hom_left_fst, CategoryTheory.Grp.rightUnitor_inv_hom_hom, CategoryTheory.Monoidal.whiskerRight, CategoryTheory.Functor.natTransEquiv_symm_apply_app, CategoryTheory.Grp.forget₂Mon_map_hom, AlgebraicGeometry.Scheme.isMonHom_fst_id_right, prodComparison_natural_assoc, SSet.prodStdSimplex.objEquiv_apply_snd, SSet.hoFunctor.unitHomEquiv_eq, CategoryTheory.GrpObj.tensorHom_inv_inv_mul_assoc, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_snd, CategoryTheory.instFaithfulMonFunctorOppositeMonCatYonedaMon, fullSubcategory_tensorUnit_obj, CategoryTheory.ChosenPullbacksAlong.Over.tensorUnit_hom, CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_snd_assoc, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_fst, CategoryTheory.leftUnitor_inv_apply, CommAlgCat.lift_unop_hom, lift_rightUnitor_hom_assoc, CategoryTheory.Over.tensorUnit_hom, CategoryTheory.Grp.whiskerRight_hom_hom, SSet.instFiniteObjOppositeSimplexCategoryTensorObj, CategoryTheory.Over.leftUnitor_inv_left_fst, associator_hom_snd_fst, CategoryTheory.Monoidal.tensorHom, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val, CategoryTheory.Hom.mul_def, CategoryTheory.Grp.Hom.hom_hom_inv, CategoryTheory.associator_hom_apply_1, SSet.leftUnitor_inv_app_apply, SSet.ι₀_fst_assoc, SSet.ι₁_comp, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_obj, CategoryTheory.CatEnrichedOrdinary.Hom.mk_comp, CategoryTheory.expComparison_whiskerLeft, tensorμ_snd, CommAlgCat.fst_unop_hom, CategoryTheory.Mon.fst_hom, CategoryTheory.Over.tensorHom_left_snd_assoc, CategoryTheory.MonObj.lift_comp_one_left, CategoryTheory.Grp.μ_def, CategoryTheory.Grp.snd_hom, CategoryTheory.Functor.OplaxMonoidal.lift_δ, CategoryTheory.Grp.tensorUnit_mul, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_snd_assoc, leftUnitor_inv_snd, prodComparisonBifunctorNatIso_hom, SSet.whiskerRight_app_apply, CategoryTheory.braiding_hom_apply, whiskerLeft_snd_assoc, CategoryTheory.CommGrp.trivial_grp_one, SSet.rightUnitor_inv_app_apply, CategoryTheory.Over.leftUnitor_inv_left_snd, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, associator_inv_snd_assoc, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_fst_assoc, CategoryTheory.MonObj.instIsMonHomLift, GrpCat.tensorObj_eq, CategoryTheory.Monoidal.rightUnitor_hom, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', CategoryTheory.bijection_symm_apply_id, CategoryTheory.Enriched.Functor.associator_hom_apply, CategoryTheory.Over.μ_pullback_left_fst_snd', SSet.ι₀_snd, rightUnitor_inv_fst, CategoryTheory.ChosenPullbacksAlong.Over.tensorUnit_left, CategoryTheory.sheafToPresheaf_δ, SSet.Truncated.Edge.CompStruct.tensor_simplex_fst, CategoryTheory.Grp.tensorUnit_X, Action.diagonalSuccIsoTensorTrivial_inv_hom_apply, CategoryTheory.Grp.whiskerLeft_hom, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_fst, CategoryTheory.Over.leftUnitor_inv_left_snd_assoc, CategoryTheory.Functor.chosenProd_obj, rightUnitor_inv_snd_assoc, CategoryTheory.CatEnrichedOrdinary.Hom.id_eq, CategoryTheory.Mon_Class.mul_eq_mul, SSet.Truncated.Edge.map_associator_hom, CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom, CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory, CategoryTheory.SimplicialThickening.functor_map, CategoryTheory.Grp.leftUnitor_inv_hom_hom, CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_map, CategoryTheory.Equivalence.mapCommGrp_unitIso, CategoryTheory.GrpObj.one_inv, CategoryTheory.GrpObj.mulRight_one, CategoryTheory.yonedaMon_map_app, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app, leftUnitor_inv_snd_assoc, inv_prodComparison_map_fst_assoc, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, CategoryTheory.Enriched.Functor.whiskerRight_app_apply, prodComparison_comp, SSet.ι₁_snd_assoc, CategoryTheory.Functor.OplaxMonoidal.instIsIsoη, CategoryTheory.Over.associator_hom_left_snd_fst, CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app, CategoryTheory.GrpObj.tensorObj.inv_def, CategoryTheory.MonObj.instIsMonHomFst, ModuleCat.free_ε_one, CategoryTheory.Grp.rightUnitor_inv_hom, CategoryTheory.Functor.Monoidal.toUnit_ε, CategoryTheory.Functor.Monoidal.whiskerRight_app_fst, inv_prodComparison_map_snd_assoc, SSet.instHasDimensionLETensorObjHAddNat, map_toUnit_comp_terminalComparison, SSet.ι₁_app_fst, SSet.ι₁_snd, CategoryTheory.Over.rightUnitor_inv_left_snd_assoc, CategoryTheory.Over.toOverSectionsAdj_counit_app, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_snd, CategoryTheory.CommGrp.instFaithfulCommMonForget₂CommMon, CategoryTheory.Monoidal.associator_hom, Rep.linearization_η_hom_apply, CategoryTheory.CommGrp.hom_ext_iff, CategoryTheory.associator_inv_apply_1_2, CategoryTheory.Grp.forget₂Mon_obj_mul, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor, prodComparisonNatTrans_comp, prodComparison_natural_whiskerRight, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_snd_assoc, CategoryTheory.Mon_Class.one_eq_one, CategoryTheory.Grp.Hom.hom_pow, lift_lift_associator_hom, CategoryTheory.Grp.δ_def, SSet.whiskerLeft_app_apply, CategoryTheory.GrpObj.whiskerLeft_η_commutator, CategoryTheory.Grp.associator_hom_hom_hom, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_fst_assoc, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv, CategoryTheory.isoCartesianComon_hom_hom, ModuleCat.FreeMonoidal.εIso_inv_freeMk, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, CategoryTheory.Grp.toMon_X, CategoryTheory.frobeniusMorphism_iso_of_preserves_binary_products, CategoryTheory.instIsMonHomInvOfIsCommMonObj, CategoryTheory.Grp.braiding_inv_hom, CategoryTheory.Monoidal.whiskerLeft_snd, CategoryTheory.Over.sections_obj, CategoryTheory.Grp.mkIso'_hom_hom_hom, CategoryTheory.GrpObj.lift_inv_left_eq, CategoryTheory.Functor.comp_mapCommGrp_mul, SSet.Subcomplex.prod_obj, prodComparisonNatIso_hom, CommAlgCat.snd_unop_hom, CategoryTheory.Grp.id_hom, CategoryTheory.Functor.Monoidal.tensorObjComp_inv_app, tensorδ_fst_assoc, SSet.Truncated.Edge.map_whiskerLeft, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, AddCommGrpCat.μ_forget_apply, Action.leftRegularTensorIso_hom_hom, CategoryTheory.CatEnrichedOrdinary.Hom.base_comp, CategoryTheory.equivToOverUnit_counitIso, SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse, ModuleCat.free_η_freeMk, CategoryTheory.Over.tensorHom_left, SSet.Truncated.Edge.map_snd, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, CategoryTheory.Grp.fst_hom, associator_hom_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse, CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply, CategoryTheory.isCommMonObj_iff_isMulCommutative, CategoryTheory.Functor.chosenProd_map, CategoryTheory.Over.associator_inv_left_fst_snd, CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom, lift_whiskerLeft, LightCondensed.free_internallyProjective_iff_tensor_condition', SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, AddCommGrpCat.tensorObj_eq, associator_inv_fst_snd_assoc, lift_fst_snd, CategoryTheory.Equivalence.mapGrp_unitIso, prodComparison_natural_whiskerRight_assoc, CategoryTheory.toOverPullbackIsoToOver_hom_app_left, SSet.instHasDimensionLTTensorObjHAddNat, CategoryTheory.Mon.instIsCommMonObj, CategoryTheory.Over.associator_hom_left_snd_snd_assoc, CategoryTheory.Grp.tensorUnit_one, CategoryTheory.Mon.Hom.hom_mul, prodComparisonNatTrans_id, CategoryTheory.Functor.Monoidal.whiskerRight_app_snd_assoc, braiding_inv_snd, terminalComparison_isIso_of_preservesLimits, tensorHom_snd, CategoryTheory.Over.μ_pullback_left_fst_fst', CategoryTheory.instIsMonHomInvHomOfIsCommMonObj, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_obj, CategoryTheory.Over.μ_pullback_left_fst_snd, CategoryTheory.Over.whiskerRight_left, CategoryTheory.Functor.EssImageSubcategory.toUnit_def, CategoryTheory.Over.monObjMkPullbackSnd_one, CategoryTheory.CommGrp.forget₂Grp_obj_one, CategoryTheory.GrpObj.whiskerLeft_η_commutator_assoc, ModuleCat.free_μ_freeMk_tmul_freeMk, CategoryTheory.GrpObj.isPullback, CategoryTheory.uncurry_expComparison, AddGrpCat.μ_forget_apply, prodComparison_inv_natural_whiskerLeft, CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply, whiskerLeft_toUnit_comp_rightUnitor_hom_assoc, CategoryTheory.toOverIsoToOverUnit_hom_app_left, whiskerLeft_snd, CommGrpCat.tensorObj_eq, ModuleCat.FreeMonoidal.μIso_hom_freeMk_tmul_freeMk, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_map, CategoryTheory.Cat.ihom_map, SSet.prodStdSimplex.objEquiv_map_apply, associator_inv_fst_fst_assoc, prodComparisonNatIso_inv, CategoryTheory.types_tensorObj_def, whiskerRight_toUnit_comp_leftUnitor_hom, CategoryTheory.Functor.mapCommGrp_id_one, CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_fst_assoc, AlgebraicGeometry.Scheme.monObjAsOverPullback_mul, lift_braiding_hom_assoc, CategoryTheory.Functor.Monoidal.tensorHom_app_fst, SSet.Truncated.Edge.map_tensorHom, lift_snd, CategoryTheory.associator_hom_apply, CategoryTheory.Over.associator_inv_left_fst_fst, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, CategoryTheory.SimplicialThickening.SimplicialCategory.assoc, CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd, CategoryTheory.Functor.mapGrp_map_hom_hom, CategoryTheory.SemilatticeInf.tensorUnit, preservesTerminalIso_hom, CategoryTheory.Functor.Monoidal.μ_comp, CategoryTheory.CommGrp.forget₂Grp_map_hom, CategoryTheory.Over.snd_left, CategoryTheory.Monoidal.tensorUnit, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_fst_assoc, CategoryTheory.Grp.comp_hom_hom, CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app, CategoryTheory.GrpObj.toMon_Class_injective, CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoδ, lift_snd_assoc, CategoryTheory.CommGrp.forget₂CommMon_obj_mul, CategoryTheory.Over.tensorHom_left_fst, associator_hom_snd_snd, CategoryTheory.CatEnrichedOrdinary.Hom.comp_eq, CategoryTheory.Grp.braiding_inv_hom_hom, CategoryTheory.Over.whiskerRight_left_snd, braiding_hom_fst_assoc, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app, CategoryTheory.GrpObj.eq_lift_inv_right, SSet.prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_snd_assoc, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_snd, CategoryTheory.Functor.Monoidal.μ_fst, preservesTerminalIso_comp, CategoryTheory.MonObj.ofRepresentableBy_mul, braiding_inv_fst, CommAlgCat.toUnit_unop_hom, SSet.Subcomplex.prod_monotone, SSet.ι₀_comp_assoc, CategoryTheory.Functor.Monoidal.tensorHom_app_snd, CategoryTheory.CatEnriched.comp_eq, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_fst, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val, CategoryTheory.GrpObj.left_inv, CategoryTheory.Functor.OplaxMonoidal.δ_fst, CategoryTheory.Grp.tensorObj_X, SSet.ι₀_comp, CategoryTheory.Over.tensorHom_left_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_snd_assoc, rightUnitor_inv_snd, CategoryTheory.forgetAdjToOver.homEquiv_symm, CategoryTheory.Functor.Monoidal.ε_of_cartesianMonoidalCategory, CategoryTheory.Grp.Hom.hom_mul, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_hom_left, CategoryTheory.Mon.Hom.hom_pow, CategoryTheory.GrpObj.mul_inv_rev_assoc, prodComparison_inv_natural_whiskerRight_assoc, comp_lift_assoc, CategoryTheory.ε_def, CategoryTheory.Over.η_pullback_left, CategoryTheory.CommGrpObj.toIsCommMonObj, CategoryTheory.Grp.tensorObj_mul, CategoryTheory.Grp.rightUnitor_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_hom_left, CategoryTheory.Grp.forget₂Mon_obj_X, CategoryTheory.Grp.hom_ext_iff, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_obj, SSet.RelativeMorphism.Homotopy.h₁_assoc, CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst, CategoryTheory.Over.whiskerLeft_left_fst, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app, CategoryTheory.expComparison_ev, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, inv_prodComparison_map_snd, CategoryTheory.Functor.Monoidal.snd_app, CategoryTheory.CatEnrichedOrdinary.homEquiv_comp, CategoryTheory.Functor.Monoidal.fst_app, SSet.RelativeMorphism.Homotopy.ofEq_h, CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app, instNonemptyBraidedCategory, prodComparison_inv_natural, fullSubcategory_leftUnitor_hom_hom, CategoryTheory.GrpObj.tensorHom_inv_inv_mul, leftUnitor_inv_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.lift_left, SSet.rightUnitor_hom_app_apply, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv_assoc, lift_whiskerRight_assoc, CategoryTheory.Grp.forget₂Mon_comp_forget, CategoryTheory.associator_hom_apply_2_2, hom_ext_iff, SSet.Truncated.tensor_map_apply_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj, CategoryTheory.Over.whiskerLeft_left_fst_assoc, CategoryTheory.GrpObj.mul_inv, CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage, inv_prodComparison_map_fst, ModuleCat.free_δ_freeMk, SSet.ι₁_fst, CategoryTheory.zeroMul_inv, CategoryTheory.Grp.tensorObj_one, CategoryTheory.Functor.Monoidal.tensorObj_obj, SSet.Truncated.Edge.tensor_edge, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_fst, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_obj, CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_obj, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', CategoryTheory.Over.whiskerLeft_left_snd_assoc, CategoryTheory.Functor.Monoidal.tensorHom_app_snd_assoc, prodComparisonIso_comp, CategoryTheory.Functor.Monoidal.associator_inv_app, CategoryTheory.GrpObj.inv_def, lift_comp_fst_snd, lift_whiskerRight, CategoryTheory.Grp.leftUnitor_inv_hom, mono_lift_of_mono_right, SSet.Truncated.HomotopyCategory.BinaryProduct.square, CategoryTheory.Over.leftUnitor_inv_left_fst_assoc, prodComparisonBifunctorNatTrans_app, CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left, CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso, CategoryTheory.Functor.mapGrp_obj_grp_mul, CategoryTheory.Functor.mapCommpGrp_id_mul, CategoryTheory.CommGrp.forget₂CommMon_obj_one, CategoryTheory.sheafToPresheaf_η, ModuleCat.FreeMonoidal.μIso_inv_freeMk, Rep.linearization_δ_hom, CategoryTheory.equivToOverUnit_inverse, prodComparison_fst_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app, CategoryTheory.GrpObj.mul_inv_rev, CategoryTheory.GrpObj.mulRight_hom, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app, fullSubcategory_associator_hom_hom, CategoryTheory.Preadditive.mul_def, CategoryTheory.Grp.trivial_grp_one, CategoryTheory.Grp.snd_hom_hom, CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom, CategoryTheory.GrpObj.lift_comp_inv_left_assoc, CategoryTheory.Functor.comp_mapCommGrp_one, CategoryTheory.Over.associator_inv_left_fst_snd_assoc, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app, SSet.RelativeMorphism.Homotopy.h₀, CategoryTheory.Grp.hom_one, CategoryTheory.Grp.forget₂Mon_obj_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Over.rightUnitor_hom_left, CategoryTheory.Mod_.trivialAction_X, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.CatEnriched.id_eq, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val, CategoryTheory.toOver_map_left, CategoryTheory.Over.sections_map, lift_fst, SSet.RelativeMorphism.Homotopy.precomp_h, prodComparisonIso_id, CategoryTheory.Hom.one_def, CategoryTheory.Over.μ_pullback_left_snd, CategoryTheory.Grp.associator_inv_hom, SSet.ι₀_fst, leftUnitor_inv_fst, CategoryTheory.Grp.homMk_hom_hom, CategoryTheory.ChosenPullbacksAlong.Over.toUnit_left, CategoryTheory.Functor.Monoidal.μ_snd, CategoryTheory.Monoidal.whiskerRight_snd, CategoryTheory.Functor.FullyFaithful.grpObj_mul, SSet.associator_hom_app_apply, lift_leftUnitor_hom, CategoryTheory.GrpObj.mulRight_inv, CategoryTheory.symmetricOfHasFiniteProducts_braiding_inv, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity, CategoryTheory.sheafToPresheaf_ε, CategoryTheory.GrpObj.mul_inv_assoc, whiskerLeft_fst, CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom, CategoryTheory.Functor.Monoidal.μ_snd_assoc, CategoryTheory.Mon.hom_mul, CategoryTheory.Over.braiding_hom_left, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_snd, SSet.RelativeMorphism.Homotopy.h₁, CategoryTheory.Functor.Monoidal.whiskerRight_app_snd, CategoryTheory.GrpObj.η_whiskerRight_commutator, SSet.Subcomplex.range_tensorHom, lift_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_snd, CategoryTheory.Functor.homMonoidHom_apply, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_snd, CategoryTheory.whiskerLeft_apply, lift_lift_associator_hom_assoc, CategoryTheory.Over.μ_pullback_left_fst_fst, SSet.RelativeMorphism.Homotopy.postcomp_h, mono_lift_of_mono_left, fullSubcategory_whiskerRight_hom, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, CategoryTheory.ExponentialIdeal.exp_closed, CategoryTheory.GrpObj.right_inv, CategoryTheory.GrpObj.lift_comp_inv_left, CategoryTheory.Over.tensorUnit_left, CategoryTheory.GrpObj.eq_lift_inv_left, CategoryTheory.Grp.Hom.hom_inv, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, Action.diagonalSuccIsoTensorDiagonal_hom_hom, CategoryTheory.Equivalence.mapCommGrp_counitIso, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, lift_snd_comp_fst_comp_assoc, lift_map, CategoryTheory.MonObj.lift_comp_one_left_assoc, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, Action.diagonalSuccIsoTensorTrivial_hom_hom_apply, CategoryTheory.Grp.instFaithfulMonForget₂Mon, CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, CategoryTheory.Monoidal.associator_inv, CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso, CategoryTheory.Monoidal.rightUnitor_inv, CategoryTheory.Monoidal.whiskerLeft, CategoryTheory.Functor.Monoidal.associator_hom_app, prodComparison_inv_natural_whiskerRight, CategoryTheory.Grp.braiding_hom_hom, CategoryTheory.Over.whiskerRight_left_fst_assoc, SSet.RelativeMorphism.Homotopy.rel, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, lift_map_assoc, CategoryTheory.monoidalOfHasFiniteProducts.η_eq, CategoryTheory.Over.tensorHom_left_snd, CategoryTheory.Grp.η_def, SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app, CategoryTheory.equivToOverUnit_functor, CategoryTheory.Functor.FullyFaithful.grpObj_one, lift_fst_comp_snd_comp, SSet.Truncated.Edge.map_whiskerRight, ModuleCat.FreeMonoidal.εIso_hom_one, CategoryTheory.CommGrp.trivial_grp_mul, CategoryTheory.Grp.associator_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, SSet.RelativeMorphism.Homotopy.refl_h, braiding_inv_snd_assoc, CategoryTheory.associator_hom_apply_2_1, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.Monoidal.tensorObj, CategoryTheory.Preadditive.one_def, CategoryTheory.Over.lift_left, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map, fullSubcategory_tensorProductIsBinaryProduct_lift_hom, whiskerRight_fst, preservesTerminalIso_id, CategoryTheory.whiskerRight_apply, CategoryTheory.instIsLeftAdjointTensorLeft, lift_snd_comp_fst_comp, CategoryTheory.CommGrp.trivial_grp_inv, CategoryTheory.SimplicialThickening.functor_id, CategoryTheory.GrpObj.ofIso_mul, CategoryTheory.Functor.Monoidal.leftUnitor_hom_app, AlgebraicGeometry.Scheme.monObjAsOverPullback_one, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_map, CategoryTheory.GrpObj.lift_comp_inv_right, CategoryTheory.Functor.Monoidal.lift_μ, prodComparison_inv_natural_whiskerLeft_assoc, CategoryTheory.yonedaGrp_map_app, CategoryTheory.Functor.Monoidal.leftUnitor_inv_app, SSet.hasDimensionLE_prod, SSet.ι₁_fst_assoc, CategoryTheory.Monoidal.whiskerLeft_fst, CategoryTheory.MonObj.one_eq_one, CategoryTheory.ChosenPullbacksAlong.Over.fst_eq_fst', SSet.Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse, rightUnitor_inv_fst_assoc, CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom, CategoryTheory.braiding_inv_apply, homEquivToProd_apply, CategoryTheory.Functor.Monoidal.rightUnitor_hom_app, CategoryTheory.Grp.whiskerRight_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, CategoryTheory.Over.fst_left, CategoryTheory.Over.associator_hom_left_fst_assoc, fullSubcategory_whiskerLeft_hom, SSet.leftUnitor_hom_app_apply, CategoryTheory.rightUnitor_inv_apply, CategoryTheory.Over.isMonHom_pullbackFst_id_right, CategoryTheory.Functor.OplaxMonoidal.lift_δ_assoc, CategoryTheory.Grp.tensorHom_hom, CategoryTheory.GrpObj.toMonObj_injective, tensorμ_fst, CategoryTheory.GrpObj.ofIso_one, CategoryTheory.Grp.Hom.hom_one, CategoryTheory.Functor.Braided.instSubsingleton, CategoryTheory.Over.tensorObj_left, CategoryTheory.Grp.fst_hom_hom, lift_snd_fst, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd', CategoryTheory.toOverUnitPullback_hom_app_left, CategoryTheory.Functor.EssImageSubcategory.lift_def, CategoryTheory.Mod_.trivialAction_mod_smul, CategoryTheory.Grp.mkIso'_inv_hom_hom, CategoryTheory.Over.ε_pullback_left, lift_rightUnitor_hom, CategoryTheory.isoCartesianComon_inv_hom, SSet.associator_inv_app_apply, CategoryTheory.Grp.trivial_grp_mul, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, GrpCat.μ_forget_apply, CategoryTheory.Monoidal.leftUnitor_inv, whiskerRight_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_snd_assoc, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_fst_assoc, CategoryTheory.tensor_apply, CategoryTheory.Grp.trivial_X, CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, CategoryTheory.SimplicialThickening.functor_obj_as, prodComparisonBifunctorNatTrans_comp, prodComparisonNatTrans_app, braiding_hom_snd, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj, CategoryTheory.Over.associator_hom_left_snd_snd, CategoryTheory.Grp.braiding_hom_hom_hom, CategoryTheory.Over.associator_inv_left_snd_assoc, CategoryTheory.CommGrp.forget₂CommMon_comp_forget, CategoryTheory.GrpObj.right_inv_assoc, CategoryTheory.comonEquiv_inverse, CategoryTheory.toOverUnitPullback_inv_app_left, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_fst, CategoryTheory.CatEnrichedOrdinary.homEquiv_id, Rep.linearization_ε_hom, CategoryTheory.SimplicialThickening.SimplicialCategory.id_comp, AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed, CategoryTheory.MonObj.instIsMonHomMulOfIsCommMonObj, CategoryTheory.SimplicialThickening.functor_comp, CategoryTheory.Sheaf.tensorUnit_isSheaf, CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd_assoc, CategoryTheory.Functor.map_one, CategoryTheory.associator_inv_apply_2, whiskerLeft_fst_assoc, CategoryTheory.Monoidal.leftUnitor_hom, rightUnitor_hom, CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom, fullSubcategory_tensorHom_hom, CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoη, CategoryTheory.Mon.hom_one, CategoryTheory.Over.whiskerLeft_left_snd, CategoryTheory.yonedaMon_obj, CategoryTheory.toOver_map, CategoryTheory.rightUnitor_hom_apply, CategoryTheory.Functor.Monoidal.instSubsingleton, homEquivToProd_symm_apply, lift_whiskerLeft_assoc, SSet.ι₀_app_fst, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_fst_assoc, CategoryTheory.forgetAdjToOver_counit_app, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_snd, prodComparison_inv_natural_assoc, tensorδ_fst, CategoryTheory.toUnit_comp_curryRightUnitorHom, CategoryTheory.MonObj.mul_eq_mul, CategoryTheory.Grp.comp_hom, CategoryTheory.Grp.instFullMonForget₂Mon, tensorHom_fst_assoc, CategoryTheory.Grp.id_hom_hom, CategoryTheory.Adjunction.mapCommGrp_counit, CategoryTheory.associator_inv_apply_1_1, CategoryTheory.GrpObj.lift_inv_comp_right_assoc, CategoryTheory.Over.tensorObj_hom, tensorμ_snd_assoc, SSet.ι₁_comp_assoc, isIso_prodComparison_of_preservesLimit_pair, CategoryTheory.toOverUnit_obj_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_inv, prodComparison_natural_whiskerLeft, CategoryTheory.Adjunction.mapGrp_counit, CategoryTheory.Functor.comp_mapGrp_one, CategoryTheory.SemilatticeInf.tensorObj, CategoryTheory.Mon.snd_hom, CategoryTheory.Mon.Hom.hom_one, CategoryTheory.Functor.OplaxMonoidal.instIsIsoδ, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_fst_assoc, CategoryTheory.CommGrp.forget_map, CategoryTheory.comonEquiv_counitIso, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_snd_assoc, Rep.linearization_μ_hom, CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map, fullSubcategory_rightUnitor_inv_hom, CategoryTheory.CatEnrichedOrdinary.Hom.base_id, SSet.RelativeMorphism.Homotopy.rel_assoc, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left, leftUnitor_hom, lift_braiding_inv_assoc, whiskerRight_snd, whiskerRight_toUnit_comp_leftUnitor_hom_assoc
toSymmetricCategory 📖	CompOp	1 math math: CategoryTheory.Mon.instIsCommMonObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.Limits.IsTerminal.comp_from
associator_hom_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_fst
associator_hom_snd_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Category.assoc whiskerLeft_snd whiskerLeft_snd_assoc
associator_hom_snd_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_snd_fst
associator_hom_snd_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.SemiCartesianMonoidalCategory.snd_def CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.Category.assoc CategoryTheory.Limits.IsTerminal.comp_from CategoryTheory.Iso.hom_inv_id_assoc
associator_hom_snd_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_snd_snd
associator_inv_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.Limits.IsTerminal.comp_from CategoryTheory.Iso.inv_hom_id_assoc
associator_inv_fst_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_fst_fst
associator_inv_fst_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Category.assoc whiskerLeft_snd whiskerLeft_snd_assoc CategoryTheory.Iso.inv_hom_id_assoc
associator_inv_fst_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_fst_snd
associator_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.SemiCartesianMonoidalCategory.snd_def CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.Category.assoc CategoryTheory.Limits.IsTerminal.comp_from
associator_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_snd
braiding_hom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.braiding_tensorUnit_left CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.SemiCartesianMonoidalCategory.snd_def
braiding_hom_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' braiding_hom_fst
braiding_hom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.SemiCartesianMonoidalCategory.snd_def CategoryTheory.braiding_tensorUnit_right CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.SemiCartesianMonoidalCategory.fst_def
braiding_hom_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' braiding_hom_snd
braiding_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.braiding_inv_tensorUnit_right CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.SemiCartesianMonoidalCategory.snd_def
braiding_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' braiding_inv_fst
braiding_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.SemiCartesianMonoidalCategory.snd_def CategoryTheory.braiding_inv_tensorUnit_left CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.SemiCartesianMonoidalCategory.fst_def
braiding_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' braiding_inv_snd
comp_lift 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift	—	hom_ext CategoryTheory.Category.assoc lift_fst lift_snd
comp_lift_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_lift
fullSubcategory_associator_hom_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategoryStruct.associator fullSubcategory	—	—
fullSubcategory_associator_inv_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategoryStruct.associator fullSubcategory	—	—
fullSubcategory_fst_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.fullSubcategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.fst fullSubcategory	—	—
fullSubcategory_isTerminalTensorUnit_lift_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.empty CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.fullSubcategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Limits.IsLimit.lift CategoryTheory.Limits.asEmptyCone CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit fullSubcategory CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	—
fullSubcategory_leftUnitor_hom_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategoryStruct.leftUnitor fullSubcategory	—	—
fullSubcategory_leftUnitor_inv_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategoryStruct.leftUnitor fullSubcategory	—	—
fullSubcategory_rightUnitor_hom_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategoryStruct.rightUnitor fullSubcategory	—	—
fullSubcategory_rightUnitor_inv_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategoryStruct.rightUnitor fullSubcategory	—	—
fullSubcategory_snd_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.fullSubcategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.snd fullSubcategory	—	—
fullSubcategory_tensorHom_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ObjectProperty.FullSubcategory.category fullSubcategory	—	—
fullSubcategory_tensorObj_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory fullSubcategory	—	—
fullSubcategory_tensorProductIsBinaryProduct_lift_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Limits.pair CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.fullSubcategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.ObjectProperty.homMk CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Limits.IsLimit.lift tensorProductIsBinaryProduct fullSubcategory lift CategoryTheory.Limits.BinaryFan.fst CategoryTheory.Limits.BinaryFan.snd	—	—
fullSubcategory_tensorUnit_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory fullSubcategory	—	—
fullSubcategory_whiskerLeft_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.ObjectProperty.FullSubcategory.category fullSubcategory	—	—
fullSubcategory_whiskerRight_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ObjectProperty.FullSubcategory.category fullSubcategory	—	—
homEquivToProd_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory EquivLike.toFunLike Equiv.instEquivLike homEquivToProd CategoryTheory.CategoryStruct.comp CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—
homEquivToProd_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquivToProd lift	—	—
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—	CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	hom_ext
instHasFiniteProducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteProducts	—	CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair CategoryTheory.Limits.hasTerminal_of_unique Unique.instSubsingleton
instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparison	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft prodComparisonBifunctorNatTrans	—	CategoryTheory.NatIso.isIso_of_isIso_app CategoryTheory.NatIso.isIso_app_of_isIso instIsIsoFunctorProdComparisonNatTransOfProdComparison
instIsIsoFunctorProdComparisonNatTransOfProdComparison 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparison	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.curriedTensor prodComparisonNatTrans	—	CategoryTheory.NatIso.isIso_of_isIso_app
instNonemptyBraidedCategory 📖	mathematical	—	CategoryTheory.BraidedCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory	—	—
instSubsingletonBraidedCategory 📖	mathematical	—	CategoryTheory.BraidedCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory	—	CategoryTheory.Iso.ext hom_ext braiding_hom_fst braiding_hom_snd
instSubsingletonSymmetricCategory 📖	mathematical	—	CategoryTheory.SymmetricCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory	—	instSubsingletonBraidedCategory
inv_prodComparison_map_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.fst	—	prodComparison_fst
inv_prodComparison_map_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_prodComparison_map_fst
inv_prodComparison_map_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.snd	—	prodComparison_snd
inv_prodComparison_map_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_prodComparison_map_snd
isIso_prodComparison_of_preservesLimit_pair 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparison	—	prodComparisonIso_hom CategoryTheory.Iso.isIso_hom
leftUnitor_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.SemiCartesianMonoidalCategory.snd_def CategoryTheory.Limits.IsTerminal.from_self CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp
leftUnitor_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
leftUnitor_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_inv_fst
leftUnitor_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.CategoryStruct.id	—	CategoryTheory.SemiCartesianMonoidalCategory.snd_def CategoryTheory.Limits.IsTerminal.from_self CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id
leftUnitor_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_inv_snd
lift_braiding_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	hom_ext CategoryTheory.Category.assoc braiding_hom_fst lift_snd lift_fst braiding_hom_snd
lift_braiding_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_braiding_hom
lift_braiding_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding	—	hom_ext CategoryTheory.Category.assoc braiding_inv_fst lift_snd lift_fst braiding_inv_snd
lift_braiding_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_braiding_inv
lift_comp_fst_snd 📖	mathematical	—	lift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	hom_ext lift_fst lift_snd
lift_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.SemiCartesianMonoidalCategory.fst	—	—
lift_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fst
lift_fst_comp_snd_comp 📖	mathematical	—	lift CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.MonoidalCategoryStruct.tensorHom	—	hom_ext lift_fst tensorHom_fst lift_snd tensorHom_snd
lift_fst_snd 📖	mathematical	—	lift CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	hom_ext lift_fst CategoryTheory.Category.id_comp lift_snd
lift_leftUnitor_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit lift CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.Iso.eq_comp_inv hom_ext CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique lift_snd CategoryTheory.Category.assoc leftUnitor_inv_snd CategoryTheory.Category.comp_id
lift_leftUnitor_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit lift CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_leftUnitor_hom
lift_lift_associator_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	hom_ext CategoryTheory.Category.assoc associator_hom_fst lift_fst_assoc lift_fst associator_hom_snd_fst lift_snd associator_hom_snd_snd
lift_lift_associator_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_lift_associator_hom
lift_lift_associator_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	hom_ext CategoryTheory.Category.assoc associator_inv_fst_fst lift_fst associator_inv_fst_snd lift_snd_assoc lift_snd associator_inv_snd
lift_lift_associator_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_lift_associator_inv
lift_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.MonoidalCategoryStruct.tensorHom	—	hom_ext CategoryTheory.Category.assoc tensorHom_fst lift_fst_assoc lift_fst tensorHom_snd lift_snd_assoc lift_snd
lift_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_map
lift_rightUnitor_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit lift CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.Iso.eq_comp_inv hom_ext lift_fst CategoryTheory.Category.assoc rightUnitor_inv_fst CategoryTheory.Category.comp_id CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
lift_rightUnitor_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit lift CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_rightUnitor_hom
lift_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—
lift_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_snd
lift_snd_comp_fst_comp 📖	mathematical	—	lift CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.MonoidalCategoryStruct.tensorHom	—	hom_ext lift_fst CategoryTheory.Category.assoc tensorHom_fst braiding_hom_fst_assoc lift_snd tensorHom_snd braiding_hom_snd_assoc
lift_snd_comp_fst_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_snd_comp_fst_comp
lift_snd_fst 📖	mathematical	—	lift CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	hom_ext lift_fst braiding_hom_fst lift_snd braiding_hom_snd
lift_whiskerLeft 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	hom_ext CategoryTheory.Category.assoc whiskerLeft_fst lift_fst whiskerLeft_snd lift_snd_assoc lift_snd
lift_whiskerLeft_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_whiskerLeft
lift_whiskerRight 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	hom_ext CategoryTheory.Category.assoc whiskerRight_fst lift_fst_assoc lift_fst whiskerRight_snd lift_snd
lift_whiskerRight_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_whiskerRight
map_toUnit_comp_terminalComparison 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.toUnit terminalComparison	—	CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
map_toUnit_comp_terminalComparison_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.toUnit terminalComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_toUnit_comp_terminalComparison
mono_lift_of_mono_left 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift	—	CategoryTheory.mono_of_mono_fac lift_fst
mono_lift_of_mono_right 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory lift	—	CategoryTheory.mono_of_mono_fac lift_snd
preservesLimit_empty_of_isIso_terminalComparison 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
preservesLimit_pair_of_isIso_prodComparison 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Category.comp_id prodComparison_fst CategoryTheory.Category.id_comp prodComparison_snd
preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparison	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory	—	CategoryTheory.Limits.preservesLimit_of_iso_diagram preservesLimit_pair_of_isIso_prodComparison
preservesTerminalIso_comp 📖	mathematical	—	preservesTerminalIso CategoryTheory.Functor.comp CategoryTheory.Iso.trans CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.mapIso	—	CategoryTheory.Iso.ext CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
preservesTerminalIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory preservesTerminalIso terminalComparison	—	CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
preservesTerminalIso_id 📖	mathematical	—	preservesTerminalIso CategoryTheory.Functor.id CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.CreatesLimitsOfShape.CreatesLimit CategoryTheory.CreatesLimitsOfSize.CreatesLimitsOfShape CategoryTheory.idCreatesLimits CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete instHasFiniteProducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Functor.comp CategoryTheory.Iso.refl CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory	—	CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete instHasFiniteProducts Finite.of_fintype CategoryTheory.Iso.ext CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
prodComparisonBifunctorNatIso_hom 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft prodComparisonBifunctorNatIso prodComparisonBifunctorNatTrans	—	—
prodComparisonBifunctorNatIso_inv 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft prodComparisonBifunctorNatIso CategoryTheory.inv prodComparisonBifunctorNatTrans	—	—
prodComparisonBifunctorNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft prodComparisonBifunctorNatTrans prodComparisonNatTrans	—	—
prodComparisonBifunctorNatTrans_comp 📖	mathematical	—	prodComparisonBifunctorNatTrans CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.whiskerLeft	—	CategoryTheory.NatTrans.ext' prodComparison_comp
prodComparisonIso_comp 📖	mathematical	—	prodComparisonIso CategoryTheory.Functor.comp CategoryTheory.Iso.trans CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.mapIso	—	CategoryTheory.Iso.ext hom_ext lift_fst comp_lift CategoryTheory.Functor.map_comp lift_snd
prodComparisonIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparisonIso prodComparison	—	—
prodComparisonIso_id 📖	mathematical	—	prodComparisonIso CategoryTheory.Functor.id CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.CreatesLimitsOfShape.CreatesLimit CategoryTheory.CreatesLimitsOfSize.CreatesLimitsOfShape CategoryTheory.idCreatesLimits CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Functor.comp CategoryTheory.Iso.refl CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory	—	CategoryTheory.Iso.ext CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete instHasFiniteProducts Finite.of_fintype hom_ext prodComparison_id CategoryTheory.Category.id_comp
prodComparisonNatIso_hom 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparisonNatIso prodComparisonNatTrans	—	—
prodComparisonNatIso_inv 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparisonNatIso CategoryTheory.inv prodComparisonNatTrans	—	—
prodComparisonNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparisonNatTrans prodComparison	—	—
prodComparisonNatTrans_comp 📖	mathematical	—	prodComparisonNatTrans CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.whiskerLeft	—	CategoryTheory.NatTrans.ext' prodComparison_comp
prodComparisonNatTrans_id 📖	mathematical	—	prodComparisonNatTrans CategoryTheory.Functor.id CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.curriedTensor CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory	—	CategoryTheory.NatTrans.ext' prodComparison_id
prodComparison_comp 📖	mathematical	—	prodComparison CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.map	—	hom_ext lift_fst comp_lift CategoryTheory.Functor.map_comp lift_snd
prodComparison_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparison CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Functor.map	—	lift_fst
prodComparison_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparison CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' prodComparison_fst
prodComparison_id 📖	mathematical	—	prodComparison CategoryTheory.Functor.id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory	—	lift_fst_snd
prodComparison_inv_natural 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.IsIso.eq_comp_inv CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_comp_eq prodComparison_natural
prodComparison_inv_natural_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' prodComparison_inv_natural
prodComparison_inv_natural_whiskerLeft 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.IsIso.eq_comp_inv CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_comp_eq prodComparison_natural_whiskerLeft
prodComparison_inv_natural_whiskerLeft_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' prodComparison_inv_natural_whiskerLeft
prodComparison_inv_natural_whiskerRight 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.IsIso.eq_comp_inv CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_comp_eq prodComparison_natural_whiskerRight
prodComparison_inv_natural_whiskerRight_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.inv prodComparison CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' prodComparison_inv_natural_whiskerRight
prodComparison_natural 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorHom prodComparison	—	hom_ext CategoryTheory.Category.assoc prodComparison_fst CategoryTheory.Functor.map_comp tensorHom_fst prodComparison_fst_assoc prodComparison_snd tensorHom_snd prodComparison_snd_assoc
prodComparison_natural_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorHom prodComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' prodComparison_natural
prodComparison_natural_whiskerLeft 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft prodComparison	—	hom_ext CategoryTheory.Category.assoc prodComparison_fst whiskerLeft_fst prodComparison_snd whiskerLeft_snd prodComparison_snd_assoc
prodComparison_natural_whiskerLeft_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft prodComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' prodComparison_natural_whiskerLeft
prodComparison_natural_whiskerRight 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight prodComparison	—	hom_ext CategoryTheory.Category.assoc prodComparison_fst whiskerRight_fst prodComparison_fst_assoc prodComparison_snd whiskerRight_snd
prodComparison_natural_whiskerRight_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight prodComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' prodComparison_natural_whiskerRight
prodComparison_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparison CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Functor.map	—	lift_snd
prodComparison_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory prodComparison CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' prodComparison_snd
rightUnitor_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.Limits.IsTerminal.from_self CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp
rightUnitor_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.CategoryStruct.id	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.Limits.IsTerminal.from_self CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id
rightUnitor_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_inv_fst
rightUnitor_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
rightUnitor_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_inv_snd
tensorHom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.Category.assoc whiskerLeft_fst whiskerRight_fst
tensorHom_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorHom_fst
tensorHom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.Category.assoc whiskerLeft_snd whiskerRight_snd_assoc
tensorHom_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorHom_snd
tensorδ_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.tensorδ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.MonoidalCategoryStruct.tensorHom	—	hom_ext CategoryTheory.Category.assoc associator_inv_fst_fst whiskerLeft_fst associator_hom_fst tensorHom_fst associator_inv_fst_snd whiskerLeft_snd_assoc whiskerRight_fst_assoc braiding_inv_fst associator_hom_snd_snd_assoc tensorHom_snd
tensorδ_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.tensorδ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorδ_fst
tensorδ_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.tensorδ CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.MonoidalCategoryStruct.tensorHom	—	hom_ext CategoryTheory.Category.assoc associator_inv_snd whiskerLeft_snd_assoc associator_hom_snd_fst whiskerRight_fst_assoc braiding_inv_snd associator_inv_fst_fst tensorHom_fst associator_hom_snd_snd whiskerRight_snd associator_hom_snd_snd_assoc tensorHom_snd
tensorδ_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.tensorδ CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorδ_snd
tensorμ_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.MonoidalCategoryStruct.tensorHom	—	hom_ext CategoryTheory.Category.assoc associator_inv_fst_fst whiskerLeft_fst associator_hom_fst tensorHom_fst associator_inv_fst_snd whiskerLeft_snd_assoc whiskerRight_fst_assoc braiding_hom_fst associator_hom_snd_snd_assoc tensorHom_snd
tensorμ_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorμ_fst
tensorμ_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.MonoidalCategoryStruct.tensorHom	—	hom_ext CategoryTheory.Category.assoc associator_inv_snd whiskerLeft_snd_assoc associator_hom_snd_fst whiskerRight_fst_assoc braiding_hom_snd associator_inv_fst_fst tensorHom_fst associator_hom_snd_snd whiskerRight_snd associator_hom_snd_snd_assoc tensorHom_snd
tensorμ_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorμ_snd
terminalComparison_isIso_of_preservesLimits 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory terminalComparison	—	preservesTerminalIso_hom CategoryTheory.Iso.isIso_hom
whiskerLeft_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.Limits.IsTerminal.comp_from
whiskerLeft_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_fst
whiskerLeft_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.SemiCartesianMonoidalCategory.snd_def CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.id_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
whiskerLeft_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_snd
whiskerLeft_toUnit_comp_rightUnitor_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id hom_ext whiskerLeft_fst rightUnitor_inv_fst CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
whiskerLeft_toUnit_comp_rightUnitor_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_toUnit_comp_rightUnitor_hom
whiskerRight_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.SemiCartesianMonoidalCategory.fst_def CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
whiskerRight_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_fst
whiskerRight_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.SemiCartesianMonoidalCategory.snd_def CategoryTheory.Limits.IsTerminal.comp_from
whiskerRight_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_snd
whiskerRight_toUnit_comp_leftUnitor_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id hom_ext CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique whiskerRight_snd leftUnitor_inv_snd
whiskerRight_toUnit_comp_leftUnitor_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_toUnit_comp_leftUnitor_hom

CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts

Definitions

Name	Category	Theorems
tensorHom 📖	CompOp	7 math math: id_tensorHom_id, associator_naturality, leftUnitor_naturality, triangle, pentagon, tensorHom_comp_tensorHom, rightUnitor_naturality
tensorObj 📖	CompOp	7 math math: id_tensorHom_id, associator_naturality, leftUnitor_naturality, triangle, pentagon, tensorHom_comp_tensorHom, rightUnitor_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct tensorObj CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.LimitCone.cone tensorHom CategoryTheory.Iso.hom CategoryTheory.Limits.BinaryFan.associatorOfLimitCone	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp CategoryTheory.Limits.IsLimit.fac_assoc CategoryTheory.Limits.IsLimit.fac CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp_assoc
id_tensorHom_id 📖	mathematical	—	tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct tensorObj	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Limits.IsLimit.fac CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
leftUnitor_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct tensorObj CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Limits.LimitCone.cone tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.BinaryFan.leftUnitor CategoryTheory.Limits.LimitCone.isLimit	—	CategoryTheory.Limits.IsLimit.fac
pentagon 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct tensorObj CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.LimitCone.cone tensorHom CategoryTheory.Iso.hom CategoryTheory.Limits.BinaryFan.associatorOfLimitCone CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.IsLimit.fac CategoryTheory.Category.comp_id CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp CategoryTheory.Limits.IsLimit.fac_assoc CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp_assoc
rightUnitor_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct tensorObj CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Limits.LimitCone.cone tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.BinaryFan.rightUnitor CategoryTheory.Limits.LimitCone.isLimit	—	CategoryTheory.Limits.IsLimit.fac
tensorHom_comp_tensorHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct tensorObj tensorHom	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.IsLimit.fac CategoryTheory.Limits.IsLimit.fac_assoc
triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Functor.empty CategoryTheory.Limits.LimitCone.cone tensorObj CategoryTheory.Iso.hom CategoryTheory.Limits.BinaryFan.associatorOfLimitCone tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Limits.BinaryFan.leftUnitor CategoryTheory.Limits.LimitCone.isLimit CategoryTheory.Limits.BinaryFan.rightUnitor	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.IsLimit.fac CategoryTheory.Category.comp_id CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp_assoc

CategoryTheory.Functor.Braided

Definitions

Name	Category	Theorems
ofChosenFiniteProducts 📖	CompOp	2 math math: CategoryTheory.Functor.mapCommGrpFunctor_obj, CategoryTheory.Functor.mapCommGrpFunctor_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingleton 📖	mathematical	—	CategoryTheory.Functor.Braided CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	Function.Injective.subsingleton toMonoidal_injective CategoryTheory.Functor.Monoidal.instSubsingleton

CategoryTheory.Functor.EssImageSubcategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_def 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.EssImageSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.essImage CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.fullSubcategory CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ObjectProperty.homMk CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts
associator_inv_def 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor.EssImageSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.essImage CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.fullSubcategory CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ObjectProperty.homMk CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts
lift_def 📖	mathematical	—	CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.Functor.EssImageSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.essImage CategoryTheory.CartesianMonoidalCategory.fullSubcategory CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.ObjectProperty.homMk CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts
tensor_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.essImage CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor.EssImageSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.fullSubcategory CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.fintypeWalkingPair	—	CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts
toUnit_def 📖	mathematical	—	CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.Functor.EssImageSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.essImage CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.fullSubcategory CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.ObjectProperty.homMk CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts

CategoryTheory.Functor.Monoidal

Definitions

Name	Category	Theorems
ofChosenFiniteProducts 📖	CompOp	2 math math: CategoryTheory.Functor.mapGrpFunctor_obj, CategoryTheory.Functor.mapGrpFunctor_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesFiniteProducts 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts	—	instIsIsoδ CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory instIsIsoη CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison CategoryTheory.CartesianMonoidalCategory.preservesLimit_empty_of_isIso_terminalComparison CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts
instSubsingleton 📖	mathematical	—	CategoryTheory.Functor.Monoidal CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	Function.Injective.subsingleton toOplaxMonoidal_injective CategoryTheory.Functor.OplaxMonoidal.instSubsingleton
lift_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc μ_δ CategoryTheory.Category.comp_id CategoryTheory.Functor.OplaxMonoidal.lift_δ
lift_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_μ
nonempty_monoidal_iff_preservesFiniteProducts 📖	mathematical	—	CategoryTheory.Functor.Monoidal CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Limits.PreservesFiniteProducts	—	instPreservesFiniteProducts
toUnit_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.map	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
toUnit_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.Functor.LaxMonoidal.ε toLaxMonoidal CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toUnit_ε
ε_of_cartesianMonoidalCategory 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toLaxMonoidal CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype Fintype.instPEmpty CategoryTheory.Functor.empty	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Iso.ext CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
μ_comp 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.comp toLaxMonoidal CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.CartesianMonoidalCategory.hom_ext μ_δ CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Functor.OplaxMonoidal.δ_fst μ_fst CategoryTheory.Functor.OplaxMonoidal.δ_snd μ_snd
μ_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.comp toLaxMonoidal CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_comp
μ_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_inv δ_μ_assoc CategoryTheory.Functor.OplaxMonoidal.δ_fst
μ_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_fst
μ_of_cartesianMonoidalCategory 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toLaxMonoidal CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CartesianMonoidalCategory.prodComparisonIso CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Iso.ext CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory
μ_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_inv δ_μ_assoc CategoryTheory.Functor.OplaxMonoidal.δ_snd
μ_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ toLaxMonoidal CategoryTheory.Functor.map CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_snd

CategoryTheory.Functor.OplaxMonoidal

Definitions

Name	Category	Theorems
ofChosenFiniteProducts 📖	CompOp	2 math math: CategoryTheory.Over.grpObjMkPullbackSnd_one, CategoryTheory.Over.grpObjMkPullbackSnd_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoδ 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory δ	—	CategoryTheory.CartesianMonoidalCategory.isIso_prodComparison_of_preservesLimit_pair CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype δ_of_cartesianMonoidalCategory
instIsIsoη 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory η	—	CategoryTheory.CartesianMonoidalCategory.terminalComparison_isIso_of_preservesLimits CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype η_of_cartesianMonoidalCategory
instSubsingleton 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	ext CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique δ_of_cartesianMonoidalCategory
lift_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.CartesianMonoidalCategory.lift δ	—	CategoryTheory.CartesianMonoidalCategory.hom_ext CategoryTheory.Category.assoc δ_fst CategoryTheory.CartesianMonoidalCategory.lift_fst δ_snd CategoryTheory.CartesianMonoidalCategory.lift_snd
lift_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.map CategoryTheory.CartesianMonoidalCategory.lift δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_δ
δ_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory δ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Functor.map	—	CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst δ_natural_right_assoc CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom
δ_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory δ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_fst
δ_of_cartesianMonoidalCategory 📖	mathematical	—	δ CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.prodComparison	—	CategoryTheory.CartesianMonoidalCategory.hom_ext δ_fst CategoryTheory.CartesianMonoidalCategory.prodComparison_fst δ_snd CategoryTheory.CartesianMonoidalCategory.prodComparison_snd
δ_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory δ CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Functor.map	—	CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd δ_natural_left_assoc CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom
δ_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory δ CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_snd
η_of_cartesianMonoidalCategory 📖	mathematical	—	η CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.terminalComparison	—	CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique

CategoryTheory.NatTrans.IsMonoidal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_cartesianMonoidalCategory 📖	mathematical	—	CategoryTheory.NatTrans.IsMonoidal CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.CartesianMonoidalCategory.hom_ext CategoryTheory.Category.assoc CategoryTheory.Functor.Monoidal.δ_μ_assoc CategoryTheory.Functor.OplaxMonoidal.δ_fst CategoryTheory.Functor.Monoidal.μ_δ CategoryTheory.Category.comp_id CategoryTheory.CartesianMonoidalCategory.tensorHom_fst CategoryTheory.Functor.OplaxMonoidal.δ_fst_assoc CategoryTheory.NatTrans.naturality CategoryTheory.Functor.OplaxMonoidal.δ_snd CategoryTheory.CartesianMonoidalCategory.tensorHom_snd CategoryTheory.Functor.OplaxMonoidal.δ_snd_assoc

CategoryTheory.SemiCartesianMonoidalCategory

Definitions

Name	Category	Theorems
fst 📖	CompOp	100 math math: CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_map, CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst_assoc, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst, CategoryTheory.CartesianMonoidalCategory.associator_hom_fst_assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst, CategoryTheory.Functor.Monoidal.tensorHom_app_fst_assoc, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst_assoc, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom, SSet.Truncated.Edge.map_fst, CategoryTheory.Functor.Monoidal.whiskerRight_app_fst_assoc, CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd_assoc, CategoryTheory.toOverPullbackIsoToOver_inv_app_left, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd, CategoryTheory.symmetricOfHasFiniteProducts_braiding_hom, CategoryTheory.CartesianMonoidalCategory.tensorμ_fst_assoc, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_fst_hom, CategoryTheory.Functor.OplaxMonoidal.δ_fst_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app, CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst_assoc, CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst, CategoryTheory.Functor.Monoidal.μ_fst_assoc, CategoryTheory.CartesianMonoidalCategory.tensorHom_fst, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst, SSet.ι₀_fst_assoc, CommAlgCat.fst_unop_hom, CategoryTheory.Mon.fst_hom, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst, CategoryTheory.Mon_Class.mul_eq_mul, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app, CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_fst_assoc, CategoryTheory.MonObj.instIsMonHomFst, CategoryTheory.Functor.Monoidal.whiskerRight_app_fst, CategoryTheory.CartesianMonoidalCategory.tensorδ_fst_assoc, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, CategoryTheory.Grp.fst_hom, CategoryTheory.CartesianMonoidalCategory.associator_hom_fst, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd_assoc, CategoryTheory.CartesianMonoidalCategory.lift_fst_snd, CategoryTheory.toOverPullbackIsoToOver_hom_app_left, CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom_assoc, CategoryTheory.toOverIsoToOverUnit_hom_app_left, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst_assoc, CategoryTheory.Functor.Monoidal.tensorHom_app_fst, CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst_assoc, CategoryTheory.Functor.Monoidal.μ_fst, CategoryTheory.MonObj.ofRepresentableBy_mul, CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst, CategoryTheory.Functor.OplaxMonoidal.δ_fst, CategoryTheory.forgetAdjToOver.homEquiv_symm, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_obj, CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app, CategoryTheory.Functor.Monoidal.fst_app, SSet.RelativeMorphism.Homotopy.ofEq_h, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst_assoc, CategoryTheory.CartesianMonoidalCategory.hom_ext_iff, CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_fst, SSet.ι₁_fst, CategoryTheory.CartesianMonoidalCategory.lift_comp_fst_snd, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst_assoc, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app, CategoryTheory.Preadditive.mul_def, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val, CategoryTheory.CartesianMonoidalCategory.lift_fst, SSet.ι₀_fst, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst, CategoryTheory.symmetricOfHasFiniteProducts_braiding_inv, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst, CategoryTheory.CartesianMonoidalCategory.lift_fst_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp_assoc, SSet.RelativeMorphism.Homotopy.rel, CategoryTheory.CartesianMonoidalCategory.lift_fst_comp_snd_comp, SSet.RelativeMorphism.Homotopy.refl_h, CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd_assoc, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom, CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst, CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp, fst_def, SSet.ι₁_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.fst_eq_fst', CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst_assoc, CategoryTheory.CartesianMonoidalCategory.homEquivToProd_apply, CategoryTheory.Over.fst_left, CategoryTheory.CartesianMonoidalCategory.tensorμ_fst, CategoryTheory.Grp.fst_hom_hom, CategoryTheory.CartesianMonoidalCategory.lift_snd_fst, CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst_assoc, CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst_assoc, CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom, CategoryTheory.forgetAdjToOver_counit_app, CategoryTheory.CartesianMonoidalCategory.tensorδ_fst, CategoryTheory.toUnit_comp_curryRightUnitorHom, CategoryTheory.MonObj.mul_eq_mul, CategoryTheory.CartesianMonoidalCategory.tensorHom_fst_assoc, SSet.RelativeMorphism.Homotopy.rel_assoc
instUniqueHomTensorUnit 📖	CompOp	1 math math: default_eq_toUnit
isTerminalTensorUnit 📖	CompOp	3 math math: CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, fst_def, snd_def
snd 📖	CompOp	98 math math: CategoryTheory.CartesianMonoidalCategory.prodComparison_snd, CategoryTheory.CartesianMonoidalCategory.tensorδ_snd, SSet.ι₀_snd_assoc, CategoryTheory.zeroMul_hom, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst_assoc, CategoryTheory.Functor.OplaxMonoidal.δ_snd_assoc, CategoryTheory.CartesianMonoidalCategory.tensorδ_snd_assoc, CategoryTheory.toOver_obj_hom, CategoryTheory.CartesianMonoidalCategory.associator_inv_snd, CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd_assoc, CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd_assoc, CategoryTheory.toOverPullbackIsoToOver_inv_app_left, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd, CategoryTheory.Functor.OplaxMonoidal.δ_snd, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_snd_hom, CategoryTheory.symmetricOfHasFiniteProducts_braiding_hom, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd_assoc, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app, CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst, CategoryTheory.MonObj.instIsMonHomSnd, CategoryTheory.ChosenPullbacksAlong.Over.snd_eq_snd', CategoryTheory.CartesianMonoidalCategory.tensorHom_snd_assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_snd_assoc, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val, CategoryTheory.CartesianMonoidalCategory.tensorμ_snd, CategoryTheory.Grp.snd_hom, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, CategoryTheory.CartesianMonoidalCategory.associator_inv_snd_assoc, SSet.ι₀_snd, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd_assoc, CategoryTheory.Mon_Class.mul_eq_mul, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd_assoc, SSet.ι₁_snd_assoc, CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_snd_assoc, SSet.ι₁_snd, CommAlgCat.snd_unop_hom, SSet.Truncated.Edge.map_snd, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd_assoc, CategoryTheory.CartesianMonoidalCategory.lift_fst_snd, CategoryTheory.Functor.Monoidal.whiskerRight_app_snd_assoc, CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd, CategoryTheory.CartesianMonoidalCategory.tensorHom_snd, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_obj, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_map, CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom, CategoryTheory.CartesianMonoidalCategory.lift_snd, CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd, CategoryTheory.Over.snd_left, CategoryTheory.CartesianMonoidalCategory.lift_snd_assoc, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd, CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst_assoc, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app, CategoryTheory.MonObj.ofRepresentableBy_mul, CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst, CategoryTheory.Functor.Monoidal.tensorHom_app_snd, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd, CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_snd, CategoryTheory.Functor.Monoidal.snd_app, CategoryTheory.CartesianMonoidalCategory.hom_ext_iff, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_obj, CategoryTheory.Functor.Monoidal.tensorHom_app_snd_assoc, CategoryTheory.CartesianMonoidalCategory.lift_comp_fst_snd, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app, CategoryTheory.Preadditive.mul_def, CategoryTheory.Grp.snd_hom_hom, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app, CategoryTheory.toOver_map_left, CategoryTheory.Functor.Monoidal.μ_snd, CategoryTheory.symmetricOfHasFiniteProducts_braiding_inv, CategoryTheory.Functor.Monoidal.μ_snd_assoc, CategoryTheory.Functor.Monoidal.whiskerRight_app_snd, CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp_assoc, CategoryTheory.CartesianMonoidalCategory.lift_fst_comp_snd_comp, CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd_assoc, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom, CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_map, CategoryTheory.CartesianMonoidalCategory.homEquivToProd_apply, CategoryTheory.CartesianMonoidalCategory.lift_snd_fst, CategoryTheory.Mod_.trivialAction_mod_smul, CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd, CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd_assoc, snd_def, CategoryTheory.MonObj.mul_eq_mul, CategoryTheory.CartesianMonoidalCategory.tensorμ_snd_assoc, CategoryTheory.Mon.snd_hom, CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom, CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd, CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom_assoc
toMonoidalCategory 📖	CompOp	845 math math: CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val, CategoryTheory.Grp.Hom.hom_div, CategoryTheory.Over.associator_hom_left_snd_fst_assoc, CategoryTheory.Grp.comp', CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor, CategoryTheory.Enriched.Functor.associator_inv_apply, CategoryTheory.GrpObj.lift_inv_comp_left, LightCondensed.free_internallyProjective_iff_tensor_condition, CategoryTheory.Over.μ_pullback_left_snd', CategoryTheory.Functor.natTransEquiv_apply_app, CategoryTheory.Grp.instIsIsoHomHomMon, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_fst_assoc, CategoryTheory.Functor.homObjEquiv_apply_app, CategoryTheory.Grp.homMk'_hom, CategoryTheory.CartesianMonoidalCategory.prodComparison_snd, CategoryTheory.CartesianMonoidalCategory.tensorδ_snd, CategoryTheory.CartesianCopyDiscard.instDeterministic, CategoryTheory.CommGrp.instFullCommMonForget₂CommMon, CategoryTheory.comonEquiv_unitIso, SSet.Truncated.tensor_map_apply_snd, Action.leftRegularTensorIso_inv_hom, CategoryTheory.Equivalence.mapGrp_counitIso, CategoryTheory.Functor.Monoidal.rightUnitor_inv_app, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_fst, AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral, CategoryTheory.Grp.Hom.hom_hom_zpow, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_map, CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst_assoc, CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, CategoryTheory.Over.associator_inv_left_snd, SSet.ι₀_snd_assoc, CategoryTheory.CommGrp.comm, CategoryTheory.instFullMonFunctorOppositeMonCatYonedaMon, CategoryTheory.SimplicialThickening.SimplicialCategory.comp_id, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst, CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app_app, CategoryTheory.Functor.map_mul, CategoryTheory.zeroMul_hom, CategoryTheory.CartesianMonoidalCategory.associator_hom_fst_assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst, CategoryTheory.Functor.mapCommGrp_obj_grp_one, CategoryTheory.Functor.Monoidal.tensorHom_app_fst_assoc, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst_assoc, CategoryTheory.Grp.id', CategoryTheory.Enriched.Functor.whiskerLeft_app_apply, CategoryTheory.GrpObj.lift_inv_right_eq, CategoryTheory.prodComparison_iso, SSet.iSup_subcomplexOfSimplex_prod_eq_top, CategoryTheory.Functor.FullyFaithful.mapGrp_preimage, CategoryTheory.Over.rightUnitor_inv_left_fst_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, CategoryTheory.Functor.OplaxMonoidal.δ_snd_assoc, CategoryTheory.CartesianMonoidalCategory.tensorδ_snd_assoc, CategoryTheory.counit_eq_toUnit, CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj_homEquiv, CategoryTheory.μ_def, CategoryTheory.GrpObj.lift_inv_comp_left_assoc, CategoryTheory.CartesianMonoidalCategory.lift_leftUnitor_hom_assoc, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, CategoryTheory.Functor.EssImageSubcategory.associator_inv_def, CategoryTheory.Grp.trivial_grp_inv, Action.diagonalSuccIsoTensorDiagonal_inv_hom, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_hom_hom, CategoryTheory.Over.monObjMkPullbackSnd_mul, CategoryTheory.Functor.comp_mapGrp_mul, CategoryTheory.Over.whiskerLeft_left, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom, SSet.instHasDimensionLETensorUnitOfNatNat, CategoryTheory.Grp.whiskerLeft_hom_hom, CategoryTheory.GrpObj.left_inv_assoc, CategoryTheory.Functor.mapGrp_id_mul, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_inv_hom, CategoryTheory.MonObj.instIsMonHomOne, SSet.tensorHom_app_apply, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, CategoryTheory.MonObj.instIsMonHomToUnit, CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, CategoryTheory.CartesianMonoidalCategory.instSubsingletonBraidedCategory, CategoryTheory.Over.grpObjMkPullbackSnd_one, CategoryTheory.CartesianMonoidalCategory.associator_inv_snd, CategoryTheory.Functor.EssImageSubcategory.associator_hom_def, SSet.prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, SSet.Truncated.Edge.map_fst, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorObj_obj, CategoryTheory.Over.grpObjMkPullbackSnd_mul, CategoryTheory.Functor.Monoidal.toUnit_ε_assoc, CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory, CategoryTheory.Grp.leftUnitor_hom_hom, CategoryTheory.CartesianCopyDiscard.instIsCommComonObjOfCartesian, CategoryTheory.Functor.Monoidal.whiskerRight_app_fst_assoc, CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd_assoc, CategoryTheory.comonEquiv_functor, CategoryTheory.CommGrp.toCommMon_X, CategoryTheory.Monoidal.whiskerRight_fst, CategoryTheory.MonObj.lift_comp_one_right, CategoryTheory.Functor.Monoidal.tensorObj_map, CategoryTheory.Functor.Monoidal.lift_μ_assoc, CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory, CategoryTheory.toOver_obj_left, CategoryTheory.Functor.Monoidal.tensorObjComp_hom_app, CategoryTheory.toOverPullbackIsoToOver_inv_app_left, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd, CategoryTheory.Functor.OplaxMonoidal.δ_snd, CategoryTheory.Over.toUnit_left, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_snd_hom, CategoryTheory.Functor.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts, SSet.hasDimensionLT_prod, CategoryTheory.monoidalOfHasFiniteProducts.δ_eq, CategoryTheory.Over.braiding_inv_left, CategoryTheory.leftUnitor_hom_apply, SSet.RelativeMorphism.Homotopy.h₀_assoc, CategoryTheory.IsSifted.factorization_prodComparison_colim, CategoryTheory.Grp.ε_def, CategoryTheory.toOverUnit_map_left, CategoryTheory.Grp.rightUnitor_hom_hom_hom, SSet.prodStdSimplex.objEquiv_apply_fst, CategoryTheory.MonObj.ofRepresentableBy_one, CategoryTheory.GrpObj.lift_inv_comp_right, AddGrpCat.tensorObj_eq, CategoryTheory.IsSifted.instIsIsoObjFunctorTypeColimTensorObjProdComparison, CategoryTheory.sheafToPresheaf_μ, CategoryTheory.symmetricOfHasFiniteProducts_braiding_hom, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, CategoryTheory.comul_eq_lift, CategoryTheory.Over.leftUnitor_hom_left, CategoryTheory.Grp.lift_hom, CategoryTheory.CartesianMonoidalCategory.tensorμ_fst_assoc, CategoryTheory.Over.isCommMonObj_mk_pullbackSnd, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd_assoc, CategoryTheory.Over.tensorObj_ext_iff, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_inv, CategoryTheory.Grp.hom_mul, CategoryTheory.coev_expComparison, CategoryTheory.types_tensorUnit_def, CategoryTheory.frobeniusMorphism_mate, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_fst_hom, CategoryTheory.toOverIsoToOverUnit_inv_app_left, CategoryTheory.Functor.OplaxMonoidal.δ_fst_assoc, CategoryTheory.MonoidalClosedFunctor.comparison_iso, SSet.instFiniteTensorUnit, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_ext_iff, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_hom, CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.Over.rightUnitor_inv_left_fst, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_snd_assoc, CategoryTheory.MonObj.lift_comp_one_right_assoc, CategoryTheory.CartesianMonoidalCategory.lift_braiding_hom, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app, CategoryTheory.Grp.Hom.hom_zpow, CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_snd, CategoryTheory.equivToOverUnit_unitIso, CategoryTheory.Preadditive.instIsCommMonObj, CategoryTheory.CartesianMonoidalCategory.instSubsingletonSymmetricCategory, CategoryTheory.GrpObj.one_inv_assoc, CategoryTheory.Functor.mapGrp_obj_grp_one, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, CategoryTheory.NatTrans.IsMonoidal.of_cartesianMonoidalCategory, CommGrpCat.μ_forget_apply, CategoryTheory.Cat.ihom_obj, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, SSet.Subcomplex.ofSimplexProd_eq_range, CategoryTheory.Over.whiskerRight_left_fst, SSet.Truncated.Edge.CompStruct.tensor_simplex_snd, CategoryTheory.Functor.homObjEquiv_symm_apply_app, CategoryTheory.Over.preservesTerminalIso_pullback, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, SSet.prodStdSimplex.objEquiv_δ_apply, CategoryTheory.Adjunction.mapCommGrp_unit, CategoryTheory.CartesianMonoidalCategory.comp_lift, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_inv_hom, CategoryTheory.Functor.mapGrp_id_one, CategoryTheory.Grp.associator_inv_hom_hom, CategoryTheory.Functor.Monoidal.μ_comp_assoc, CategoryTheory.GrpObj.η_whiskerRight_commutator_assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_id, CategoryTheory.associator_inv_apply, CategoryTheory.GrpObj.lift_comp_inv_right_assoc, CategoryTheory.bijection_natural, CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_inv_assoc, CategoryTheory.Over.rightUnitor_inv_left_snd, CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_hom, SSet.Truncated.Edge.id_tensor_id, CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst, AlgebraicGeometry.instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, CategoryTheory.IsCommMonObj.ofRepresentableBy, CategoryTheory.Grp.Hom.hom_hom_div, CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_inv, CategoryTheory.Grp.leftUnitor_hom_hom_hom, SSet.prodStdSimplex.objEquiv_naturality, CategoryTheory.CommGrp.instIsIsoMonHomGrp, CategoryTheory.Sheaf.tensorProd_isSheaf, CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η, CategoryTheory.toOverUnit_obj_left, CategoryTheory.Functor.Monoidal.μ_fst_assoc, CategoryTheory.Grp.forget_map, CategoryTheory.CartesianMonoidalCategory.tensorHom_fst, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural, CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_left, CategoryTheory.Mon.lift_hom, comp_toUnit_assoc, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_fst, CategoryTheory.IsCommMon.ofRepresentableBy, CategoryTheory.CommGrp.forget₂CommMon_map_hom, CategoryTheory.Functor.EssImageSubcategory.tensor_obj, CategoryTheory.essImage_yonedaMon, CategoryTheory.CommGrp.trivial_X, CategoryTheory.Over.whiskerRight_left_snd_assoc, CategoryTheory.MonObj.instIsMonHomSnd, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft_assoc, CategoryTheory.CommGrp.forget₂Grp_obj_mul, CategoryTheory.CartesianMonoidalCategory.lift_braiding_inv, CategoryTheory.CartesianMonoidalCategory.tensorHom_snd_assoc, CategoryTheory.CartesianMonoidalCategory.map_toUnit_comp_terminalComparison_assoc, SSet.instFiniteTensorObj, CategoryTheory.Adjunction.mapGrp_unit, CategoryTheory.Over.associator_inv_left_fst_fst_assoc, AlgebraicGeometry.Scheme.isCommMonObj_asOver_pullback, CategoryTheory.Functor.OplaxMonoidal.instSubsingleton, CategoryTheory.CartesianMonoidalCategory.prodComparison_snd_assoc, CategoryTheory.Over.associator_hom_left_fst, CategoryTheory.Grp.rightUnitor_inv_hom_hom, CategoryTheory.Monoidal.whiskerRight, CategoryTheory.Functor.natTransEquiv_symm_apply_app, CategoryTheory.Grp.forget₂Mon_map_hom, AlgebraicGeometry.Scheme.isMonHom_fst_id_right, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_assoc, SSet.prodStdSimplex.objEquiv_apply_snd, SSet.hoFunctor.unitHomEquiv_eq, CategoryTheory.GrpObj.tensorHom_inv_inv_mul_assoc, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_snd, CategoryTheory.instFaithfulMonFunctorOppositeMonCatYonedaMon, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorUnit_obj, CategoryTheory.ChosenPullbacksAlong.Over.tensorUnit_hom, CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_snd_assoc, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_fst, CategoryTheory.leftUnitor_inv_apply, CommAlgCat.lift_unop_hom, CategoryTheory.CartesianMonoidalCategory.lift_rightUnitor_hom_assoc, CategoryTheory.Over.tensorUnit_hom, CategoryTheory.Grp.whiskerRight_hom_hom, SSet.instFiniteObjOppositeSimplexCategoryTensorObj, CategoryTheory.Over.leftUnitor_inv_left_fst, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst, CategoryTheory.Monoidal.tensorHom, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val, CategoryTheory.Hom.mul_def, CategoryTheory.Grp.Hom.hom_hom_inv, CategoryTheory.associator_hom_apply_1, SSet.leftUnitor_inv_app_apply, SSet.ι₀_fst_assoc, SSet.ι₁_comp, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_obj, CategoryTheory.CatEnrichedOrdinary.Hom.mk_comp, CategoryTheory.expComparison_whiskerLeft, CategoryTheory.CartesianMonoidalCategory.tensorμ_snd, CommAlgCat.fst_unop_hom, CategoryTheory.Mon.fst_hom, CategoryTheory.Over.tensorHom_left_snd_assoc, CategoryTheory.MonObj.lift_comp_one_left, CategoryTheory.Grp.μ_def, CategoryTheory.Grp.snd_hom, CategoryTheory.Functor.OplaxMonoidal.lift_δ, CategoryTheory.Grp.tensorUnit_mul, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_snd_assoc, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_hom, SSet.whiskerRight_app_apply, CategoryTheory.braiding_hom_apply, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd_assoc, CategoryTheory.CommGrp.trivial_grp_one, SSet.rightUnitor_inv_app_apply, CategoryTheory.Over.leftUnitor_inv_left_snd, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, CategoryTheory.CartesianMonoidalCategory.associator_inv_snd_assoc, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_fst_assoc, CategoryTheory.MonObj.instIsMonHomLift, GrpCat.tensorObj_eq, CategoryTheory.Monoidal.rightUnitor_hom, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', CategoryTheory.bijection_symm_apply_id, CategoryTheory.Enriched.Functor.associator_hom_apply, CategoryTheory.Over.μ_pullback_left_fst_snd', SSet.ι₀_snd, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst, CategoryTheory.ChosenPullbacksAlong.Over.tensorUnit_left, CategoryTheory.sheafToPresheaf_δ, SSet.Truncated.Edge.CompStruct.tensor_simplex_fst, CategoryTheory.Grp.tensorUnit_X, Action.diagonalSuccIsoTensorTrivial_inv_hom_apply, CategoryTheory.Grp.whiskerLeft_hom, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_fst, CategoryTheory.Over.leftUnitor_inv_left_snd_assoc, CategoryTheory.Functor.chosenProd_obj, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd_assoc, CategoryTheory.CatEnrichedOrdinary.Hom.id_eq, CategoryTheory.Mon_Class.mul_eq_mul, SSet.Truncated.Edge.map_associator_hom, CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom, CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory, CategoryTheory.SimplicialThickening.functor_map, CategoryTheory.Grp.leftUnitor_inv_hom_hom, CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_map, CategoryTheory.Equivalence.mapCommGrp_unitIso, CategoryTheory.GrpObj.one_inv, CategoryTheory.GrpObj.mulRight_one, CategoryTheory.yonedaMon_map_app, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd_assoc, CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_fst_assoc, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, CategoryTheory.Enriched.Functor.whiskerRight_app_apply, CategoryTheory.CartesianMonoidalCategory.prodComparison_comp, SSet.ι₁_snd_assoc, CategoryTheory.Functor.OplaxMonoidal.instIsIsoη, CategoryTheory.Over.associator_hom_left_snd_fst, CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app, CategoryTheory.GrpObj.tensorObj.inv_def, CategoryTheory.MonObj.instIsMonHomFst, ModuleCat.free_ε_one, CategoryTheory.Grp.rightUnitor_inv_hom, CategoryTheory.Functor.Monoidal.toUnit_ε, CategoryTheory.Functor.Monoidal.whiskerRight_app_fst, CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_snd_assoc, SSet.instHasDimensionLETensorObjHAddNat, CategoryTheory.CartesianMonoidalCategory.map_toUnit_comp_terminalComparison, SSet.ι₁_app_fst, SSet.ι₁_snd, CategoryTheory.Over.rightUnitor_inv_left_snd_assoc, CategoryTheory.Over.toOverSectionsAdj_counit_app, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_snd, CategoryTheory.CommGrp.instFaithfulCommMonForget₂CommMon, CategoryTheory.Monoidal.associator_hom, Rep.linearization_η_hom_apply, CategoryTheory.CommGrp.hom_ext_iff, CategoryTheory.associator_inv_apply_1_2, CategoryTheory.Grp.forget₂Mon_obj_mul, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_comp, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerRight, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_snd_assoc, CategoryTheory.Mon_Class.one_eq_one, CategoryTheory.Grp.Hom.hom_pow, CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom, CategoryTheory.Grp.δ_def, SSet.whiskerLeft_app_apply, CategoryTheory.GrpObj.whiskerLeft_η_commutator, CategoryTheory.Grp.associator_hom_hom_hom, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_fst_assoc, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv, CategoryTheory.isoCartesianComon_hom_hom, ModuleCat.FreeMonoidal.εIso_inv_freeMk, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, CategoryTheory.Grp.toMon_X, CategoryTheory.frobeniusMorphism_iso_of_preserves_binary_products, CategoryTheory.instIsMonHomInvOfIsCommMonObj, CategoryTheory.Grp.braiding_inv_hom, CategoryTheory.Monoidal.whiskerLeft_snd, CategoryTheory.Over.sections_obj, CategoryTheory.Grp.mkIso'_hom_hom_hom, CategoryTheory.GrpObj.lift_inv_left_eq, CategoryTheory.Functor.comp_mapCommGrp_mul, SSet.Subcomplex.prod_obj, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso_hom, CommAlgCat.snd_unop_hom, CategoryTheory.Grp.id_hom, CategoryTheory.Functor.Monoidal.tensorObjComp_inv_app, CategoryTheory.CartesianMonoidalCategory.tensorδ_fst_assoc, SSet.Truncated.Edge.map_whiskerLeft, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, AddCommGrpCat.μ_forget_apply, Action.leftRegularTensorIso_hom_hom, CategoryTheory.CatEnrichedOrdinary.Hom.base_comp, CategoryTheory.equivToOverUnit_counitIso, SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse, ModuleCat.free_η_freeMk, CategoryTheory.Over.tensorHom_left, SSet.Truncated.Edge.map_snd, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, CategoryTheory.Grp.fst_hom, CategoryTheory.CartesianMonoidalCategory.associator_hom_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse, CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply, CategoryTheory.isCommMonObj_iff_isMulCommutative, CategoryTheory.Functor.chosenProd_map, CategoryTheory.Over.associator_inv_left_fst_snd, CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom, CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft, LightCondensed.free_internallyProjective_iff_tensor_condition', SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, AddCommGrpCat.tensorObj_eq, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd_assoc, CategoryTheory.CartesianMonoidalCategory.lift_fst_snd, CategoryTheory.Equivalence.mapGrp_unitIso, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerRight_assoc, CategoryTheory.toOverPullbackIsoToOver_hom_app_left, SSet.instHasDimensionLTTensorObjHAddNat, CategoryTheory.Mon.instIsCommMonObj, CategoryTheory.Over.associator_hom_left_snd_snd_assoc, CategoryTheory.Grp.tensorUnit_one, CategoryTheory.Mon.Hom.hom_mul, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_id, CategoryTheory.Functor.Monoidal.whiskerRight_app_snd_assoc, CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd, CategoryTheory.CartesianMonoidalCategory.terminalComparison_isIso_of_preservesLimits, CategoryTheory.CartesianMonoidalCategory.tensorHom_snd, CategoryTheory.Over.μ_pullback_left_fst_fst', CategoryTheory.instIsMonHomInvHomOfIsCommMonObj, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_obj, CategoryTheory.Over.μ_pullback_left_fst_snd, CategoryTheory.Over.whiskerRight_left, CategoryTheory.Functor.EssImageSubcategory.toUnit_def, CategoryTheory.Over.monObjMkPullbackSnd_one, CategoryTheory.CommGrp.forget₂Grp_obj_one, CategoryTheory.GrpObj.whiskerLeft_η_commutator_assoc, ModuleCat.free_μ_freeMk_tmul_freeMk, CategoryTheory.GrpObj.isPullback, CategoryTheory.uncurry_expComparison, AddGrpCat.μ_forget_apply, CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerLeft, CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom_assoc, CategoryTheory.toOverIsoToOverUnit_hom_app_left, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd, CommGrpCat.tensorObj_eq, ModuleCat.FreeMonoidal.μIso_hom_freeMk_tmul_freeMk, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_map, CategoryTheory.Cat.ihom_map, SSet.prodStdSimplex.objEquiv_map_apply, CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst_assoc, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso_inv, CategoryTheory.types_tensorObj_def, CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom, CategoryTheory.Functor.mapCommGrp_id_one, CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_fst_assoc, AlgebraicGeometry.Scheme.monObjAsOverPullback_mul, CategoryTheory.CartesianMonoidalCategory.lift_braiding_hom_assoc, CategoryTheory.Functor.Monoidal.tensorHom_app_fst, SSet.Truncated.Edge.map_tensorHom, CategoryTheory.CartesianMonoidalCategory.lift_snd, CategoryTheory.associator_hom_apply, CategoryTheory.Over.associator_inv_left_fst_fst, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, CategoryTheory.SimplicialThickening.SimplicialCategory.assoc, CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd, CategoryTheory.Functor.mapGrp_map_hom_hom, CategoryTheory.SemilatticeInf.tensorUnit, CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_hom, CategoryTheory.Functor.Monoidal.μ_comp, CategoryTheory.CommGrp.forget₂Grp_map_hom, CategoryTheory.Over.snd_left, CategoryTheory.Monoidal.tensorUnit, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_fst_assoc, CategoryTheory.Grp.comp_hom_hom, CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app, CategoryTheory.GrpObj.toMon_Class_injective, CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoδ, CategoryTheory.CartesianMonoidalCategory.lift_snd_assoc, CategoryTheory.CommGrp.forget₂CommMon_obj_mul, CategoryTheory.Over.tensorHom_left_fst, CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd, CategoryTheory.CatEnrichedOrdinary.Hom.comp_eq, CategoryTheory.Grp.braiding_inv_hom_hom, CategoryTheory.Over.whiskerRight_left_snd, CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst_assoc, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app, CategoryTheory.GrpObj.eq_lift_inv_right, SSet.prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_snd_assoc, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_snd, CategoryTheory.Functor.Monoidal.μ_fst, CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_comp, CategoryTheory.MonObj.ofRepresentableBy_mul, CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst, CommAlgCat.toUnit_unop_hom, SSet.Subcomplex.prod_monotone, SSet.ι₀_comp_assoc, CategoryTheory.Functor.Monoidal.tensorHom_app_snd, CategoryTheory.CatEnriched.comp_eq, CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_fst, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val, CategoryTheory.GrpObj.left_inv, CategoryTheory.Functor.OplaxMonoidal.δ_fst, CategoryTheory.Grp.tensorObj_X, SSet.ι₀_comp, CategoryTheory.Over.tensorHom_left_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_snd_assoc, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd, CategoryTheory.Functor.Monoidal.ε_of_cartesianMonoidalCategory, CategoryTheory.Grp.Hom.hom_mul, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_hom_left, CategoryTheory.Mon.Hom.hom_pow, CategoryTheory.GrpObj.mul_inv_rev_assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerRight_assoc, CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc, CategoryTheory.ε_def, CategoryTheory.Over.η_pullback_left, CategoryTheory.CommGrpObj.toIsCommMonObj, CategoryTheory.Grp.tensorObj_mul, CategoryTheory.Grp.rightUnitor_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_hom_left, CategoryTheory.Grp.forget₂Mon_obj_X, CategoryTheory.Grp.hom_ext_iff, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_obj, SSet.RelativeMorphism.Homotopy.h₁_assoc, CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst, CategoryTheory.Over.whiskerLeft_left_fst, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app, CategoryTheory.expComparison_ev, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_snd, CategoryTheory.Functor.Monoidal.snd_app, CategoryTheory.CatEnrichedOrdinary.homEquiv_comp, CategoryTheory.Functor.Monoidal.fst_app, SSet.RelativeMorphism.Homotopy.ofEq_h, CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app, CategoryTheory.CartesianMonoidalCategory.instNonemptyBraidedCategory, CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_hom_hom, CategoryTheory.GrpObj.tensorHom_inv_inv_mul, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.lift_left, SSet.rightUnitor_hom_app_apply, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv_assoc, CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight_assoc, CategoryTheory.Grp.forget₂Mon_comp_forget, CategoryTheory.associator_hom_apply_2_2, CategoryTheory.CartesianMonoidalCategory.hom_ext_iff, SSet.Truncated.tensor_map_apply_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj, CategoryTheory.Over.whiskerLeft_left_fst_assoc, CategoryTheory.GrpObj.mul_inv, CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage, CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_fst, ModuleCat.free_δ_freeMk, SSet.ι₁_fst, CategoryTheory.zeroMul_inv, CategoryTheory.Grp.tensorObj_one, CategoryTheory.Functor.Monoidal.tensorObj_obj, SSet.Truncated.Edge.tensor_edge, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_fst, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_obj, CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_obj, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', CategoryTheory.Over.whiskerLeft_left_snd_assoc, CategoryTheory.Functor.Monoidal.tensorHom_app_snd_assoc, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_comp, CategoryTheory.Functor.Monoidal.associator_inv_app, CategoryTheory.GrpObj.inv_def, CategoryTheory.CartesianMonoidalCategory.lift_comp_fst_snd, CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight, CategoryTheory.Grp.leftUnitor_inv_hom, CategoryTheory.CartesianMonoidalCategory.mono_lift_of_mono_right, SSet.Truncated.HomotopyCategory.BinaryProduct.square, CategoryTheory.Over.leftUnitor_inv_left_fst_assoc, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_app, CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left, CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso, CategoryTheory.Functor.mapGrp_obj_grp_mul, CategoryTheory.Functor.mapCommpGrp_id_mul, CategoryTheory.CommGrp.forget₂CommMon_obj_one, CategoryTheory.sheafToPresheaf_η, ModuleCat.FreeMonoidal.μIso_inv_freeMk, Rep.linearization_δ_hom, CategoryTheory.equivToOverUnit_inverse, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst_assoc, default_eq_toUnit, SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app, CategoryTheory.GrpObj.mul_inv_rev, CategoryTheory.GrpObj.mulRight_hom, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_hom_hom, CategoryTheory.Preadditive.mul_def, CategoryTheory.Grp.trivial_grp_one, CategoryTheory.Grp.snd_hom_hom, CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom, CategoryTheory.GrpObj.lift_comp_inv_left_assoc, CategoryTheory.Functor.comp_mapCommGrp_one, CategoryTheory.Over.associator_inv_left_fst_snd_assoc, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app, SSet.RelativeMorphism.Homotopy.h₀, CategoryTheory.Grp.hom_one, CategoryTheory.Grp.forget₂Mon_obj_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Over.rightUnitor_hom_left, CategoryTheory.Mod_.trivialAction_X, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.CatEnriched.id_eq, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val, CategoryTheory.toOver_map_left, CategoryTheory.Over.sections_map, CategoryTheory.CartesianMonoidalCategory.lift_fst, SSet.RelativeMorphism.Homotopy.precomp_h, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_id, CategoryTheory.Hom.one_def, CategoryTheory.Over.μ_pullback_left_snd, CategoryTheory.Grp.associator_inv_hom, SSet.ι₀_fst, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst, CategoryTheory.Grp.homMk_hom_hom, CategoryTheory.ChosenPullbacksAlong.Over.toUnit_left, CategoryTheory.Functor.Monoidal.μ_snd, CategoryTheory.Monoidal.whiskerRight_snd, CategoryTheory.Functor.FullyFaithful.grpObj_mul, SSet.associator_hom_app_apply, CategoryTheory.CartesianMonoidalCategory.lift_leftUnitor_hom, toUnit_unit, CategoryTheory.GrpObj.mulRight_inv, CategoryTheory.symmetricOfHasFiniteProducts_braiding_inv, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity, CategoryTheory.sheafToPresheaf_ε, CategoryTheory.GrpObj.mul_inv_assoc, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst, CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom, CategoryTheory.Functor.Monoidal.μ_snd_assoc, CategoryTheory.Mon.hom_mul, CategoryTheory.Over.braiding_hom_left, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_snd, SSet.RelativeMorphism.Homotopy.h₁, CategoryTheory.Functor.Monoidal.whiskerRight_app_snd, CategoryTheory.GrpObj.η_whiskerRight_commutator, SSet.Subcomplex.range_tensorHom, CategoryTheory.CartesianMonoidalCategory.lift_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_snd, CategoryTheory.Functor.homMonoidHom_apply, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_snd, CategoryTheory.whiskerLeft_apply, CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom_assoc, CategoryTheory.Over.μ_pullback_left_fst_fst, SSet.RelativeMorphism.Homotopy.postcomp_h, CategoryTheory.CartesianMonoidalCategory.mono_lift_of_mono_left, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerRight_hom, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, CategoryTheory.ExponentialIdeal.exp_closed, CategoryTheory.GrpObj.right_inv, CategoryTheory.GrpObj.lift_comp_inv_left, CategoryTheory.Over.tensorUnit_left, CategoryTheory.GrpObj.eq_lift_inv_left, CategoryTheory.Grp.Hom.hom_inv, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, Action.diagonalSuccIsoTensorDiagonal_hom_hom, CategoryTheory.Equivalence.mapCommGrp_counitIso, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp_assoc, CategoryTheory.CartesianMonoidalCategory.lift_map, CategoryTheory.MonObj.lift_comp_one_left_assoc, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, Action.diagonalSuccIsoTensorTrivial_hom_hom_apply, CategoryTheory.Grp.instFaithfulMonForget₂Mon, CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, CategoryTheory.Monoidal.associator_inv, CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso, CategoryTheory.Monoidal.rightUnitor_inv, CategoryTheory.Monoidal.whiskerLeft, CategoryTheory.Functor.Monoidal.associator_hom_app, CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerRight, CategoryTheory.Grp.braiding_hom_hom, CategoryTheory.Over.whiskerRight_left_fst_assoc, SSet.RelativeMorphism.Homotopy.rel, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, CategoryTheory.CartesianMonoidalCategory.lift_map_assoc, CategoryTheory.monoidalOfHasFiniteProducts.η_eq, CategoryTheory.Over.tensorHom_left_snd, CategoryTheory.Grp.η_def, SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app, CategoryTheory.equivToOverUnit_functor, CategoryTheory.Functor.FullyFaithful.grpObj_one, CategoryTheory.CartesianMonoidalCategory.lift_fst_comp_snd_comp, SSet.Truncated.Edge.map_whiskerRight, ModuleCat.FreeMonoidal.εIso_hom_one, CategoryTheory.CommGrp.trivial_grp_mul, CategoryTheory.Grp.associator_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, SSet.RelativeMorphism.Homotopy.refl_h, CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd_assoc, CategoryTheory.associator_hom_apply_2_1, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.Monoidal.tensorObj, CategoryTheory.Preadditive.one_def, CategoryTheory.Over.lift_left, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom, CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst, CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_id, CategoryTheory.whiskerRight_apply, CategoryTheory.instIsLeftAdjointTensorLeft, CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp, CategoryTheory.CommGrp.trivial_grp_inv, CategoryTheory.SimplicialThickening.functor_id, CategoryTheory.GrpObj.ofIso_mul, CategoryTheory.Functor.Monoidal.leftUnitor_hom_app, AlgebraicGeometry.Scheme.monObjAsOverPullback_one, CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_map, CategoryTheory.GrpObj.lift_comp_inv_right, CategoryTheory.Functor.Monoidal.lift_μ, CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerLeft_assoc, fst_def, CategoryTheory.yonedaGrp_map_app, CategoryTheory.Functor.Monoidal.leftUnitor_inv_app, SSet.hasDimensionLE_prod, SSet.ι₁_fst_assoc, CategoryTheory.Monoidal.whiskerLeft_fst, CategoryTheory.MonObj.one_eq_one, SSet.Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst_assoc, CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom, CategoryTheory.braiding_inv_apply, CategoryTheory.CartesianMonoidalCategory.homEquivToProd_apply, CategoryTheory.Functor.Monoidal.rightUnitor_hom_app, CategoryTheory.Grp.whiskerRight_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, CategoryTheory.Over.fst_left, CategoryTheory.Over.associator_hom_left_fst_assoc, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerLeft_hom, SSet.leftUnitor_hom_app_apply, CategoryTheory.rightUnitor_inv_apply, CategoryTheory.Over.isMonHom_pullbackFst_id_right, CategoryTheory.Functor.OplaxMonoidal.lift_δ_assoc, CategoryTheory.Grp.tensorHom_hom, CategoryTheory.GrpObj.toMonObj_injective, CategoryTheory.CartesianMonoidalCategory.tensorμ_fst, CategoryTheory.GrpObj.ofIso_one, CategoryTheory.Grp.Hom.hom_one, CategoryTheory.Functor.Braided.instSubsingleton, CategoryTheory.Over.tensorObj_left, CategoryTheory.Grp.fst_hom_hom, CategoryTheory.CartesianMonoidalCategory.lift_snd_fst, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd', CategoryTheory.toOverUnitPullback_hom_app_left, CategoryTheory.Functor.EssImageSubcategory.lift_def, CategoryTheory.Mod_.trivialAction_mod_smul, CategoryTheory.Grp.mkIso'_inv_hom_hom, CategoryTheory.Over.ε_pullback_left, CategoryTheory.CartesianMonoidalCategory.lift_rightUnitor_hom, CategoryTheory.isoCartesianComon_inv_hom, SSet.associator_inv_app_apply, CategoryTheory.Grp.trivial_grp_mul, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, GrpCat.μ_forget_apply, CategoryTheory.Monoidal.leftUnitor_inv, CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst_assoc, CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_snd_assoc, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_fst_assoc, CategoryTheory.tensor_apply, CategoryTheory.Grp.trivial_X, CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, CategoryTheory.SimplicialThickening.functor_obj_as, CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_comp, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_app, CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj, CategoryTheory.Over.associator_hom_left_snd_snd, CategoryTheory.Grp.braiding_hom_hom_hom, CategoryTheory.Over.associator_inv_left_snd_assoc, CategoryTheory.CommGrp.forget₂CommMon_comp_forget, CategoryTheory.GrpObj.right_inv_assoc, CategoryTheory.comonEquiv_inverse, CategoryTheory.toOverUnitPullback_inv_app_left, CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_fst, CategoryTheory.CatEnrichedOrdinary.homEquiv_id, Rep.linearization_ε_hom, CategoryTheory.SimplicialThickening.SimplicialCategory.id_comp, AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed, CategoryTheory.MonObj.instIsMonHomMulOfIsCommMonObj, CategoryTheory.SimplicialThickening.functor_comp, CategoryTheory.Sheaf.tensorUnit_isSheaf, CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd_assoc, CategoryTheory.Functor.map_one, CategoryTheory.associator_inv_apply_2, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst_assoc, CategoryTheory.Monoidal.leftUnitor_hom, CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom, CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorHom_hom, CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoη, CategoryTheory.Mon.hom_one, CategoryTheory.Over.whiskerLeft_left_snd, CategoryTheory.yonedaMon_obj, CategoryTheory.toOver_map, CategoryTheory.rightUnitor_hom_apply, CategoryTheory.Functor.Monoidal.instSubsingleton, CategoryTheory.CartesianMonoidalCategory.homEquivToProd_symm_apply, CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft_assoc, SSet.ι₀_app_fst, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_fst_assoc, snd_def, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_snd, CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_assoc, CategoryTheory.CartesianMonoidalCategory.tensorδ_fst, CategoryTheory.toUnit_comp_curryRightUnitorHom, CategoryTheory.MonObj.mul_eq_mul, CategoryTheory.Grp.comp_hom, CategoryTheory.Grp.instFullMonForget₂Mon, CategoryTheory.CartesianMonoidalCategory.tensorHom_fst_assoc, CategoryTheory.Grp.id_hom_hom, CategoryTheory.Adjunction.mapCommGrp_counit, CategoryTheory.associator_inv_apply_1_1, CategoryTheory.GrpObj.lift_inv_comp_right_assoc, CategoryTheory.Over.tensorObj_hom, CategoryTheory.CartesianMonoidalCategory.tensorμ_snd_assoc, SSet.ι₁_comp_assoc, CategoryTheory.CartesianMonoidalCategory.isIso_prodComparison_of_preservesLimit_pair, CategoryTheory.toOverUnit_obj_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_inv, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft, CategoryTheory.Adjunction.mapGrp_counit, CategoryTheory.Functor.comp_mapGrp_one, CategoryTheory.SemilatticeInf.tensorObj, CategoryTheory.Mon.snd_hom, comp_toUnit, CategoryTheory.Mon.Hom.hom_one, CategoryTheory.Functor.OplaxMonoidal.instIsIsoδ, CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_fst_assoc, CategoryTheory.CommGrp.forget_map, CategoryTheory.comonEquiv_counitIso, CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_snd_assoc, Rep.linearization_μ_hom, CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_inv_hom, CategoryTheory.CatEnrichedOrdinary.Hom.base_id, SSet.RelativeMorphism.Homotopy.rel_assoc, CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left, CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom, CategoryTheory.CartesianMonoidalCategory.lift_braiding_inv_assoc, CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd, CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom_assoc
toUnit 📖	CompOp	48 math math: CategoryTheory.GrpObj.lift_inv_comp_left, CategoryTheory.counit_eq_toUnit, CategoryTheory.GrpObj.lift_inv_comp_left_assoc, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom, CategoryTheory.GrpObj.left_inv_assoc, CategoryTheory.MonObj.instIsMonHomToUnit, CategoryTheory.Functor.Monoidal.toUnit_ε_assoc, CategoryTheory.Over.toUnit_left, CategoryTheory.toOverUnit_map_left, CategoryTheory.GrpObj.lift_inv_comp_right, CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, CategoryTheory.GrpObj.η_whiskerRight_commutator_assoc, CategoryTheory.GrpObj.lift_comp_inv_right_assoc, CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η, comp_toUnit_assoc, CategoryTheory.CartesianMonoidalCategory.map_toUnit_comp_terminalComparison_assoc, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd_assoc, CategoryTheory.Functor.Monoidal.toUnit_ε, CategoryTheory.CartesianMonoidalCategory.map_toUnit_comp_terminalComparison, CategoryTheory.GrpObj.whiskerLeft_η_commutator, CategoryTheory.Functor.EssImageSubcategory.toUnit_def, CategoryTheory.GrpObj.whiskerLeft_η_commutator_assoc, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom_assoc, CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom, CommAlgCat.toUnit_unop_hom, CategoryTheory.GrpObj.left_inv, CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst_assoc, default_eq_toUnit, CategoryTheory.GrpObj.mulRight_hom, CategoryTheory.GrpObj.lift_comp_inv_left_assoc, CategoryTheory.Hom.one_def, CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst, CategoryTheory.ChosenPullbacksAlong.Over.toUnit_left, toUnit_unit, CategoryTheory.GrpObj.mulRight_inv, CategoryTheory.GrpObj.η_whiskerRight_commutator, CategoryTheory.GrpObj.right_inv, CategoryTheory.GrpObj.lift_comp_inv_left, CategoryTheory.GrpObj.lift_comp_inv_right, CategoryTheory.toOverUnitPullback_hom_app_left, CategoryTheory.GrpObj.right_inv_assoc, CategoryTheory.toOverUnitPullback_inv_app_left, CategoryTheory.toUnit_comp_curryRightUnitorHom, CategoryTheory.GrpObj.lift_inv_comp_right_assoc, CategoryTheory.toOverUnit_obj_hom, comp_toUnit, CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_toUnit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalCategory toUnit	—	toUnit_unique
comp_toUnit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalCategory toUnit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_toUnit
default_eq_toUnit 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalCategory Unique.instInhabited instUniqueHomTensorUnit toUnit	—	—
fst_def 📖	mathematical	—	fst CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Limits.IsTerminal.from isTerminalTensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
snd_def 📖	mathematical	—	snd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.IsTerminal.from isTerminalTensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
toUnit_unique 📖	—	—	—	—	Unique.instSubsingleton
toUnit_unique_iff 📖	—	—	—	—	toUnit_unique
toUnit_unit 📖	mathematical	—	toUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	toUnit_unique

---

← Back to Index