Over

📁 Source: Mathlib/CategoryTheory/LocallyCartesianClosed/Over.lean

Statistics

Metric	Count
Definitions binaryFan, binaryFanIsBinaryProduct, cartesianMonoidalCategoryOver, equivToOverUnit, forgetAdjToOver, toOver, toOverIsoToOverUnit, toOverIteratedSliceForwardIsoPullback, toOverPullbackIsoToOver, toOverUnit, toOverUnitPullback	11
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, fst_eq_fst', leftUnitor_hom_left, leftUnitor_inv_left_fst, leftUnitor_inv_left_fst_assoc, leftUnitor_inv_left_snd, leftUnitor_inv_left_snd_assoc, lift_left, rightUnitor_hom_left, rightUnitor_inv_left_fst, rightUnitor_inv_left_fst_assoc, rightUnitor_inv_left_snd, rightUnitor_inv_left_snd_assoc, snd_eq_snd', 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, equivToOverUnit_counitIso, equivToOverUnit_functor, equivToOverUnit_inverse, equivToOverUnit_unitIso, homEquiv_symm, forgetAdjToOver_counit_app, forgetAdjToOver_unit_app, toOverIsoToOverUnit_hom_app_left, toOverIsoToOverUnit_inv_app_left, toOverIteratedSliceForwardIsoPullback_hom_app_left, toOverIteratedSliceForwardIsoPullback_inv_app_left, toOverPullbackIsoToOver_hom_app_left, toOverPullbackIsoToOver_inv_app_left, toOverUnitPullback_hom_app_left, toOverUnitPullback_inv_app_left, toOverUnit_map_left, toOverUnit_obj_hom, toOverUnit_obj_left, toOver_map, toOver_map_left, toOver_obj_hom, toOver_obj_left	69
Total	80

CategoryTheory

Definitions

