Pseudofunctor

📁 Source: Mathlib/CategoryTheory/Join/Pseudofunctor.lean

Statistics

Metric	Count
Definitions mapCompLeft, mapCompRight, pseudofunctorLeft, pseudofunctorRight, Pseudofunctor	5
Theorems mapWhiskerLeft_associator_hom, mapWhiskerLeft_associator_hom_assoc, mapWhiskerLeft_leftUnitor_hom, mapWhiskerLeft_rightUnitor_hom, mapWhiskerLeft_whiskerLeft, mapWhiskerLeft_whiskerLeft_assoc, mapWhiskerLeft_whiskerRight, mapWhiskerLeft_whiskerRight_assoc, mapWhiskerRight_associator_hom, mapWhiskerRight_leftUnitor_hom, mapWhiskerRight_rightUnitor_hom, mapWhiskerRight_whiskerLeft, mapWhiskerRight_whiskerLeft_assoc, mapWhiskerRight_whiskerRight, mapWhiskerRight_whiskerRight_assoc, pseudofunctorLeft_mapComp_hom_toNatTrans_app, pseudofunctorLeft_mapComp_inv_toNatTrans_app, pseudofunctorLeft_mapId_hom_toNatTrans_app, pseudofunctorLeft_mapId_inv_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, pseudofunctorRight_mapComp_hom_toNatTrans_app, pseudofunctorRight_mapComp_inv_toNatTrans_app, pseudofunctorRight_mapId_hom_toNatTrans_app, pseudofunctorRight_mapId_inv_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α	35
Total	40

CategoryTheory

Definitions

Name	Category	Theorems
Pseudofunctor 📖	CompData	25 math math: Pseudofunctor.StrongTrans.homCategory_comp_as_app, Pseudofunctor.StrongTrans.comp_app, Pseudofunctor.CoGrothendieck.map_comp_eq, Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom, Pseudofunctor.StrongTrans.leftUnitor_inv_as_app, Pseudofunctor.Grothendieck.map_id_eq, Pseudofunctor.Grothendieck.map_id_map, Pseudofunctor.StrongTrans.id.toOplax, Pseudofunctor.StrongTrans.homCategory_id_as_app, Pseudofunctor.StrongTrans.isoMk_hom_as_app, Pseudofunctor.StrongTrans.categoryStruct_id_naturality_hom, Pseudofunctor.StrongTrans.isoMk_inv_as_app, Pseudofunctor.StrongTrans.associator_inv_as_app, Pseudofunctor.StrongTrans.leftUnitor_hom_as_app, Pseudofunctor.StrongTrans.rightUnitor_inv_as_app, Pseudofunctor.StrongTrans.categoryStruct_id_naturality_inv, Pseudofunctor.StrongTrans.whiskerRight_as_app, Pseudofunctor.StrongTrans.associator_hom_as_app, Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv, Pseudofunctor.Grothendieck.map_comp_eq, Pseudofunctor.StrongTrans.rightUnitor_hom_as_app, Pseudofunctor.StrongTrans.whiskerLeft_as_app, Pseudofunctor.StrongTrans.categoryStruct_id_app, Pseudofunctor.CoGrothendieck.map_id_eq, Pseudofunctor.CoGrothendieck.map_id_map

CategoryTheory.Join

Definitions

