Basic

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

Statistics

Metric	Count
Definitions adj, rightAdj, MonoidalClosed, closed, comp, compTranspose, curry, curry', curryHomEquiv', id, internalHom, internalHomAdjunction₂, ofEquiv, pre, uncurry, uncurry', unitIsoSelf, unitNatIso, ihom, adjunction, coev, ev, «term_⟶[_]_», tensorClosed, unitClosed	25
Theorems assoc, assoc_assoc, coev_app_comp_pre_app, coev_app_comp_pre_app_assoc, compTranspose_eq, comp_eq, comp_id, comp_id_assoc, curry'_comp, curry'_id, curry'_ihom_map, curry'_injective, curry'_uncurry', curry'_whiskerRight_comp, curry'_whiskerRight_comp_assoc, curryHomEquiv'_apply, curryHomEquiv'_symm_apply, curry_eq, curry_eq_iff, curry_id_eq_coev, curry_injective, curry_natural_left, curry_natural_left_assoc, curry_natural_right, curry_natural_right_assoc, curry_pre_app, curry_pre_app_assoc, curry_uncurry, eq_curry_iff, homEquiv_apply_eq, homEquiv_symm_apply_eq, id_comp, id_comp_assoc, id_eq, id_tensor_pre_app_comp_ev, id_tensor_pre_app_comp_ev_assoc, internalHomAdjunction₂_adj, internalHom_map, internalHom_obj, ofEquiv_curry_def, ofEquiv_uncurry_def, pre_comm_ihom_map, pre_id, pre_map, uncurry'_curry', uncurry'_injective, uncurry_curry, uncurry_eq, uncurry_id_eq_ev, uncurry_ihom_map, uncurry_injective, uncurry_natural_left, uncurry_natural_left_assoc, uncurry_natural_right, uncurry_natural_right_assoc, uncurry_pre, uncurry_pre_app, uncurry_pre_app_assoc, whiskerLeft_curry'_comp, whiskerLeft_curry'_comp_assoc, whiskerLeft_curry'_ihom_ev_app, whiskerLeft_curry'_ihom_ev_app_assoc, whiskerLeft_curry_ihom_ev_app, whiskerLeft_curry_ihom_ev_app_assoc, coev_ev, coev_ev_assoc, coev_naturality, coev_naturality_assoc, ev_coev, ev_coev_assoc, ev_naturality, ev_naturality_assoc, ihom_adjunction_counit, ihom_adjunction_unit, instIsLeftAdjointTensorLeft, instPreservesColimitsTensorLeft	76
Total	101

CategoryTheory

Definitions

