CartesianClosed

📁 Source: Mathlib/CategoryTheory/Category/Cat/CartesianClosed.lean

Statistics

Metric	Count
Definitions cartesianClosed, closed, exp, curryingIso, flippingIso	5
Theorems exp_map, exp_obj, ihom_map, ihom_obj, curryingIso_hom_toFunctor_map_app, curryingIso_hom_toFunctor_obj_map, curryingIso_hom_toFunctor_obj_obj, curryingIso_inv_toFunctor_map_app_app, curryingIso_inv_toFunctor_obj_map_app, curryingIso_inv_toFunctor_obj_obj_map, curryingIso_inv_toFunctor_obj_obj_obj, flippingIso_hom_toFunctor_map_app_app, flippingIso_hom_toFunctor_obj_map_app, flippingIso_hom_toFunctor_obj_obj_map, flippingIso_hom_toFunctor_obj_obj_obj, flippingIso_inv_toFunctor_map_app_app, flippingIso_inv_toFunctor_obj_map_app, flippingIso_inv_toFunctor_obj_obj_map, flippingIso_inv_toFunctor_obj_obj_obj	19
Total	24

CategoryTheory

Definitions

Name	Category	Theorems
curryingIso 📖	CompOp	7 math math: curryingIso_hom_toFunctor_obj_map, curryingIso_inv_toFunctor_obj_map_app, curryingIso_hom_toFunctor_obj_obj, curryingIso_inv_toFunctor_obj_obj_obj, curryingIso_inv_toFunctor_map_app_app, curryingIso_inv_toFunctor_obj_obj_map, curryingIso_hom_toFunctor_map_app
flippingIso 📖	CompOp	8 math math: flippingIso_inv_toFunctor_obj_obj_obj, flippingIso_inv_toFunctor_obj_map_app, flippingIso_inv_toFunctor_map_app_app, flippingIso_hom_toFunctor_obj_obj_map, flippingIso_hom_toFunctor_obj_map_app, flippingIso_inv_toFunctor_obj_obj_map, flippingIso_hom_toFunctor_obj_obj_obj, flippingIso_hom_toFunctor_map_app_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curryingIso_hom_toFunctor_map_app 📖	mathematical	—	NatTrans.app prod' Functor.obj Functor Functor.category CategoryStruct.comp Category.toCategoryStruct Functor.map Quiver.Hom CategoryStruct.toQuiver Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.hom Cat Cat.category curryingIso	—	—
curryingIso_hom_toFunctor_obj_map 📖	mathematical	—	Functor.map prod' Functor.obj Bundled.α Category Cat.of Functor Functor.category Cat.str Cat.Hom.toFunctor Iso.hom Cat Cat.category curryingIso CategoryStruct.comp Category.toCategoryStruct NatTrans.app Quiver.Hom CategoryStruct.toQuiver	—	—
curryingIso_hom_toFunctor_obj_obj 📖	mathematical	—	Functor.obj prod' Bundled.α Category Cat.of Functor Functor.category Cat.str Cat.Hom.toFunctor Iso.hom Cat Cat.category curryingIso	—	—
curryingIso_inv_toFunctor_map_app_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.curryObj Functor.map Bundled.α Category Cat.of prod' Cat.str Cat.Hom.toFunctor Iso.inv Cat Cat.category curryingIso	—	—
curryingIso_inv_toFunctor_obj_map_app 📖	mathematical	—	NatTrans.app Functor.obj prod' Functor.map Prod.mkHom Category.toCategoryStruct CategoryStruct.id Functor Functor.category Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.inv Cat Cat.category curryingIso	—	—
curryingIso_inv_toFunctor_obj_obj_map 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category Bundled.α Category Cat.of prod' Cat.str Cat.Hom.toFunctor Iso.inv Cat Cat.category curryingIso Prod.mkHom Category.toCategoryStruct CategoryStruct.id	—	—
curryingIso_inv_toFunctor_obj_obj_obj 📖	mathematical	—	Functor.obj Functor Functor.category Bundled.α Category Cat.of prod' Cat.str Cat.Hom.toFunctor Iso.inv Cat Cat.category curryingIso	—	—
flippingIso_hom_toFunctor_map_app_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.flip Functor.map Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.hom Cat Cat.category flippingIso	—	—
flippingIso_hom_toFunctor_obj_map_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.map Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.hom Cat Cat.category flippingIso	—	—
flippingIso_hom_toFunctor_obj_obj_map 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.hom Cat Cat.category flippingIso NatTrans.app	—	—
flippingIso_hom_toFunctor_obj_obj_obj 📖	mathematical	—	Functor.obj Functor Functor.category Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.hom Cat Cat.category flippingIso	—	—
flippingIso_inv_toFunctor_map_app_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.flip Functor.map Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.inv Cat Cat.category flippingIso	—	—
flippingIso_inv_toFunctor_obj_map_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.map Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.inv Cat Cat.category flippingIso	—	—
flippingIso_inv_toFunctor_obj_obj_map 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.inv Cat Cat.category flippingIso NatTrans.app	—	—
flippingIso_inv_toFunctor_obj_obj_obj 📖	mathematical	—	Functor.obj Functor Functor.category Bundled.α Category Cat.of Cat.str Cat.Hom.toFunctor Iso.inv Cat Cat.category flippingIso	—	—

CategoryTheory.Cat

Definitions

Name	Category	Theorems
cartesianClosed 📖	CompOp	—
closed 📖	CompOp	2 math math: ihom_obj, ihom_map
exp 📖	CompOp	2 math math: exp_obj, exp_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cat category exp CategoryTheory.Functor.toCatHom CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight Hom.toFunctor	—	—
exp_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Cat category exp of CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Functor.category	—	—
ihom_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cat category CategoryTheory.ihom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory of closed CategoryTheory.Functor.toCatHom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight	—	—
ihom_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Cat category CategoryTheory.ihom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory of closed CategoryTheory.Functor CategoryTheory.Functor.category	—	—

---

← Back to Index