Currying

📁 Source: Mathlib/CategoryTheory/Functor/Currying.lean

Statistics

Metric	Count
Definitions compFlipUncurryIso, curry, curryObj, curryObjCompIso, curryObjProdComp, currying, curryingEquiv, curryingFlipEquiv, flipIsoCurrySwapUncurry, flipping, flippingEquiv, fullyFaithfulCurry, fullyFaithfulUncurry, uncurry, uncurryObjFlip, whiskeringRight₂	16
Theorems compFlipUncurryIso_hom_app, compFlipUncurryIso_inv_app, comp_flip_uncurry_eq, curryObjCompIso_hom_app_app, curryObjCompIso_inv_app_app, curryObjProdComp_hom_app_app, curryObjProdComp_inv_app_app, curry_map_app_app, curry_obj_comp_flip, curry_obj_injective, curry_obj_map_app, curry_obj_obj_map, curry_obj_obj_obj, curry_obj_uncurry_obj, curryingEquiv_apply_map, curryingEquiv_apply_obj, curryingEquiv_symm_apply_map_app, curryingEquiv_symm_apply_obj_map, curryingEquiv_symm_apply_obj_obj, curryingFlipEquiv_apply_map, curryingFlipEquiv_apply_obj, curryingFlipEquiv_symm_apply_map_app, curryingFlipEquiv_symm_apply_obj_map, curryingFlipEquiv_symm_apply_obj_obj, currying_counitIso_hom_app_app, currying_counitIso_inv_app_app, currying_functor_map_app, currying_functor_obj_map, currying_functor_obj_obj, currying_inverse_map_app_app, currying_inverse_obj_map_app, currying_inverse_obj_obj_map, currying_inverse_obj_obj_obj, currying_unitIso_hom_app_app_app, currying_unitIso_inv_app_app_app, flipIsoCurrySwapUncurry_hom_app_app, flipIsoCurrySwapUncurry_inv_app_app, flip_flip, flip_injective, flippingEquiv_apply_map_app, flippingEquiv_apply_obj_map, flippingEquiv_apply_obj_obj, flippingEquiv_symm_apply_map_app, flippingEquiv_symm_apply_obj_map, flippingEquiv_symm_apply_obj_obj, flipping_counitIso_hom_app_app_app, flipping_counitIso_inv_app_app_app, flipping_functor_map_app_app, flipping_functor_obj_map_app, flipping_functor_obj_obj_map, flipping_functor_obj_obj_obj, flipping_inverse_map_app_app, flipping_inverse_obj_map_app, flipping_inverse_obj_obj_map, flipping_inverse_obj_obj_obj, flipping_unitIso_hom_app_app_app, flipping_unitIso_inv_app_app_app, instFaithfulProdCurry, instFaithfulProdUncurry, instFullProdCurry, instFullProdUncurry, uncurryObjFlip_hom_app, uncurryObjFlip_inv_app, uncurry_map_app, uncurry_obj_curry_obj, uncurry_obj_curry_obj_flip_flip, uncurry_obj_curry_obj_flip_flip', uncurry_obj_injective, uncurry_obj_map, uncurry_obj_obj, whiskeringRight₂_map_app_app_app, whiskeringRight₂_obj_map_app_app, whiskeringRight₂_obj_obj_map_app, whiskeringRight₂_obj_obj_obj_map, whiskeringRight₂_obj_obj_obj_obj	75
Total	91

CategoryTheory.Functor

Definitions