Name	Category	Theorems
MonoidalClosed 📖	CompData	—
ihom 📖	CompOp	156 math math: MonoidalCategory.DayConvolutionInternalHom.hπ_assoc, ihom.coev_naturality, Rep.MonoidalClosed.linearHomEquiv_symm_hom, LightCondensed.ihomPoints_apply, LightCondensed.ihomPoints_symm_comp, MonoidalClosed.ofEquiv_uncurry_def, MonoidalClosed.uncurry_natural_right, ModuleCat.monoidalClosed_uncurry, Functor.closedIhom_obj_map, MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight, MonoidalClosed.coev_app_comp_pre_app, CartesianClosed.curry_id_eq_coev, MonoidalClosed.uncurry_natural_left_assoc, MonoidalClosed.uncurry_pre_app_assoc, coev_expComparison, MonoidalClosed.uncurry_natural_right_assoc, exp.coev_ev, frobeniusMorphism_mate, MonoidalClosedFunctor.comparison_iso, MonoidalClosed.uncurry_pre_app, ihom.ev_coev_assoc, Cat.ihom_obj, Rep.ihom_ev_app_hom, Rep.MonoidalClosed.linearHomEquivComm_hom, MonoidalClosed.uncurry_eq, MonoidalCategory.DayConvolutionInternalHom.coev_app_π_assoc, CartesianClosed.homEquiv_apply_eq, MonoidalClosed.whiskerLeft_curry'_comp, MonoidalClosed.whiskerLeft_curry'_ihom_ev_app_assoc, Rep.homEquiv_def, Pi.closedCounit_app, ModuleCat.monoidalClosed_curry, Pi.closedUnit_app, CartesianClosed.curry_natural_right_assoc, Functor.ihom_ev_app, MonoidalClosed.curry'_ihom_map, MonoidalClosed.assoc, CartesianClosed.curry_natural_left_assoc, coev_app_comp_pre_app, CartesianClosed.curry_natural_right, MonoidalClosed.assoc_assoc, MonoidalClosed.curry_id_eq_coev, expComparison_whiskerLeft, MonoidalClosed.uncurry_pre, Functor.ihom_map, CartesianClosed.curry_eq, MonoidalClosed.pre_comm_ihom_map, MonoidalClosed.id_tensor_pre_app_comp_ev, CartesianClosed.homEquiv_symm_apply_eq, MonoidalClosed.curry_pre_app, MonoidalCategory.DayConvolutionInternalHom.hπ, MonoidalCategory.DayConvolutionInternalHom.map_app_comp_π, MonoidalClosed.curry_eq, MonoidalClosed.curry_natural_left, CartesianClosed.uncurry_natural_right, MonoidalClosed.curry_pre_app_assoc, MonoidalClosed.comp_eq, Over.toOverSectionsAdj_counit_app, CartesianClosed.uncurry_eq, FGModuleCat.ihom_obj, pre_id, MonoidalClosed.curry'_comp, Over.sections_obj, ObjectProperty.ihom_obj, exp.ev_coev, MonoidalCategory.DayConvolutionInternalHom.map_comp_π_assoc, CartesianClosed.uncurry_id_eq_ev, MonoidalClosed.id_tensor_pre_app_comp_ev_assoc, uncurry_pre, ihom.coev_naturality_assoc, exp.ev_coev_assoc, CartesianClosed.uncurry_natural_left_assoc, MonoidalClosed.whiskerLeft_curry'_ihom_ev_app, Functor.closedUnit_app_app, MonoidalCategory.DayConvolutionInternalHom.map_comp_π, uncurry_expComparison, CartesianClosed.uncurry_natural_left, MonoidalClosed.uncurry_ihom_map, MonoidalClosed.uncurry_injective, MonoidalClosed.uncurry_id_eq_ev, ObjectProperty.ihom_map, Cat.ihom_map, Functor.ihom_coev_app, Monoidal.Reflective.instIsIsoAppUnitObjIhom, MonoidalClosed.pre_id, ModuleCat.ihom_map_apply, ModuleCat.ihom_coev_app, MonoidalClosed.curry_natural_left_assoc, CartesianClosed.uncurry_natural_right_assoc, ihom.ihom_adjunction_unit, MonoidalClosed.curry_natural_right_assoc, Functor.closedIhom_obj_obj, MonoidalClosed.comp_id_assoc, expComparison_ev, Functor.closedIhom_map_app, MonoidalClosed.uncurry_natural_left, MonoidalClosed.homEquiv_symm_apply_eq, ObjectProperty.IsMonoidalClosed.prop_ihom, LightCondensed.ihomPoints_symm_apply, exp.coev_ev_assoc, prod_map_pre_app_comp_ev, MonoidalClosed.curry'_whiskerRight_comp_assoc, MonoidalClosed.curry_injective, expComparison_iso_of_frobeniusMorphism_iso, LightCondensed.ihom_map_val_app, InternallyProjective.preserves_epi, MonoidalClosed.internalHom_obj, Rep.MonoidalClosed.linearHomEquiv_hom, MonoidalClosed.whiskerLeft_curry_ihom_ev_app, MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_map_app_app, ihom.ev_naturality, Pi.ihom_map, Over.sections_map, MonoidalClosed.curryHomEquiv'_symm_apply, MonoidalClosed.enrichedCategorySelf_hom, MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_map, CartesianClosed.uncurry_injective, ihom.ev_naturality_assoc, MonoidalClosed.homEquiv_apply_eq, MonoidalClosed.compTranspose_eq, ExponentialIdeal.exp_closed, Rep.ihom_coev_app_hom, MonoidalClosed.whiskerLeft_curry'_comp_assoc, Functor.closedCounit_app_app, pre_map, MonoidalClosed.pre_map, CartesianClosed.curry_natural_left, MonoidalClosed.curryHomEquiv'_apply, Pi.ihom_obj, MonoidalClosed.coev_app_comp_pre_app_assoc, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, CartesianClosed.curry_injective, MonoidalClosed.curry'_whiskerRight_comp, MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app, MonoidalClosed.ofEquiv_curry_def, MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft, ObjectProperty.prop_ihom, MonoidalClosed.curry_natural_right, MonoidalClosed.comp_id, MonoidalClosed.leftDistrib_inv, ModuleCat.monoidalClosed_pre_app, MonoidalCategory.DayConvolutionInternalHom.coev_app_π, Rep.ihom_obj_ρ_def, MonoidalClosed.id_comp, ihom.ihom_adjunction_counit, ObjectProperty.ihom_map_hom, MonoidalCategory.DayConvolutionInternalHom.map_app_comp_π_assoc, MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_obj, toUnit_comp_curryRightUnitorHom, ihom.ev_coev, ModuleCat.ihom_ev_app, MonoidalClosed.whiskerLeft_curry_ihom_ev_app_assoc, ihom.coev_ev_assoc, MonoidalClosed.id_comp_assoc, MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_map_app_app_app, ihom.coev_ev
tensorClosed 📖	CompOp	—
unitClosed 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesColimitsTensorLeft 📖	mathematical	—	Limits.PreservesColimits MonoidalCategory.tensorLeft	—	Adjunction.leftAdjoint_preservesColimits