Name	Category	Theorems
mapCompLeft 📖	CompOp	7 math math: mapWhiskerRight_leftUnitor_hom, mapWhiskerRight_whiskerRight, mapWhiskerRight_associator_hom, mapWhiskerRight_whiskerLeft, mapWhiskerRight_whiskerLeft_assoc, mapWhiskerRight_rightUnitor_hom, mapWhiskerRight_whiskerRight_assoc
mapCompRight 📖	CompOp	8 math math: mapWhiskerLeft_whiskerRight, mapWhiskerLeft_whiskerLeft, mapWhiskerLeft_whiskerRight_assoc, mapWhiskerLeft_associator_hom, mapWhiskerLeft_associator_hom_assoc, mapWhiskerLeft_rightUnitor_hom, mapWhiskerLeft_whiskerLeft_assoc, mapWhiskerLeft_leftUnitor_hom
pseudofunctorLeft 📖	CompOp	10 math math: pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, pseudofunctorLeft_mapId_inv_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, pseudofunctorLeft_mapId_hom_toNatTrans_app, pseudofunctorLeft_mapComp_hom_toNatTrans_app, pseudofunctorLeft_mapComp_inv_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj
pseudofunctorRight 📖	CompOp	10 math math: pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, pseudofunctorRight_mapComp_inv_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, pseudofunctorRight_mapId_hom_toNatTrans_app, pseudofunctorRight_mapId_inv_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, pseudofunctorRight_mapComp_hom_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapWhiskerLeft_associator_hom 📖	mathematical	—	mapWhiskerLeft CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.associator CategoryTheory.CategoryStruct.comp CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct mapPair mapCompRight CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.inv	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerLeft_app CategoryTheory.Functor.whiskerRight_comp CategoryTheory.Category.assoc CategoryTheory.Functor.whiskerLeft_twice CategoryTheory.Iso.hom_inv_id_assoc mapIsoWhiskerRight_hom_app CategoryTheory.Functor.map_id mapPairComp_hom_app_left mapPairComp_inv_app_left mapIsoWhiskerRight_inv_app CategoryTheory.Category.comp_id mapPairComp_hom_app_right mapPairComp_inv_app_right
mapWhiskerLeft_associator_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair CategoryTheory.Functor.id CategoryTheory.Functor.comp mapWhiskerLeft CategoryTheory.Iso.hom CategoryTheory.Functor.associator mapCompRight CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapWhiskerLeft_associator_hom
mapWhiskerLeft_leftUnitor_hom 📖	mathematical	—	mapWhiskerLeft CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct mapPair mapCompRight CategoryTheory.Functor.whiskerRight mapPairId	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerLeft_app CategoryTheory.Category.assoc mapIsoWhiskerRight_hom_app CategoryTheory.Functor.map_id mapPairComp_hom_app_left mapPairId_hom_app CategoryTheory.Category.comp_id mapPairComp_hom_app_right
mapWhiskerLeft_rightUnitor_hom 📖	mathematical	—	mapWhiskerLeft CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct mapPair mapCompRight CategoryTheory.Functor.whiskerLeft mapPairId	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerLeft_app CategoryTheory.Category.assoc CategoryTheory.Functor.whiskerLeft_twice mapIsoWhiskerRight_hom_app CategoryTheory.Functor.map_id mapPairComp_hom_app_left mapPairId_hom_app CategoryTheory.Category.comp_id mapPairComp_hom_app_right
mapWhiskerLeft_whiskerLeft 📖	mathematical	—	mapWhiskerLeft CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair CategoryTheory.Iso.hom mapCompRight CategoryTheory.Iso.inv	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerLeft_app CategoryTheory.Category.assoc CategoryTheory.Functor.whiskerLeft_twice mapIsoWhiskerRight_hom_app CategoryTheory.Functor.map_id mapPairComp_hom_app_left mapPairComp_inv_app_left mapIsoWhiskerRight_inv_app CategoryTheory.Category.comp_id mapPairComp_hom_app_right mapPairComp_inv_app_right CategoryTheory.Category.id_comp
mapWhiskerLeft_whiskerLeft_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair CategoryTheory.Functor.id CategoryTheory.Functor.comp mapWhiskerLeft CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom mapCompRight CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapWhiskerLeft_whiskerLeft
mapWhiskerLeft_whiskerRight 📖	mathematical	—	mapWhiskerLeft CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair CategoryTheory.Iso.hom mapCompRight CategoryTheory.Iso.inv	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerLeft_app CategoryTheory.Category.assoc mapIsoWhiskerRight_hom_app CategoryTheory.Functor.map_id mapPairComp_hom_app_left mapPairComp_inv_app_left mapIsoWhiskerRight_inv_app CategoryTheory.Category.comp_id mapPairComp_hom_app_right mapPairComp_inv_app_right CategoryTheory.Category.id_comp
mapWhiskerLeft_whiskerRight_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair CategoryTheory.Functor.id CategoryTheory.Functor.comp mapWhiskerLeft CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom mapCompRight CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapWhiskerLeft_whiskerRight
mapWhiskerRight_associator_hom 📖	mathematical	—	mapWhiskerRight CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.associator CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct mapPair mapCompLeft CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.inv	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerRight_app CategoryTheory.Functor.map_id CategoryTheory.Functor.whiskerRight_comp CategoryTheory.Category.assoc CategoryTheory.Functor.whiskerLeft_twice CategoryTheory.Iso.hom_inv_id_assoc mapIsoWhiskerLeft_hom_app mapPairComp_hom_app_left mapPairComp_inv_app_left mapIsoWhiskerLeft_inv_app CategoryTheory.Category.comp_id mapPairComp_hom_app_right mapPairComp_inv_app_right
mapWhiskerRight_leftUnitor_hom 📖	mathematical	—	mapWhiskerRight CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct mapPair mapCompLeft CategoryTheory.Functor.whiskerRight mapPairId	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerRight_app CategoryTheory.Functor.map_id CategoryTheory.Category.assoc mapIsoWhiskerLeft_hom_app mapPairComp_hom_app_left mapPairId_hom_app CategoryTheory.Category.comp_id mapPairComp_hom_app_right
mapWhiskerRight_rightUnitor_hom 📖	mathematical	—	mapWhiskerRight CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct mapPair mapCompLeft CategoryTheory.Functor.whiskerLeft mapPairId	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerRight_app CategoryTheory.Functor.map_id CategoryTheory.Category.assoc CategoryTheory.Functor.whiskerLeft_twice mapIsoWhiskerLeft_hom_app mapPairComp_hom_app_left mapPairId_hom_app CategoryTheory.Category.comp_id mapPairComp_hom_app_right
mapWhiskerRight_whiskerLeft 📖	mathematical	—	mapWhiskerRight CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair CategoryTheory.Iso.hom mapCompLeft CategoryTheory.Iso.inv	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerRight_app CategoryTheory.Category.assoc CategoryTheory.Functor.whiskerLeft_twice mapIsoWhiskerLeft_hom_app mapPairComp_hom_app_left mapPairComp_inv_app_left mapIsoWhiskerLeft_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id mapPairComp_hom_app_right mapPairComp_inv_app_right
mapWhiskerRight_whiskerLeft_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair CategoryTheory.Functor.comp CategoryTheory.Functor.id mapWhiskerRight CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom mapCompLeft CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapWhiskerRight_whiskerLeft
mapWhiskerRight_whiskerRight 📖	mathematical	—	mapWhiskerRight CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair CategoryTheory.Iso.hom mapCompLeft CategoryTheory.Iso.inv	—	natTrans_ext CategoryTheory.NatTrans.ext' mapWhiskerRight_app CategoryTheory.Category.assoc mapIsoWhiskerLeft_hom_app mapPairComp_hom_app_left mapPairComp_inv_app_left mapIsoWhiskerLeft_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id mapPairComp_hom_app_right mapPairComp_inv_app_right
mapWhiskerRight_whiskerRight_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair CategoryTheory.Functor.comp CategoryTheory.Functor.id mapWhiskerRight CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom mapCompLeft CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapWhiskerRight_whiskerRight
pseudofunctorLeft_mapComp_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory mapPair CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapComp pseudofunctorLeft comp CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct id left right CategoryTheory.Functor CategoryTheory.Functor.category mapPairComp	—	mapIsoWhiskerLeft_hom_app CategoryTheory.Functor.map_id
pseudofunctorLeft_mapComp_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory CategoryTheory.Functor.comp CategoryTheory.Cat.of CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.toCatHom mapPair CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapComp pseudofunctorLeft comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category mapPairComp CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct id left right	—	mapIsoWhiskerLeft_inv_app CategoryTheory.Functor.map_id
pseudofunctorLeft_mapId_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory mapPair CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Functor.id CategoryTheory.Cat.of CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapId pseudofunctorLeft CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj comp left id right	—	—
pseudofunctorLeft_mapId_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory CategoryTheory.Functor.id CategoryTheory.Cat.of mapPair CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapId pseudofunctorLeft CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj comp left id right	—	—
pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory mapPair CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.id CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorLeft CategoryTheory.Functor.obj comp left id CategoryTheory.Functor.map inclLeft right	—	CategoryTheory.Functor.map_id
pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of Prefunctor.map CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorLeft homInduction left CategoryTheory.Functor.obj right inclLeft inclRight edge	—	—
pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of Prefunctor.map CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorLeft left right	—	—
pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Category.toCategoryStruct CategoryTheory.Bundled.str Prefunctor.obj CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorLeft comp	—	—
pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Category.toCategoryStruct CategoryTheory.Bundled.str Prefunctor.obj CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorLeft id	—	—
pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α 📖	mathematical	—	CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorLeft CategoryTheory.Join CategoryTheory.Cat.str	—	—
pseudofunctorRight_mapComp_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory mapPair CategoryTheory.Functor.id CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Functor.comp CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapComp pseudofunctorRight comp CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct id left right CategoryTheory.Functor CategoryTheory.Functor.category mapPairComp	—	mapIsoWhiskerRight_hom_app CategoryTheory.Functor.map_id
pseudofunctorRight_mapComp_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory CategoryTheory.Functor.comp CategoryTheory.Cat.of CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.toCatHom mapPair CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapComp pseudofunctorRight comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category mapPairComp CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct id left right	—	mapIsoWhiskerRight_inv_app CategoryTheory.Functor.map_id
pseudofunctorRight_mapId_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory mapPair CategoryTheory.Functor.id CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Cat.of CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapId pseudofunctorRight CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj comp left id right	—	—
pseudofunctorRight_mapId_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory CategoryTheory.Functor.id CategoryTheory.Cat.of mapPair CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapId pseudofunctorRight CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj comp left id right	—	—
pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory mapPair CategoryTheory.Functor.id CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorRight CategoryTheory.Functor.obj comp left id right CategoryTheory.Functor.map inclRight	—	CategoryTheory.Functor.map_id
pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of Prefunctor.map CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorRight homInduction left right CategoryTheory.Functor.obj inclLeft inclRight edge	—	—
pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str instCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of Prefunctor.map CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorRight left right	—	—
pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Category.toCategoryStruct CategoryTheory.Bundled.str Prefunctor.obj CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorRight comp	—	—
pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Join CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Category.toCategoryStruct CategoryTheory.Bundled.str Prefunctor.obj CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorRight id	—	—
pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α 📖	mathematical	—	CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorRight CategoryTheory.Join CategoryTheory.Cat.str	—	—

---

← Back to Index