Name	Category	Theorems
compFlipUncurryIso 📖	CompOp	2 math math: compFlipUncurryIso_inv_app, compFlipUncurryIso_hom_app
curry 📖	CompOp	58 math math: CategoryTheory.Limits.map_id_right_eq_curry_swap_map, CategoryTheory.Limits.colimitLimitToLimitColimit_isIso, curryObjCompIso_hom_app_app, curry_obj_obj_obj, CategoryTheory.Limits.coconeOfCoconeCurry_pt, CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π_assoc, curry_obj_uncurry_obj, CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom, CategoryTheory.Limits.colimitIsoSwapCompColim_hom_app, currying_counitIso_hom_app_app, CategoryTheory.IsSifted.factorization_prodComparison_colim, CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom_assoc, CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv, instFaithfulProdCurry, curryObjProdComp_hom_app_app, uncurry_obj_curry_obj, CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π, CategoryTheory.Limits.limitIsoSwapCompLim_hom_app, CategoryTheory.Limits.coneOfConeCurry_pt, currying_counitIso_inv_app_app, CategoryTheory.Limits.map_id_left_eq_curry_map, CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π, CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, CategoryTheory.Limits.coneOfConeCurry_π_app, CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv_assoc, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂, CategoryTheory.Limits.colimitIsoSwapCompColim_inv_app, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁, flipIsoCurrySwapUncurry_hom_app_app, whiskeringRight₂_map_app_app_app, CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π, curryObjCompIso_inv_app_app, currying_unitIso_inv_app_app_app, currying_unitIso_hom_app_app_app, CategoryTheory.Limits.limitIsoSwapCompLim_inv_app, curry_obj_obj_map, instFullProdCurry, CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π, CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply, CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π_assoc, CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π, curry_obj_map_app, uncurry_obj_curry_obj_flip_flip', CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv, curryObjProdComp_inv_app_app, flipIsoCurrySwapUncurry_inv_app_app, bifunctorComp₁₂Iso_inv_app_app_app, bifunctorComp₁₂Iso_hom_app_app_app, bifunctorComp₂₃Iso_hom_app_app_app, CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_assoc, curry_map_app_app, CategoryTheory.Limits.coconeOfCoconeCurry_ι_app, curry_obj_comp_flip, CategoryTheory.Limits.colimitLimitToLimitColimit_injective, bifunctorComp₂₃Iso_inv_app_app_app, CategoryTheory.Limits.colimitLimitToLimitColimit_surjective, uncurry_obj_curry_obj_flip_flip
curryObj 📖	CompOp	4 math math: whiskeringRight₂_map_app_app_app, CategoryTheory.curryingIso_inv_toFunctor_map_app_app, curry_map_app_app, currying_inverse_map_app_app
curryObjCompIso 📖	CompOp	2 math math: curryObjCompIso_hom_app_app, curryObjCompIso_inv_app_app
curryObjProdComp 📖	CompOp	2 math math: curryObjProdComp_hom_app_app, curryObjProdComp_inv_app_app
currying 📖	CompOp	12 math math: currying_inverse_obj_obj_obj, currying_counitIso_hom_app_app, currying_inverse_obj_obj_map, currying_counitIso_inv_app_app, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, currying_unitIso_inv_app_app_app, currying_unitIso_hom_app_app_app, currying_functor_obj_obj, currying_functor_obj_map, currying_functor_map_app, currying_inverse_map_app_app, currying_inverse_obj_map_app
curryingEquiv 📖	CompOp	6 math math: curryingEquiv_symm_apply_obj_obj, curryingFlipEquiv_symm_apply_map_app, curryingEquiv_apply_obj, curryingEquiv_symm_apply_map_app, curryingEquiv_apply_map, curryingEquiv_symm_apply_obj_map
curryingFlipEquiv 📖	CompOp	5 math math: curryingFlipEquiv_symm_apply_map_app, curryingFlipEquiv_apply_obj, curryingFlipEquiv_symm_apply_obj_map, curryingFlipEquiv_apply_map, curryingFlipEquiv_symm_apply_obj_obj
flipIsoCurrySwapUncurry 📖	CompOp	6 math math: CategoryTheory.Limits.colimitIsoSwapCompColim_hom_app, CategoryTheory.Limits.limitIsoSwapCompLim_hom_app, CategoryTheory.Limits.colimitIsoSwapCompColim_inv_app, flipIsoCurrySwapUncurry_hom_app_app, CategoryTheory.Limits.limitIsoSwapCompLim_inv_app, flipIsoCurrySwapUncurry_inv_app_app
flipping 📖	CompOp	12 math math: flipping_functor_map_app_app, flipping_inverse_obj_obj_map, flipping_counitIso_inv_app_app_app, flipping_counitIso_hom_app_app_app, flipping_unitIso_hom_app_app_app, flipping_functor_obj_map_app, flipping_unitIso_inv_app_app_app, flipping_inverse_obj_map_app, flipping_functor_obj_obj_obj, flipping_inverse_map_app_app, flipping_functor_obj_obj_map, flipping_inverse_obj_obj_obj
flippingEquiv 📖	CompOp	6 math math: flippingEquiv_symm_apply_map_app, flippingEquiv_symm_apply_obj_obj, flippingEquiv_symm_apply_obj_map, flippingEquiv_apply_obj_map, flippingEquiv_apply_map_app, flippingEquiv_apply_obj_obj
fullyFaithfulCurry 📖	CompOp	—
fullyFaithfulUncurry 📖	CompOp	—
uncurry 📖	CompOp	71 math math: whiskeringRight₂_obj_obj_map_app, CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv, uncurryObjFlip_hom_app, CategoryTheory.MonoidalCategory.externalProductBifunctor_map_app, curry_obj_uncurry_obj, CategoryTheory.Limits.colimitIsoSwapCompColim_hom_app, currying_counitIso_hom_app_app, CategoryTheory.IsSifted.factorization_prodComparison_colim, CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv_assoc, CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsColimit_inv_comp_map_π, comp_flip_uncurry_eq, uncurry_obj_curry_obj, CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv, CategoryTheory.Limits.limitIsoSwapCompLim_hom_app, CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom_assoc, CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom, compFlipUncurryIso_inv_app, currying_counitIso_inv_app_app, uncurry_map_app, CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoObjConePointsOfIsColimit_hom, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit_hom_comp_π, instFaithfulProdUncurry, CategoryTheory.Limits.colimitIsoSwapCompColim_inv_app, uncurry_obj_obj, CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoObjConePointsOfIsColimit_hom_assoc, uncurryObjFlip_inv_app, CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsColimit_inv_comp_map_π_assoc, CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π, mapCone₂_pt, CategoryTheory.Limits.PreservesLimit₂.nonempty_isLimit_mapCone₂, flipIsoCurrySwapUncurry_hom_app_app, mapCone₂_π_app, instFullProdUncurry, whiskeringRight₂_map_app_app_app, CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit_hom_comp_π_assoc, CategoryTheory.Limits.coneOfConeUncurry_π_app, CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_inv_comp_π, currying_unitIso_inv_app_app_app, currying_unitIso_hom_app_app_app, mapCocone₂_pt, uncurry_obj_map, closedIhom_map_app, mapCocone₂_ι_app, CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π_assoc, CategoryTheory.Limits.limitIsoSwapCompLim_inv_app, CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_inv_comp_π_assoc, CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoObjConePointsOfIsColimit_inv, CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π, CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π_assoc, CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoColimitUncurryWhiskeringLeft₂_hom_assoc, CategoryTheory.Limits.coconeOfCoconeUncurry_pt, CategoryTheory.Limits.coconeOfCoconeUncurry_ι_app, uncurry_obj_curry_obj_flip_flip', CategoryTheory.Limits.coneOfConeUncurry_pt, CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π, flipIsoCurrySwapUncurry_inv_app_app, bifunctorComp₁₂Iso_inv_app_app_app, bifunctorComp₁₂Iso_hom_app_app_app, bifunctorComp₂₃Iso_hom_app_app_app, CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoObjConePointsOfIsColimit_inv_assoc, CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoColimitUncurryWhiskeringLeft₂_hom, CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂, CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π_assoc, CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂, whiskeringRight₂_obj_map_app_app, compFlipUncurryIso_hom_app, CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc, bifunctorComp₂₃Iso_inv_app_app_app, CategoryTheory.Limits.PreservesColimit₂.nonempty_isColimit_mapCocone₂, uncurry_obj_curry_obj_flip_flip
uncurryObjFlip 📖	CompOp	2 math math: uncurryObjFlip_hom_app, uncurryObjFlip_inv_app
whiskeringRight₂ 📖	CompOp	5 math math: whiskeringRight₂_obj_obj_map_app, whiskeringRight₂_obj_obj_obj_map, whiskeringRight₂_obj_obj_obj_obj, whiskeringRight₂_map_app_app_app, whiskeringRight₂_obj_map_app_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compFlipUncurryIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' obj CategoryTheory.Functor category uncurry flip comp CategoryTheory.Iso.hom prod id compFlipUncurryIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
compFlipUncurryIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' obj CategoryTheory.Functor category uncurry flip comp CategoryTheory.Iso.inv prod id compFlipUncurryIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
comp_flip_uncurry_eq 📖	mathematical	—	obj CategoryTheory.Functor category CategoryTheory.prod' uncurry flip comp prod id	—	—
curryObjCompIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category flip CategoryTheory.prod' curry comp CategoryTheory.Iso.hom whiskeringRight curryObjCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
curryObjCompIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category flip CategoryTheory.prod' curry comp CategoryTheory.Iso.inv whiskeringRight curryObjCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
curryObjProdComp_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.prod' curry comp prod whiskeringLeft CategoryTheory.Iso.hom curryObjProdComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
curryObjProdComp_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category comp CategoryTheory.prod' curry whiskeringLeft prod CategoryTheory.Iso.inv curryObjProdComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
curry_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category curryObj map CategoryTheory.prod' curry	—	—
curry_obj_comp_flip 📖	mathematical	—	flip obj CategoryTheory.Functor CategoryTheory.prod' category curry comp whiskeringRight	—	—
curry_obj_injective 📖	—	obj CategoryTheory.Functor CategoryTheory.prod' category curry	—	—	uncurry_obj_curry_obj
curry_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.prod' map CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Functor category curry	—	—
curry_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category CategoryTheory.prod' curry CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
curry_obj_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category CategoryTheory.prod' curry	—	—
curry_obj_uncurry_obj 📖	mathematical	—	obj CategoryTheory.Functor CategoryTheory.prod' category curry uncurry	—	ext map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.NatTrans.ext' CategoryTheory.eqToHom_app
curryingEquiv_apply_map 📖	mathematical	—	map CategoryTheory.prod' DFunLike.coe Equiv CategoryTheory.Functor category EquivLike.toFunLike Equiv.instEquivLike curryingEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	—
curryingEquiv_apply_obj 📖	mathematical	—	obj CategoryTheory.prod' DFunLike.coe Equiv CategoryTheory.Functor category EquivLike.toFunLike Equiv.instEquivLike curryingEquiv	—	—
curryingEquiv_symm_apply_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.prod' map CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Functor category DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm curryingEquiv	—	—
curryingEquiv_symm_apply_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category DFunLike.coe Equiv CategoryTheory.prod' EquivLike.toFunLike Equiv.instEquivLike Equiv.symm curryingEquiv CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
curryingEquiv_symm_apply_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category DFunLike.coe Equiv CategoryTheory.prod' EquivLike.toFunLike Equiv.instEquivLike Equiv.symm curryingEquiv	—	—
curryingFlipEquiv_apply_map 📖	mathematical	—	map CategoryTheory.prod' DFunLike.coe Equiv CategoryTheory.Functor category EquivLike.toFunLike Equiv.instEquivLike curryingFlipEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.NatTrans.naturality
curryingFlipEquiv_apply_obj 📖	mathematical	—	obj CategoryTheory.prod' DFunLike.coe Equiv CategoryTheory.Functor category EquivLike.toFunLike Equiv.instEquivLike curryingFlipEquiv	—	—
curryingFlipEquiv_symm_apply_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category DFunLike.coe Equiv CategoryTheory.prod' EquivLike.toFunLike Equiv.instEquivLike Equiv.symm curryingEquiv map curryingFlipEquiv CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
curryingFlipEquiv_symm_apply_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category DFunLike.coe Equiv CategoryTheory.prod' EquivLike.toFunLike Equiv.instEquivLike Equiv.symm curryingFlipEquiv CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
curryingFlipEquiv_symm_apply_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category DFunLike.coe Equiv CategoryTheory.prod' EquivLike.toFunLike Equiv.instEquivLike Equiv.symm curryingFlipEquiv	—	—
currying_counitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' obj CategoryTheory.Functor category comp curry uncurry id CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso currying CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
currying_counitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' obj CategoryTheory.Functor category id comp curry uncurry CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso currying CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
currying_functor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' obj CategoryTheory.Functor category CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Equivalence.functor currying	—	—
currying_functor_obj_map 📖	mathematical	—	map CategoryTheory.prod' obj CategoryTheory.Functor category CategoryTheory.Equivalence.functor currying CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	—
currying_functor_obj_obj 📖	mathematical	—	obj CategoryTheory.prod' CategoryTheory.Functor category CategoryTheory.Equivalence.functor currying	—	—
currying_inverse_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category curryObj map CategoryTheory.prod' CategoryTheory.Equivalence.inverse currying	—	—
currying_inverse_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.prod' map CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Functor category CategoryTheory.Equivalence.inverse currying	—	—
currying_inverse_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category CategoryTheory.prod' CategoryTheory.Equivalence.inverse currying CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
currying_inverse_obj_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category CategoryTheory.prod' CategoryTheory.Equivalence.inverse currying	—	—
currying_unitIso_hom_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category id comp CategoryTheory.prod' uncurry curry CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso currying CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
currying_unitIso_inv_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category comp CategoryTheory.prod' uncurry curry id CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso currying CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flipIsoCurrySwapUncurry_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category flip CategoryTheory.prod' curry comp CategoryTheory.Prod.swap uncurry CategoryTheory.Iso.hom flipIsoCurrySwapUncurry CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flipIsoCurrySwapUncurry_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.prod' curry comp CategoryTheory.Prod.swap uncurry flip CategoryTheory.Iso.inv flipIsoCurrySwapUncurry CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flip_flip 📖	mathematical	—	flip	—	—
flip_injective 📖	—	flip	—	—	flip_flip
flippingEquiv_apply_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike flippingEquiv	—	—
flippingEquiv_apply_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike flippingEquiv CategoryTheory.NatTrans.app	—	—
flippingEquiv_apply_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike flippingEquiv	—	—
flippingEquiv_symm_apply_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm flippingEquiv	—	—
flippingEquiv_symm_apply_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm flippingEquiv CategoryTheory.NatTrans.app	—	—
flippingEquiv_symm_apply_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm flippingEquiv	—	—
flipping_counitIso_hom_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category comp CategoryTheory.flipFunctor id CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso flipping CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flipping_counitIso_inv_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category id comp CategoryTheory.flipFunctor CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso flipping CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flipping_functor_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category flip map CategoryTheory.Equivalence.functor flipping	—	—
flipping_functor_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map CategoryTheory.Equivalence.functor flipping	—	—
flipping_functor_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category CategoryTheory.Equivalence.functor flipping CategoryTheory.NatTrans.app	—	—
flipping_functor_obj_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category CategoryTheory.Equivalence.functor flipping	—	—
flipping_inverse_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category flip map CategoryTheory.Equivalence.inverse flipping	—	—
flipping_inverse_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map CategoryTheory.Equivalence.inverse flipping	—	—
flipping_inverse_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category CategoryTheory.Equivalence.inverse flipping CategoryTheory.NatTrans.app	—	—
flipping_inverse_obj_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category CategoryTheory.Equivalence.inverse flipping	—	—
flipping_unitIso_hom_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category id comp CategoryTheory.flipFunctor CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso flipping CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
flipping_unitIso_inv_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category comp CategoryTheory.flipFunctor id CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso flipping CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
instFaithfulProdCurry 📖	mathematical	—	Faithful CategoryTheory.Functor CategoryTheory.prod' category curry	—	FullyFaithful.faithful
instFaithfulProdUncurry 📖	mathematical	—	Faithful CategoryTheory.Functor category CategoryTheory.prod' uncurry	—	FullyFaithful.faithful
instFullProdCurry 📖	mathematical	—	Full CategoryTheory.Functor CategoryTheory.prod' category curry	—	FullyFaithful.full
instFullProdUncurry 📖	mathematical	—	Full CategoryTheory.Functor category CategoryTheory.prod' uncurry	—	FullyFaithful.full
uncurryObjFlip_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' obj CategoryTheory.Functor category uncurry flip comp CategoryTheory.Prod.swap CategoryTheory.Iso.hom uncurryObjFlip CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
uncurryObjFlip_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' comp CategoryTheory.Prod.swap obj CategoryTheory.Functor category uncurry flip CategoryTheory.Iso.inv uncurryObjFlip CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
uncurry_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' obj CategoryTheory.Functor category CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver uncurry	—	—
uncurry_obj_curry_obj 📖	mathematical	—	obj CategoryTheory.Functor category CategoryTheory.prod' uncurry curry	—	ext map_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
uncurry_obj_curry_obj_flip_flip 📖	mathematical	—	obj CategoryTheory.Functor category CategoryTheory.prod' uncurry flip comp curry prod	—	ext map_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
uncurry_obj_curry_obj_flip_flip' 📖	mathematical	—	obj CategoryTheory.Functor category CategoryTheory.prod' uncurry comp flip curry prod	—	ext map_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
uncurry_obj_injective 📖	—	obj CategoryTheory.Functor category CategoryTheory.prod' uncurry	—	—	curry_obj_uncurry_obj
uncurry_obj_map 📖	mathematical	—	map CategoryTheory.prod' obj CategoryTheory.Functor category uncurry CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	—
uncurry_obj_obj 📖	mathematical	—	obj CategoryTheory.prod' CategoryTheory.Functor category uncurry	—	—
whiskeringRight₂_map_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor CategoryTheory.prod' category whiskeringLeft CategoryTheory.prodFunctorToFunctorProd whiskeringRight uncurry curryObj comp curry map whiskeringRight₂	—	—
whiskeringRight₂_obj_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor CategoryTheory.prod' category whiskeringLeft CategoryTheory.prodFunctorToFunctorProd whiskeringRight uncurry map CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id whiskeringRight₂	—	map_id CategoryTheory.Category.comp_id
whiskeringRight₂_obj_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor CategoryTheory.prod' category whiskeringLeft CategoryTheory.prodFunctorToFunctorProd whiskeringRight uncurry map whiskeringRight₂	—	map_id CategoryTheory.Category.id_comp
whiskeringRight₂_obj_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category whiskeringRight₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app	—	—
whiskeringRight₂_obj_obj_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category whiskeringRight₂	—	—

---

← Back to Index