CategoryTheory.Closed

Definitions

Name	Category	Theorems
adj 📖	CompOp	3 math math: CategoryTheory.Pi.monoidalClosed_closed_adj_counit, CategoryTheory.Pi.monoidalClosed_closed_adj_unit, CategoryTheory.Functor.monoidalClosed_closed_adj
rightAdj 📖	CompOp	1 math math: CategoryTheory.Pi.monoidalClosed_closed_rightAdj

CategoryTheory.MonoidalClosed

Definitions

Name	Category	Theorems
closed 📖	CompOp	75 math math: CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ_assoc, Rep.MonoidalClosed.linearHomEquiv_symm_hom, LightCondensed.ihomPoints_apply, internalHomAdjunction₂_adj, enrichedOrdinaryCategorySelf_homEquiv_symm, LightCondensed.ihomPoints_symm_comp, ofEquiv_uncurry_def, ModuleCat.monoidalClosed_uncurry, CategoryTheory.Functor.closedIhom_obj_map, enrichedOrdinaryCategorySelf_eHomWhiskerRight, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app_assoc, CategoryTheory.coev_expComparison, CategoryTheory.frobeniusMorphism_mate, CategoryTheory.MonoidalClosedFunctor.comparison_iso, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app, Rep.ihom_ev_app_hom, Rep.MonoidalClosed.linearHomEquivComm_hom, enrichedCategorySelf_comp, CategoryTheory.Pi.monoidalClosed_closed_adj_counit, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π_assoc, enrichedCategorySelf_id, Rep.homEquiv_def, CategoryTheory.Pi.closedCounit_app, ModuleCat.monoidalClosed_curry, CategoryTheory.Pi.closedUnit_app, CategoryTheory.expComparison_whiskerLeft, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_app_comp_π, CategoryTheory.Pi.monoidalClosed_closed_rightAdj, FGModuleCat.ihom_obj, enrichedOrdinaryCategorySelf_homEquiv, CategoryTheory.ObjectProperty.ihom_obj, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_comp_π_assoc, CategoryTheory.Functor.closedUnit_app_app, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_comp_π, CategoryTheory.uncurry_expComparison, CategoryTheory.ObjectProperty.ihom_map, CategoryTheory.Monoidal.Reflective.instIsIsoAppUnitObjIhom, ModuleCat.ihom_map_apply, ModuleCat.ihom_coev_app, CategoryTheory.Functor.closedIhom_obj_obj, CategoryTheory.expComparison_ev, CategoryTheory.Functor.closedIhom_map_app, CategoryTheory.ObjectProperty.IsMonoidalClosed.prop_ihom, LightCondensed.ihomPoints_symm_apply, CategoryTheory.Pi.monoidalClosed_closed_adj_unit, CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso, LightCondensed.ihom_map_val_app, CategoryTheory.InternallyProjective.preserves_epi, internalHom_map, internalHom_obj, Rep.MonoidalClosed.linearHomEquiv_hom, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_map_app_app, CategoryTheory.Pi.ihom_map, enrichedCategorySelf_hom, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_map, CategoryTheory.ExponentialIdeal.exp_closed, Rep.ihom_coev_app_hom, CategoryTheory.Functor.closedCounit_app_app, CategoryTheory.Pi.ihom_obj, CategoryTheory.Functor.monoidalClosed_closed_adj, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app, ofEquiv_curry_def, enrichedOrdinaryCategorySelf_eHomWhiskerLeft, CategoryTheory.ObjectProperty.prop_ihom, leftDistrib_inv, ModuleCat.monoidalClosed_pre_app, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π, Rep.ihom_obj_ρ_def, CategoryTheory.ObjectProperty.ihom_map_hom, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_app_comp_π_assoc, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_obj, ModuleCat.ihom_ev_app, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_map_app_app_app
comp 📖	CompOp	13 math math: enrichedCategorySelf_comp, whiskerLeft_curry'_comp, assoc, assoc_assoc, comp_eq, curry'_comp, comp_id_assoc, curry'_whiskerRight_comp_assoc, whiskerLeft_curry'_comp_assoc, curry'_whiskerRight_comp, comp_id, id_comp, id_comp_assoc
compTranspose 📖	CompOp	2 math math: comp_eq, compTranspose_eq
curry 📖	CompOp	37 math math: CategoryTheory.CartesianClosed.curry_id_eq_coev, CategoryTheory.CartesianClosed.eq_curry_iff, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π_assoc, CategoryTheory.CartesianClosed.homEquiv_apply_eq, ModuleCat.monoidalClosed_curry, CategoryTheory.CartesianClosed.curry_natural_right_assoc, CategoryTheory.CartesianClosed.curry_natural_left_assoc, CategoryTheory.CartesianClosed.curry_natural_right, id_eq, curry_id_eq_coev, CategoryTheory.CartesianClosed.curry_eq_iff, CategoryTheory.CartesianClosed.curry_eq, curry_pre_app, uncurry_curry, curry_eq, curry_natural_left, curry_pre_app_assoc, comp_eq, curry_eq_iff, eq_curry_iff, CategoryTheory.CartesianClosed.uncurry_curry, CategoryTheory.CartesianClosed.curry_uncurry, curry_natural_left_assoc, curry_natural_right_assoc, LightCondensed.ihomPoints_symm_apply, curry_injective, whiskerLeft_curry_ihom_ev_app, homEquiv_apply_eq, CategoryTheory.CartesianClosed.curry_natural_left, CategoryTheory.CartesianClosed.curry_injective, ofEquiv_curry_def, curry_natural_right, curry_uncurry, leftDistrib_inv, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π, CategoryTheory.toUnit_comp_curryRightUnitorHom, whiskerLeft_curry_ihom_ev_app_assoc
curry' 📖	CompOp	13 math math: curry'_uncurry', whiskerLeft_curry'_comp, whiskerLeft_curry'_ihom_ev_app_assoc, curry'_ihom_map, curry'_comp, enrichedOrdinaryCategorySelf_homEquiv, whiskerLeft_curry'_ihom_ev_app, curry'_whiskerRight_comp_assoc, whiskerLeft_curry'_comp_assoc, curryHomEquiv'_apply, curry'_id, curry'_whiskerRight_comp, uncurry'_curry'
curryHomEquiv' 📖	CompOp	2 math math: curryHomEquiv'_symm_apply, curryHomEquiv'_apply
id 📖	CompOp	7 math math: enrichedCategorySelf_id, id_eq, comp_id_assoc, curry'_id, comp_id, id_comp, id_comp_assoc
internalHom 📖	CompOp	7 math math: internalHomAdjunction₂_adj, CategoryTheory.Functor.closedIhom_map_app, internalHom_map, internalHom_obj, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_map_app_app, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_map_app_app_app
internalHomAdjunction₂ 📖	CompOp	1 math math: internalHomAdjunction₂_adj
ofEquiv 📖	CompOp	2 math math: ofEquiv_uncurry_def, ofEquiv_curry_def
pre 📖	CompOp	27 math math: CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ_assoc, CategoryTheory.Functor.closedIhom_obj_map, enrichedOrdinaryCategorySelf_eHomWhiskerRight, coev_app_comp_pre_app, uncurry_pre_app_assoc, uncurry_pre_app, CategoryTheory.coev_app_comp_pre_app, CategoryTheory.expComparison_whiskerLeft, uncurry_pre, pre_comm_ihom_map, id_tensor_pre_app_comp_ev, curry_pre_app, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ, curry_pre_app_assoc, CategoryTheory.pre_id, id_tensor_pre_app_comp_ev_assoc, CategoryTheory.uncurry_pre, pre_id, CategoryTheory.prod_map_pre_app_comp_ev, curry'_whiskerRight_comp_assoc, internalHom_map, CategoryTheory.pre_map, pre_map, coev_app_comp_pre_app_assoc, curry'_whiskerRight_comp, CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app, ModuleCat.monoidalClosed_pre_app
uncurry 📖	CompOp	36 math math: LightCondensed.ihomPoints_apply, ofEquiv_uncurry_def, uncurry_natural_right, ModuleCat.monoidalClosed_uncurry, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app_assoc, uncurry_natural_left_assoc, uncurry_pre_app_assoc, uncurry_natural_right_assoc, CategoryTheory.CartesianClosed.eq_curry_iff, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app, uncurry_pre_app, uncurry_eq, CategoryTheory.CartesianClosed.curry_eq_iff, uncurry_pre, CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq, uncurry_curry, CategoryTheory.CartesianClosed.uncurry_natural_right, CategoryTheory.CartesianClosed.uncurry_eq, curry_eq_iff, eq_curry_iff, CategoryTheory.CartesianClosed.uncurry_curry, CategoryTheory.CartesianClosed.uncurry_id_eq_ev, CategoryTheory.uncurry_pre, CategoryTheory.CartesianClosed.uncurry_natural_left_assoc, CategoryTheory.uncurry_expComparison, CategoryTheory.CartesianClosed.uncurry_natural_left, uncurry_ihom_map, uncurry_injective, uncurry_id_eq_ev, CategoryTheory.CartesianClosed.curry_uncurry, CategoryTheory.CartesianClosed.uncurry_natural_right_assoc, uncurry_natural_left, homEquiv_symm_apply_eq, CategoryTheory.CartesianClosed.uncurry_injective, curry_uncurry, leftDistrib_inv
uncurry' 📖	CompOp	4 math math: enrichedOrdinaryCategorySelf_homEquiv_symm, curry'_uncurry', curryHomEquiv'_symm_apply, uncurry'_curry'
unitIsoSelf 📖	CompOp	—
unitNatIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight comp CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	uncurry_injective uncurry_natural_left uncurry_curry CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc uncurry_eq CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.pentagon_inv_assoc CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.Iso.hom_inv_id_assoc
assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight comp CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' assoc
coev_app_comp_pre_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.ihom.coev pre CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.unit_conjugateEquiv
coev_app_comp_pre_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.ihom.coev CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct pre CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coev_app_comp_pre_app
compTranspose_eq 📖	mathematical	—	compTranspose CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.NatTrans.app CategoryTheory.ihom.ev	—	—
comp_eq 📖	mathematical	—	comp curry CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom compTranspose	—	—
comp_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft id comp CategoryTheory.CategoryStruct.id	—	uncurry_injective uncurry_natural_left comp_eq uncurry_curry compTranspose_eq CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv_assoc CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc uncurry_id_eq_ev CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id
comp_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft id comp	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' comp_id
curry'_comp 📖	mathematical	—	curry' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom comp	—	CategoryTheory.MonoidalCategory.tensorHom_def_assoc whiskerLeft_curry'_comp CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.unitors_equal curry'_ihom_map
curry'_id 📖	mathematical	—	curry' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct id	—	CategoryTheory.Category.comp_id
curry'_ihom_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom curry' CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc
curry'_injective 📖	—	curry'	—	—	Equiv.injective
curry'_uncurry' 📖	mathematical	—	curry' uncurry'	—	CategoryTheory.Iso.hom_inv_id_assoc curry_uncurry
curry'_whiskerRight_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.whiskerRight curry' comp CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.NatTrans.app pre	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc uncurry_injective uncurry_pre comp_eq curry_natural_left uncurry_curry compTranspose_eq CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc whiskerLeft_curry'_ihom_ev_app CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_assoc CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc
curry'_whiskerRight_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.whiskerRight curry' comp CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.NatTrans.app pre	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' curry'_whiskerRight_comp
curryHomEquiv'_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom EquivLike.toFunLike Equiv.instEquivLike curryHomEquiv' curry'	—	—
curryHomEquiv'_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm curryHomEquiv' uncurry'	—	—
curry_eq 📖	mathematical	—	curry CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom CategoryTheory.NatTrans.app CategoryTheory.ihom.coev CategoryTheory.Functor.map	—	—
curry_eq_iff 📖	mathematical	—	curry uncurry	—	CategoryTheory.Adjunction.homEquiv_apply_eq
curry_id_eq_coev 📖	mathematical	—	curry CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom CategoryTheory.ihom.coev	—	curry_eq CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
curry_injective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom curry	—	Equiv.injective
curry_natural_left 📖	mathematical	—	curry CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.obj CategoryTheory.ihom	—	CategoryTheory.Adjunction.homEquiv_naturality_left
curry_natural_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom curry CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' curry_natural_left
curry_natural_right 📖	mathematical	—	curry CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.map	—	CategoryTheory.Adjunction.homEquiv_naturality_right
curry_natural_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom curry CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' curry_natural_right
curry_pre_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom curry CategoryTheory.NatTrans.app pre CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	uncurry_injective uncurry_curry uncurry_eq CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Category.assoc id_tensor_pre_app_comp_ev CategoryTheory.MonoidalCategory.whisker_exchange_assoc whiskerLeft_curry_ihom_ev_app
curry_pre_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom curry CategoryTheory.NatTrans.app pre CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' curry_pre_app
curry_uncurry 📖	mathematical	—	curry uncurry	—	Equiv.right_inv
eq_curry_iff 📖	mathematical	—	curry uncurry	—	CategoryTheory.Adjunction.eq_homEquiv_apply
homEquiv_apply_eq 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv CategoryTheory.ihom.adjunction curry	—	—
homEquiv_symm_apply_eq 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategory.tensorLeft EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv CategoryTheory.ihom.adjunction uncurry	—	—
id_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight id comp CategoryTheory.CategoryStruct.id	—	uncurry_injective uncurry_natural_left comp_eq uncurry_curry id_eq compTranspose_eq CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc uncurry_eq CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_assoc CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc uncurry_id_eq_ev
id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight id comp	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' id_comp
id_eq 📖	mathematical	—	id curry CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
id_tensor_pre_app_comp_ev 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.NatTrans.app pre CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom.ev CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.conjugateEquiv_counit
id_tensor_pre_app_comp_ev_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.NatTrans.app pre CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.id CategoryTheory.ihom.ev CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' id_tensor_pre_app_comp_ev
internalHomAdjunction₂_adj 📖	mathematical	—	CategoryTheory.ParametrizedAdjunction.adj CategoryTheory.MonoidalCategory.curriedTensor internalHom internalHomAdjunction₂ CategoryTheory.ihom.adjunction closed	—	—
internalHom_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category internalHom pre Opposite.unop closed Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
internalHom_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category internalHom CategoryTheory.ihom Opposite.unop closed	—	—
ofEquiv_curry_def 📖	mathematical	—	curry closed ofEquiv DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm CategoryTheory.Adjunction.toEquivalence CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful CategoryTheory.Functor.IsEquivalence.full CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.toAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.compInverseIso CategoryTheory.Functor.Monoidal.commTensorLeft	—	CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful CategoryTheory.Functor.IsEquivalence.full CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv CategoryTheory.Adjunction.comp_homEquiv
ofEquiv_uncurry_def 📖	mathematical	—	uncurry closed ofEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Adjunction.toEquivalence CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful CategoryTheory.Functor.IsEquivalence.full CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Functor.id CategoryTheory.Adjunction.counit CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.compInverseIso CategoryTheory.Functor.Monoidal.commTensorLeft DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Equivalence.symm CategoryTheory.Equivalence.functor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv CategoryTheory.Equivalence.toAdjunction CategoryTheory.ihom	—	CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful CategoryTheory.Functor.IsEquivalence.full CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Adjunction.instIsIsoFunctorCounitOfIsEquivalence CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv CategoryTheory.Adjunction.comp_homEquiv
pre_comm_ihom_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.NatTrans.app pre CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality
pre_id 📖	mathematical	—	pre CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.ihom	—	pre.eq_1 CategoryTheory.Functor.map_id CategoryTheory.conjugateEquiv_id
pre_map 📖	mathematical	—	pre CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.ihom	—	pre.eq_1 CategoryTheory.conjugateEquiv_comp CategoryTheory.Functor.map_comp
uncurry'_curry' 📖	mathematical	—	uncurry' curry'	—	uncurry_curry CategoryTheory.Iso.inv_hom_id_assoc
uncurry'_injective 📖	—	uncurry'	—	—	Equiv.injective
uncurry_curry 📖	mathematical	—	uncurry curry	—	Equiv.left_inv
uncurry_eq 📖	mathematical	—	uncurry CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom.ev	—	—
uncurry_id_eq_ev 📖	mathematical	—	uncurry CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.id CategoryTheory.ihom.ev	—	uncurry_eq CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp
uncurry_ihom_map 📖	mathematical	—	uncurry CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.ihom.ev	—	curry_injective curry_uncurry curry_natural_right uncurry_id_eq_ev CategoryTheory.Category.id_comp
uncurry_injective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct uncurry	—	Equiv.injective
uncurry_natural_left 📖	mathematical	—	uncurry CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Adjunction.homEquiv_naturality_left_symm
uncurry_natural_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct uncurry CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' uncurry_natural_left
uncurry_natural_right 📖	mathematical	—	uncurry CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	CategoryTheory.Adjunction.homEquiv_naturality_right_symm
uncurry_natural_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct uncurry CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' uncurry_natural_right
uncurry_pre 📖	mathematical	—	uncurry CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.NatTrans.app pre CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom.ev	—	uncurry_eq id_tensor_pre_app_comp_ev
uncurry_pre_app 📖	mathematical	—	uncurry CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.NatTrans.app pre CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	curry_injective curry_uncurry curry_pre_app
uncurry_pre_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct uncurry CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.NatTrans.app pre CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' uncurry_pre_app
whiskerLeft_curry'_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft curry' comp CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc uncurry_injective uncurry_ihom_map comp_eq curry_natural_left uncurry_curry compTranspose_eq CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc CategoryTheory.MonoidalCategory.whisker_exchange_assoc whiskerLeft_curry'_ihom_ev_app CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv CategoryTheory.MonoidalCategory.whiskerRight_id_assoc CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc
whiskerLeft_curry'_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft curry' comp CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_curry'_comp
whiskerLeft_curry'_ihom_ev_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.whiskerLeft curry' CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom.ev CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	whiskerLeft_curry_ihom_ev_app
whiskerLeft_curry'_ihom_ev_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.whiskerLeft curry' CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.id CategoryTheory.ihom.ev CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_curry'_ihom_ev_app
whiskerLeft_curry_ihom_ev_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.whiskerLeft curry CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom.ev	—	CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Category.assoc CategoryTheory.ihom.ev_naturality CategoryTheory.ihom.ev_coev_assoc
whiskerLeft_curry_ihom_ev_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.whiskerLeft curry CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.id CategoryTheory.ihom.ev	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_curry_ihom_ev_app