Name	Category	Theorems
equivToOverUnit 📖	CompOp	6 math math: toOverIsoToOverUnit_inv_app_left, equivToOverUnit_unitIso, equivToOverUnit_counitIso, toOverIsoToOverUnit_hom_app_left, equivToOverUnit_inverse, equivToOverUnit_functor
forgetAdjToOver 📖	CompOp	3 math math: forgetAdjToOver_unit_app, forgetAdjToOver.homEquiv_symm, forgetAdjToOver_counit_app
toOver 📖	CompOp	18 math math: toOver_obj_hom, toOver_obj_left, toOverPullbackIsoToOver_inv_app_left, toOverIsoToOverUnit_inv_app_left, Over.toOverSectionsAdj_unit_app, Over.toOverSectionsAdj_counit_app, forgetAdjToOver_unit_app, toOverIteratedSliceForwardIsoPullback_hom_app_left, toOverPullbackIsoToOver_hom_app_left, toOverIsoToOverUnit_hom_app_left, forgetAdjToOver.homEquiv_symm, toOver_map_left, toOverIteratedSliceForwardIsoPullback_inv_app_left, toOverUnitPullback_hom_app_left, toOverUnitPullback_inv_app_left, Over.coreHomEquivToOverSections_homEquiv, toOver_map, forgetAdjToOver_counit_app
toOverIsoToOverUnit 📖	CompOp	2 math math: toOverIsoToOverUnit_inv_app_left, toOverIsoToOverUnit_hom_app_left
toOverIteratedSliceForwardIsoPullback 📖	CompOp	2 math math: toOverIteratedSliceForwardIsoPullback_hom_app_left, toOverIteratedSliceForwardIsoPullback_inv_app_left
toOverPullbackIsoToOver 📖	CompOp	2 math math: toOverPullbackIsoToOver_inv_app_left, toOverPullbackIsoToOver_hom_app_left
toOverUnit 📖	CompOp	10 math math: toOverUnit_map_left, toOverIsoToOverUnit_inv_app_left, equivToOverUnit_unitIso, toOverUnit_obj_left, equivToOverUnit_counitIso, toOverIsoToOverUnit_hom_app_left, equivToOverUnit_inverse, toOverUnitPullback_hom_app_left, toOverUnitPullback_inv_app_left, toOverUnit_obj_hom
toOverUnitPullback 📖	CompOp	2 math math: toOverUnitPullback_hom_app_left, toOverUnitPullback_inv_app_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivToOverUnit_counitIso 📖	mathematical	—	Equivalence.counitIso Over MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCategoryOver equivToOverUnit NatIso.ofComponents Functor.comp toOverUnit Over.forget Functor.id Iso.refl Functor.obj	—	—
equivToOverUnit_functor 📖	mathematical	—	Equivalence.functor Over MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCategoryOver equivToOverUnit Over.forget	—	—
equivToOverUnit_inverse 📖	mathematical	—	Equivalence.inverse Over MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCategoryOver equivToOverUnit toOverUnit	—	—
equivToOverUnit_unitIso 📖	mathematical	—	Equivalence.unitIso Over MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCategoryOver equivToOverUnit NatIso.ofComponents Functor.id Functor.comp Over.forget toOverUnit Over.isoMk Functor.obj Iso.refl Comma.left Discrete discreteCategory Functor.fromPUnit	—	—
forgetAdjToOver_counit_app 📖	mathematical	—	NatTrans.app Functor.comp Over instCategoryOver toOver Over.forget Functor.id Adjunction.counit forgetAdjToOver SemiCartesianMonoidalCategory.fst CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	—
forgetAdjToOver_unit_app 📖	mathematical	—	NatTrans.app Over instCategoryOver Functor.id Functor.comp Over.forget toOver Adjunction.unit forgetAdjToOver Over.homMk Functor.obj Comma.left Discrete discreteCategory Functor.fromPUnit CartesianMonoidalCategory.lift CategoryStruct.id Category.toCategoryStruct Comma.hom	—	—
toOverIsoToOverUnit_hom_app_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Functor.obj Over instCategoryOver toOver toOverUnit NatTrans.app Iso.hom Functor Functor.category toOverIsoToOverUnit CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Functor.comp Over.forget Equivalence.unit equivToOverUnit SemiCartesianMonoidalCategory.fst	—	Category.comp_id Category.id_comp
toOverIsoToOverUnit_inv_app_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Functor.obj Over instCategoryOver toOverUnit toOver NatTrans.app Iso.inv Functor Functor.category toOverIsoToOverUnit CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Functor.comp Over.forget Equivalence.counit equivToOverUnit MonoidalCategoryStruct.rightUnitor	—	Category.comp_id MonoidalCategory.whiskerRight_id Category.id_comp Iso.hom_inv_id CartesianMonoidalCategory.lift_rightUnitor_hom_assoc
toOverIteratedSliceForwardIsoPullback_hom_app_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit Comma.left Functor.obj Over instCategoryOver Functor.comp toOver ChosenPullbacksAlong.cartesianMonoidalCategoryOver Equivalence.inverse Equivalence.symm Over.iteratedSliceEquiv ChosenPullbacksAlong.pullback NatTrans.app Iso.hom Functor Functor.category Over.iteratedSliceForward toOverIteratedSliceForwardIsoPullback CategoryStruct.comp Category.toCategoryStruct ChosenPullbacksAlong.pullbackObj Comma.hom Over.map MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SemiCartesianMonoidalCategory.snd Adjunction.unit ChosenPullbacksAlong.mapPullbackAdj Functor.map Over.iteratedSliceBackward Equivalence.unitInv SemiCartesianMonoidalCategory.fst	—	Category.comp_id Functor.map_id Adjunction.comp_counit_app Functor.map_comp Category.id_comp
toOverIteratedSliceForwardIsoPullback_inv_app_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit Comma.left Functor.obj Over instCategoryOver ChosenPullbacksAlong.pullback Functor.comp toOver ChosenPullbacksAlong.cartesianMonoidalCategoryOver Equivalence.inverse Equivalence.symm Over.iteratedSliceEquiv NatTrans.app Iso.inv Functor Functor.category Over.iteratedSliceForward toOverIteratedSliceForwardIsoPullback CategoryStruct.comp Category.toCategoryStruct ChosenPullbacksAlong.pullbackObj Comma.hom Over.iteratedSliceBackward Equivalence.counitInv ChosenPullbacksAlong.lift CategoryStruct.id Quiver.Hom CategoryStruct.toQuiver Over.homMk Comma.right MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Over.map MonoidalCategoryStruct.whiskerRight Adjunction.counit ChosenPullbacksAlong.mapPullbackAdj	—	Adjunction.comp_unit_app Category.comp_id Category.id_comp Category.assoc
toOverPullbackIsoToOver_hom_app_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit Functor.obj Over instCategoryOver Functor.comp toOver ChosenPullbacksAlong.pullback NatTrans.app Iso.hom Functor Functor.category toOverPullbackIsoToOver CartesianMonoidalCategory.lift Comma.left CategoryStruct.comp Category.toCategoryStruct Over.forget Over.map Over.mapForget MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Adjunction.counit ChosenPullbacksAlong.mapPullbackAdj SemiCartesianMonoidalCategory.fst Comma.hom	—	Category.comp_id Category.id_comp Adjunction.comp_counit_app MonoidalCategory.comp_whiskerRight CartesianMonoidalCategory.lift_whiskerRight_assoc CartesianMonoidalCategory.lift_whiskerRight Category.assoc CartesianMonoidalCategory.comp_lift
toOverPullbackIsoToOver_inv_app_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit Functor.obj Over instCategoryOver toOver Functor.comp ChosenPullbacksAlong.pullback NatTrans.app Iso.inv Functor Functor.category toOverPullbackIsoToOver CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Comma.left Over.map Adjunction.unit ChosenPullbacksAlong.mapPullbackAdj Functor.map Over.homMk CartesianMonoidalCategory.lift CategoryStruct.id SemiCartesianMonoidalCategory.snd Quiver.Hom CategoryStruct.toQuiver Comma.hom Comma.right MonoidalCategoryStruct.whiskerRight Over.forget Over.mapForget SemiCartesianMonoidalCategory.fst	—	Adjunction.comp_unit_app Category.comp_id Category.id_comp toOver_map Category.assoc
toOverUnitPullback_hom_app_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit Functor.obj Over instCategoryOver Functor.comp MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toOverUnit ChosenPullbacksAlong.pullback SemiCartesianMonoidalCategory.toUnit ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit toOver NatTrans.app Iso.hom Functor Functor.category toOverUnitPullback CategoryStruct.id Category.toCategoryStruct MonoidalCategoryStruct.tensorObj	—	—
toOverUnitPullback_inv_app_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit Functor.obj Over instCategoryOver toOver Functor.comp MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toOverUnit ChosenPullbacksAlong.pullback SemiCartesianMonoidalCategory.toUnit ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit NatTrans.app Iso.inv Functor Functor.category toOverUnitPullback CategoryStruct.id Category.toCategoryStruct MonoidalCategoryStruct.tensorObj	—	—
toOverUnit_map_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SemiCartesianMonoidalCategory.toUnit Functor.map Over instCategoryOver toOverUnit	—	—
toOverUnit_obj_hom 📖	mathematical	—	Comma.hom Discrete discreteCategory Functor.id Functor.fromPUnit MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Functor.obj Over instCategoryOver toOverUnit SemiCartesianMonoidalCategory.toUnit	—	—
toOverUnit_obj_left 📖	mathematical	—	Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Functor.obj Over instCategoryOver toOverUnit	—	—
toOver_map 📖	mathematical	—	Functor.map Over instCategoryOver toOver Over.homMk Functor.obj MonoidalCategoryStruct.whiskerRight MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	—
toOver_map_left 📖	mathematical	—	CommaMorphism.left Discrete discreteCategory Functor.id Functor.fromPUnit MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SemiCartesianMonoidalCategory.snd Functor.map Over instCategoryOver toOver MonoidalCategoryStruct.whiskerRight	—	—
toOver_obj_hom 📖	mathematical	—	Comma.hom Discrete discreteCategory Functor.id Functor.fromPUnit Functor.obj Over instCategoryOver toOver SemiCartesianMonoidalCategory.snd CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	—
toOver_obj_left 📖	mathematical	—	Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit Functor.obj Over instCategoryOver toOver MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	—

