Over

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

Statistics

Metric	Count
Definitions braidedCategory, cartesianMonoidalCategory, grpObjMkPullbackSnd, instBraidedPullback, monObjMkPullbackSnd	5
Theorems associator_hom_left_fst, associator_hom_left_fst_assoc, associator_hom_left_snd_fst, associator_hom_left_snd_fst_assoc, associator_hom_left_snd_snd, associator_hom_left_snd_snd_assoc, associator_inv_left_fst_fst, associator_inv_left_fst_fst_assoc, associator_inv_left_fst_snd, associator_inv_left_fst_snd_assoc, associator_inv_left_snd, associator_inv_left_snd_assoc, braiding_hom_left, braiding_inv_left, fst_left, grpObjMkPullbackSnd_mul, grpObjMkPullbackSnd_one, isCommMonObj_mk_pullbackSnd, isMonHom_pullbackFst_id_right, leftUnitor_hom_left, leftUnitor_inv_left_fst, leftUnitor_inv_left_fst_assoc, leftUnitor_inv_left_snd, leftUnitor_inv_left_snd_assoc, lift_left, monObjMkPullbackSnd_mul, monObjMkPullbackSnd_one, preservesTerminalIso_pullback, prodComparisonIso_pullback_Spec_inv_left_fst_fst', prodComparisonIso_pullback_inv_left_fst_fst, prodComparisonIso_pullback_inv_left_fst_snd', prodComparisonIso_pullback_inv_left_snd', rightUnitor_hom_left, rightUnitor_inv_left_fst, rightUnitor_inv_left_fst_assoc, rightUnitor_inv_left_snd, rightUnitor_inv_left_snd_assoc, snd_left, tensorHom_left, tensorHom_left_fst, tensorHom_left_fst_assoc, tensorHom_left_snd, tensorHom_left_snd_assoc, tensorObj_ext, tensorObj_ext_iff, tensorObj_hom, tensorObj_left, tensorUnit_hom, tensorUnit_left, toUnit_left, whiskerLeft_left, whiskerLeft_left_fst, whiskerLeft_left_fst_assoc, whiskerLeft_left_snd, whiskerLeft_left_snd_assoc, whiskerRight_left, whiskerRight_left_fst, whiskerRight_left_fst_assoc, whiskerRight_left_snd, whiskerRight_left_snd_assoc, ε_pullback_left, η_pullback_left, μ_pullback_left_fst_fst, μ_pullback_left_fst_fst', μ_pullback_left_fst_snd, μ_pullback_left_fst_snd', μ_pullback_left_snd, μ_pullback_left_snd'	68
Total	73

CategoryTheory.Over

Definitions