CategoryTheory.ihom

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	9 math math: CategoryTheory.MonoidalClosed.internalHomAdjunction₂_adj, CategoryTheory.frobeniusMorphism_mate, CategoryTheory.CartesianClosed.homEquiv_apply_eq, Rep.homEquiv_def, CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq, ihom_adjunction_unit, CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq, CategoryTheory.MonoidalClosed.homEquiv_apply_eq, ihom_adjunction_counit
coev 📖	CompOp	24 math math: coev_naturality, CategoryTheory.MonoidalClosed.coev_app_comp_pre_app, CategoryTheory.CartesianClosed.curry_id_eq_coev, CategoryTheory.coev_expComparison, CategoryTheory.exp.coev_ev, ev_coev_assoc, CategoryTheory.Pi.closedUnit_app, CategoryTheory.coev_app_comp_pre_app, CategoryTheory.MonoidalClosed.curry_id_eq_coev, CategoryTheory.CartesianClosed.curry_eq, CategoryTheory.MonoidalClosed.curry_eq, CategoryTheory.exp.ev_coev, coev_naturality_assoc, CategoryTheory.exp.ev_coev_assoc, CategoryTheory.Functor.closedUnit_app_app, CategoryTheory.Functor.ihom_coev_app, ModuleCat.ihom_coev_app, ihom_adjunction_unit, CategoryTheory.exp.coev_ev_assoc, Rep.ihom_coev_app_hom, CategoryTheory.MonoidalClosed.coev_app_comp_pre_app_assoc, ev_coev, coev_ev_assoc, coev_ev
ev 📖	CompOp	33 math math: CategoryTheory.exp.coev_ev, ev_coev_assoc, Rep.ihom_ev_app_hom, CategoryTheory.MonoidalClosed.uncurry_eq, CategoryTheory.MonoidalClosed.whiskerLeft_curry'_ihom_ev_app_assoc, CategoryTheory.Pi.closedCounit_app, CategoryTheory.Functor.ihom_ev_app, CategoryTheory.MonoidalClosed.uncurry_pre, CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev, CategoryTheory.CartesianClosed.uncurry_eq, CategoryTheory.exp.ev_coev, CategoryTheory.CartesianClosed.uncurry_id_eq_ev, CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev_assoc, CategoryTheory.uncurry_pre, CategoryTheory.exp.ev_coev_assoc, CategoryTheory.MonoidalClosed.whiskerLeft_curry'_ihom_ev_app, CategoryTheory.uncurry_expComparison, CategoryTheory.MonoidalClosed.uncurry_ihom_map, CategoryTheory.MonoidalClosed.uncurry_id_eq_ev, CategoryTheory.expComparison_ev, CategoryTheory.exp.coev_ev_assoc, CategoryTheory.prod_map_pre_app_comp_ev, CategoryTheory.MonoidalClosed.whiskerLeft_curry_ihom_ev_app, ev_naturality, ev_naturality_assoc, CategoryTheory.MonoidalClosed.compTranspose_eq, CategoryTheory.Functor.closedCounit_app_app, ihom_adjunction_counit, ev_coev, ModuleCat.ihom_ev_app, CategoryTheory.MonoidalClosed.whiskerLeft_curry_ihom_ev_app_assoc, coev_ev_assoc, coev_ev
«term_⟶[_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coev_ev 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.ihom CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.NatTrans.app coev CategoryTheory.Functor.map ev CategoryTheory.CategoryStruct.id	—	CategoryTheory.Adjunction.right_triangle_components
coev_ev_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp coev CategoryTheory.Functor.map ev	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' coev_ev
coev_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom CategoryTheory.NatTrans.app CategoryTheory.Functor.id coev CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.NatTrans.naturality
coev_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp coev CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coev_naturality
ev_coev 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.NatTrans.app coev ev CategoryTheory.CategoryStruct.id	—	CategoryTheory.Adjunction.left_triangle_components
ev_coev_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp coev ev	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ev_coev
ev_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.Functor.id CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft ev	—	CategoryTheory.NatTrans.naturality
ev_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Functor.id ev	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ev_naturality
ihom_adjunction_counit 📖	mathematical	—	CategoryTheory.Adjunction.counit CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom adjunction ev	—	—
ihom_adjunction_unit 📖	mathematical	—	CategoryTheory.Adjunction.unit CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.ihom adjunction coev	—	—
instIsLeftAdjointTensorLeft 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.MonoidalCategory.tensorLeft	—	CategoryTheory.Adjunction.isLeftAdjoint

---

← Back to Index