CategoryTheory.ChosenPullbacksAlong

Definitions

Name	Category	Theorems
binaryFan 📖	CompOp	—
binaryFanIsBinaryProduct 📖	CompOp	—
cartesianMonoidalCategoryOver 📖	CompOp	48 math math: Over.whiskerLeft_left_fst, Over.associator_hom_left_snd_fst_assoc, Over.tensorHom_left_fst, Over.tensorObj_ext_iff, Over.tensorHom_left_snd_assoc, Over.rightUnitor_inv_left_snd, Over.tensorObj_hom, Over.tensorObj_left, Over.associator_hom_left_fst, Over.snd_eq_snd', Over.leftUnitor_inv_left_snd, Over.tensorUnit_hom, Over.whiskerLeft_left_snd_assoc, Over.associator_hom_left_snd_fst, Over.whiskerRight_left, Over.rightUnitor_inv_left_snd_assoc, Over.leftUnitor_inv_left_fst_assoc, Over.tensorUnit_left, Over.leftUnitor_inv_left_fst, Over.whiskerRight_left_snd, Over.whiskerRight_left_snd_assoc, Over.whiskerRight_left_fst_assoc, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, Over.whiskerLeft_left_fst_assoc, Over.tensorHom_left_fst_assoc, Over.associator_inv_left_fst_snd_assoc, Over.associator_inv_left_fst_snd, Over.whiskerRight_left_fst, Over.associator_inv_left_snd_assoc, Over.rightUnitor_hom_left, Over.leftUnitor_hom_left, Over.lift_left, Over.associator_inv_left_fst_fst, Over.whiskerLeft_left, Over.toUnit_left, Over.associator_inv_left_snd, Over.whiskerLeft_left_snd, Over.associator_hom_left_snd_snd, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, Over.fst_eq_fst', Over.leftUnitor_inv_left_snd_assoc, Over.rightUnitor_inv_left_fst_assoc, Over.rightUnitor_inv_left_fst, Over.associator_hom_left_fst_assoc, Over.tensorHom_left_snd, Over.associator_inv_left_fst_fst_assoc, Over.associator_hom_left_snd_snd_assoc, Over.tensorHom_left