Name	Category	Theorems
braidedCategory 📖	CompOp	15 math math: μ_pullback_left_snd', monObjMkPullbackSnd_mul, braiding_inv_left, isCommMonObj_mk_pullbackSnd, μ_pullback_left_fst_snd', μ_pullback_left_fst_fst', μ_pullback_left_fst_snd, monObjMkPullbackSnd_one, AlgebraicGeometry.Scheme.monObjAsOverPullback_mul, η_pullback_left, μ_pullback_left_snd, braiding_hom_left, μ_pullback_left_fst_fst, AlgebraicGeometry.Scheme.monObjAsOverPullback_one, ε_pullback_left
cartesianMonoidalCategory 📖	CompOp	69 math math: associator_hom_left_snd_fst_assoc, μ_pullback_left_snd', associator_inv_left_snd, rightUnitor_inv_left_fst_assoc, monObjMkPullbackSnd_mul, whiskerLeft_left, grpObjMkPullbackSnd_one, grpObjMkPullbackSnd_mul, toUnit_left, braiding_inv_left, leftUnitor_hom_left, isCommMonObj_mk_pullbackSnd, tensorObj_ext_iff, rightUnitor_inv_left_fst, whiskerRight_left_fst, preservesTerminalIso_pullback, rightUnitor_inv_left_snd, whiskerRight_left_snd_assoc, associator_inv_left_fst_fst_assoc, associator_hom_left_fst, tensorUnit_hom, leftUnitor_inv_left_fst, tensorHom_left_snd_assoc, leftUnitor_inv_left_snd, prodComparisonIso_pullback_inv_left_snd', μ_pullback_left_fst_snd', leftUnitor_inv_left_snd_assoc, associator_hom_left_snd_fst, rightUnitor_inv_left_snd_assoc, prodComparisonIso_pullback_inv_left_fst_fst, tensorHom_left, associator_inv_left_fst_snd, associator_hom_left_snd_snd_assoc, μ_pullback_left_fst_fst', μ_pullback_left_fst_snd, whiskerRight_left, monObjMkPullbackSnd_one, AlgebraicGeometry.Scheme.monObjAsOverPullback_mul, associator_inv_left_fst_fst, snd_left, tensorHom_left_fst, whiskerRight_left_snd, tensorHom_left_fst_assoc, η_pullback_left, whiskerLeft_left_fst, whiskerLeft_left_fst_assoc, prodComparisonIso_pullback_Spec_inv_left_fst_fst', whiskerLeft_left_snd_assoc, leftUnitor_inv_left_fst_assoc, associator_inv_left_fst_snd_assoc, rightUnitor_hom_left, μ_pullback_left_snd, braiding_hom_left, μ_pullback_left_fst_fst, tensorUnit_left, whiskerRight_left_fst_assoc, tensorHom_left_snd, lift_left, AlgebraicGeometry.Scheme.monObjAsOverPullback_one, fst_left, associator_hom_left_fst_assoc, isMonHom_pullbackFst_id_right, tensorObj_left, prodComparisonIso_pullback_inv_left_fst_snd', ε_pullback_left, associator_hom_left_snd_snd, associator_inv_left_snd_assoc, whiskerLeft_left_snd, tensorObj_hom
grpObjMkPullbackSnd 📖	CompOp	2 math math: grpObjMkPullbackSnd_one, grpObjMkPullbackSnd_mul
instBraidedPullback 📖	CompOp	12 math math: μ_pullback_left_snd', monObjMkPullbackSnd_mul, μ_pullback_left_fst_snd', μ_pullback_left_fst_fst', μ_pullback_left_fst_snd, monObjMkPullbackSnd_one, AlgebraicGeometry.Scheme.monObjAsOverPullback_mul, η_pullback_left, μ_pullback_left_snd, μ_pullback_left_fst_fst, AlgebraicGeometry.Scheme.monObjAsOverPullback_one, ε_pullback_left
monObjMkPullbackSnd 📖	CompOp	4 math math: monObjMkPullbackSnd_mul, isCommMonObj_mk_pullbackSnd, monObjMkPullbackSnd_one, isMonHom_pullbackFst_id_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_left_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.limit.lift_π
associator_hom_left_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_left_fst
associator_hom_left_snd_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
associator_hom_left_snd_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_left_snd_fst
associator_hom_left_snd_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
associator_hom_left_snd_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_left_snd_snd
associator_inv_left_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
associator_inv_left_fst_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_left_fst_fst
associator_inv_left_fst_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
associator_inv_left_fst_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_left_fst_snd
associator_inv_left_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.limit.lift_π
associator_inv_left_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_left_snd
braiding_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding braidedCategory CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Limits.pullbackSymmetry	—	—
braiding_inv_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding braidedCategory CategoryTheory.Iso.hom CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Limits.pullbackSymmetry	—	—
fst_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Limits.pullback.fst CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
grpObjMkPullbackSnd_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.GrpObj.toMonObj grpObjMkPullbackSnd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts CategoryTheory.Functor.map	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
grpObjMkPullbackSnd_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd CategoryTheory.GrpObj.toMonObj grpObjMkPullbackSnd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts CategoryTheory.Functor.map	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
isCommMonObj_mk_pullbackSnd 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory braidedCategory CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd monObjMkPullbackSnd	—	CategoryTheory.CommMon.comm CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
isMonHom_pullbackFst_id_right 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Limits.pullback CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd monObjMkPullbackSnd homMk CategoryTheory.Limits.pullback.fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.condition	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.pullback.condition CategoryTheory.Category.assoc OverMorphism.ext CategoryTheory.IsIso.id CategoryTheory.Limits.pullback_snd_iso_of_left_iso ε_pullback_left CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso_assoc CategoryTheory.IsIso.inv_id CategoryTheory.Category.id_comp CategoryTheory.Limits.pullback.hom_ext μ_pullback_left_fst_fst' tensorHom_left_fst μ_pullback_left_fst_snd' tensorHom_left_snd
leftUnitor_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
leftUnitor_inv_left_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Limits.pullback.fst CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Comma.hom	—	CategoryTheory.Limits.limit.lift_π
leftUnitor_inv_left_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Limits.pullback.fst CategoryTheory.CategoryStruct.id CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_inv_left_fst
leftUnitor_inv_left_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Limits.pullback.snd CategoryTheory.CategoryStruct.id CategoryTheory.Comma.hom	—	CategoryTheory.Limits.limit.lift_π
leftUnitor_inv_left_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Limits.pullback.snd CategoryTheory.CategoryStruct.id CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_inv_left_snd
lift_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.Limits.pullback.lift CategoryTheory.Comma.left CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.CommaMorphism.right CategoryTheory.CommaMorphism.w	—	—
monObjMkPullbackSnd_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd monObjMkPullbackSnd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.LaxBraided.toLaxMonoidal braidedCategory CategoryTheory.Functor.Braided.toLaxBraided instBraidedPullback CategoryTheory.Functor.map	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
monObjMkPullbackSnd_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd monObjMkPullbackSnd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.LaxBraided.toLaxMonoidal braidedCategory CategoryTheory.Functor.Braided.toLaxBraided instBraidedPullback CategoryTheory.Functor.map	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
preservesTerminalIso_pullback 📖	mathematical	—	CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso CategoryTheory.Over CategoryTheory.instCategoryOver cartesianMonoidalCategory pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.finCategoryDiscreteOfFintype Fintype.instPEmpty CategoryTheory.Functor.empty isoMk CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.asIso CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.pullback.snd CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback_snd_iso_of_left_iso CategoryTheory.IsIso.id	—	CategoryTheory.Iso.ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.Limits.pullback_snd_iso_of_left_iso CategoryTheory.IsIso.id CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
prodComparisonIso_pullback_Spec_inv_left_fst_fst' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.CartesianMonoidalCategory.prodComparisonIso CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.finCategoryDiscreteOfFintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.snd	—	prodComparisonIso_pullback_inv_left_fst_fst
prodComparisonIso_pullback_inv_left_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.CartesianMonoidalCategory.prodComparisonIso CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.finCategoryDiscreteOfFintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.pullback CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Comma.instIsIsoLeft CategoryTheory.Iso.isIso_hom hom_left_inv_left_assoc CategoryTheory.CommaMorphism.w CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
prodComparisonIso_pullback_inv_left_fst_snd' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.CartesianMonoidalCategory.prodComparisonIso CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.finCategoryDiscreteOfFintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Comma.instIsIsoLeft CategoryTheory.Iso.isIso_hom hom_left_inv_left_assoc CategoryTheory.CommaMorphism.w CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
prodComparisonIso_pullback_inv_left_snd' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.CartesianMonoidalCategory.prodComparisonIso CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.finCategoryDiscreteOfFintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Comma.instIsIsoLeft CategoryTheory.Iso.isIso_hom hom_left_inv_left_assoc CategoryTheory.CommaMorphism.w CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
rightUnitor_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Limits.pullback.fst CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
rightUnitor_inv_left_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.limit.lift_π
rightUnitor_inv_left_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_inv_left_fst
rightUnitor_inv_left_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.limit.lift_π
rightUnitor_inv_left_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_inv_left_snd
snd_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
tensorHom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.pullback.map CategoryTheory.Comma.left CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
tensorHom_left_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.limit.lift_π
tensorHom_left_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorHom_left_fst
tensorHom_left_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.limit.lift_π
tensorHom_left_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorHom_left_snd
tensorObj_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd	—	—	CategoryTheory.Limits.pullback.hom_ext
tensorObj_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd	—	tensorObj_ext
tensorObj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst	—	—
tensorObj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Limits.pullback CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan	—	—
tensorUnit_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
tensorUnit_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory	—	—
toUnit_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.Comma.hom	—	—
whiskerLeft_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Limits.pullback.map CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
whiskerLeft_left_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id
whiskerLeft_left_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Limits.pullback.fst CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_left_fst
whiskerLeft_left_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback	—	CategoryTheory.Limits.limit.lift_π
whiskerLeft_left_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_left_snd
whiskerRight_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.pullback.map CategoryTheory.Comma.left CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
whiskerRight_left_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback	—	CategoryTheory.Limits.limit.lift_π
whiskerRight_left_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.pullback.fst CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_left_fst
whiskerRight_left_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id
whiskerRight_left_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.pullback.snd CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_left_snd
ε_pullback_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.LaxBraided.toLaxMonoidal braidedCategory CategoryTheory.Functor.Braided.toLaxBraided instBraidedPullback CategoryTheory.inv CategoryTheory.Limits.pullback CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback_snd_iso_of_left_iso CategoryTheory.IsIso.id	—	CategoryTheory.IsIso.eq_inv_of_hom_inv_id CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.pullback_snd_iso_of_left_iso CategoryTheory.IsIso.id η_pullback_left comp_left CategoryTheory.Functor.Monoidal.η_ε id_left
η_pullback_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Functor.Braided.toMonoidal braidedCategory instBraidedPullback CategoryTheory.Limits.pullback.snd CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
μ_pullback_left_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.LaxBraided.toLaxMonoidal braidedCategory CategoryTheory.Functor.Braided.toLaxBraided instBraidedPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Functor.Monoidal.instPreservesFiniteProducts CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Comma.instIsIsoLeft CategoryTheory.Iso.isIso_hom comp_left_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp CategoryTheory.CommaMorphism.w CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
μ_pullback_left_fst_fst' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.LaxBraided.toLaxMonoidal braidedCategory CategoryTheory.Functor.Braided.toLaxBraided instBraidedPullback CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	μ_pullback_left_fst_fst
μ_pullback_left_fst_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.LaxBraided.toLaxMonoidal braidedCategory CategoryTheory.Functor.Braided.toLaxBraided instBraidedPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Functor.Monoidal.instPreservesFiniteProducts CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Comma.instIsIsoLeft CategoryTheory.Iso.isIso_hom comp_left_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp CategoryTheory.CommaMorphism.w CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
μ_pullback_left_fst_snd' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.LaxBraided.toLaxMonoidal braidedCategory CategoryTheory.Functor.Braided.toLaxBraided instBraidedPullback CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	μ_pullback_left_fst_snd
μ_pullback_left_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.LaxBraided.toLaxMonoidal braidedCategory CategoryTheory.Functor.Braided.toLaxBraided instBraidedPullback CategoryTheory.Limits.pullback.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.pullback	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype CategoryTheory.Functor.Monoidal.instPreservesFiniteProducts CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint pullbackIsRightAdjoint CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Comma.instIsIsoLeft CategoryTheory.Iso.isIso_hom comp_left_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp CategoryTheory.CommaMorphism.w CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π
μ_pullback_left_snd' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.Functor.obj pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.CommaMorphism.left CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.LaxBraided.toLaxMonoidal braidedCategory CategoryTheory.Functor.Braided.toLaxBraided instBraidedPullback CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	μ_pullback_left_snd

---

← Back to Index