CategoryTheory.ChosenPullbacksAlong.Over

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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.snd	—	CategoryTheory.CartesianMonoidalCategory.associator_hom_fst
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.snd	—	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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.ChosenPullbacksAlong.fst	—	CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.snd	—	CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.snd	—	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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.ChosenPullbacksAlong.snd	—	CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.ChosenPullbacksAlong.snd	—	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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.ChosenPullbacksAlong.snd	—	CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.CartesianMonoidalCategory.associator_inv_snd
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_left_snd
fst_eq_fst' 📖	mathematical	—	CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.ChosenPullbacksAlong.fst' CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Comma.hom	—	CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.CategoryStruct.id CategoryTheory.Comma.hom	—	CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.ChosenPullbacksAlong.lift CategoryTheory.Comma.left CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.Functor.obj CategoryTheory.Comma.right 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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_inv_left_snd
snd_eq_snd' 📖	mathematical	—	CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.ChosenPullbacksAlong.snd' CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit 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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ChosenPullbacksAlong.pullbackMap CategoryTheory.Functor.obj CategoryTheory.Comma.left 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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.pullbackObj	—	CategoryTheory.CartesianMonoidalCategory.tensorHom_fst
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.pullbackObj	—	CategoryTheory.CartesianMonoidalCategory.tensorHom_snd
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.snd	—	—	CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.ChosenPullbacksAlong.snd	—	—
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.ChosenPullbacksAlong.pullbackObj CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver 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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver	—	—
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver 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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.ChosenPullbacksAlong.pullbackMap 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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.pullbackObj	—	CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ChosenPullbacksAlong.pullbackMap CategoryTheory.Functor.obj CategoryTheory.Comma.left 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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ChosenPullbacksAlong.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.ChosenPullbacksAlong.pullbackObj	—	CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ChosenPullbacksAlong.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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.Functor.obj CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd
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 CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOver CategoryTheory.CommaMorphism.left CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ChosenPullbacksAlong.snd CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_left_snd

CategoryTheory.forgetAdjToOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homEquiv_symm 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Over CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.toOver CategoryTheory.Over.forget EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv CategoryTheory.forgetAdjToOver CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	CategoryTheory.Adjunction.homEquiv_counit CategoryTheory.forgetAdjToOver_counit_app

---

← Back to Index