Yoneda

📁 Source: Mathlib/CategoryTheory/Bicategory/Yoneda.lean

Statistics

Metric	Count
Definitions associatorNatIsoLeftCat, associatorNatIsoMiddleCat, associatorNatIsoRightCat, leftUnitorNatIsoCat, postcomposingCat, postcomposing₂, postcomp₂, precomposingCat, rightUnitorNatIsoCat, yoneda, yoneda₀	11
Theorems associatorNatIsoLeftCat_hom_toNatTrans_app, associatorNatIsoLeftCat_inv_toNatTrans_app, associatorNatIsoMiddleCat_hom_toNatTrans_app, associatorNatIsoMiddleCat_inv_toNatTrans_app, associatorNatIsoRightCat_hom_toNatTrans_app, associatorNatIsoRightCat_inv_toNatTrans_app, leftUnitorNatIsoCat_hom_toNatTrans_app, leftUnitorNatIsoCat_inv_toNatTrans_app, postcomposingCat_map, postcomposingCat_obj, postcomposing₂_map_as_app_toNatTrans_app, postcomposing₂_obj_app_toFunctor_map, postcomposing₂_obj_app_toFunctor_obj, postcomposing₂_obj_naturality_hom_toNatTrans_app, postcomposing₂_obj_naturality_inv_toNatTrans_app, postcomp₂_app_toFunctor_map, postcomp₂_app_toFunctor_obj, postcomp₂_naturality_hom_toNatTrans_app, postcomp₂_naturality_inv_toNatTrans_app, precomposingCat_map, precomposingCat_obj, rightUnitorNatIsoCat_hom_toNatTrans_app, rightUnitorNatIsoCat_inv_toNatTrans_app, yoneda_mapComp_hom_as_app_toNatTrans_app, yoneda_mapComp_inv_as_app_toNatTrans_app, yoneda_mapId_hom_as_app_toNatTrans_app, yoneda_mapId_inv_as_app_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_map, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_obj, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_hom_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_hom_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_hom_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, yoneda₀_mapComp_hom_toNatTrans_app, yoneda₀_mapComp_inv_toNatTrans_app, yoneda₀_mapId_hom_toNatTrans_app, yoneda₀_mapId_inv_toNatTrans_app, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α	50
Total	61

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
associatorNatIsoLeftCat 📖	CompOp	2 math math: associatorNatIsoLeftCat_hom_toNatTrans_app, associatorNatIsoLeftCat_inv_toNatTrans_app
associatorNatIsoMiddleCat 📖	CompOp	2 math math: associatorNatIsoMiddleCat_hom_toNatTrans_app, associatorNatIsoMiddleCat_inv_toNatTrans_app
associatorNatIsoRightCat 📖	CompOp	2 math math: associatorNatIsoRightCat_inv_toNatTrans_app, associatorNatIsoRightCat_hom_toNatTrans_app
leftUnitorNatIsoCat 📖	CompOp	2 math math: leftUnitorNatIsoCat_inv_toNatTrans_app, leftUnitorNatIsoCat_hom_toNatTrans_app
postcomposingCat 📖	CompOp	18 math math: associatorNatIsoLeftCat_hom_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_inv_toNatTrans_app, postcomposing₂_map_as_app_toNatTrans_app, postcomposing₂_obj_naturality_hom_toNatTrans_app, postcomposingCat_obj, postcomp₂_naturality_hom_toNatTrans_app, rightUnitorNatIsoCat_hom_toNatTrans_app, postcomposingCat_map, associatorNatIsoLeftCat_inv_toNatTrans_app, associatorNatIsoMiddleCat_hom_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app, yoneda_mapComp_inv_as_app_toNatTrans_app, postcomp₂_naturality_inv_toNatTrans_app, associatorNatIsoMiddleCat_inv_toNatTrans_app, rightUnitorNatIsoCat_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_hom_toNatTrans_app, postcomposing₂_obj_naturality_inv_toNatTrans_app, yoneda_mapComp_hom_as_app_toNatTrans_app
postcomposing₂ 📖	CompOp	9 math math: postcomposing₂_map_as_app_toNatTrans_app, postcomposing₂_obj_naturality_hom_toNatTrans_app, yoneda_mapId_inv_as_app_toNatTrans_app, postcomposing₂_obj_app_toFunctor_map, yoneda_mapId_hom_as_app_toNatTrans_app, postcomposing₂_obj_app_toFunctor_obj, yoneda_mapComp_inv_as_app_toNatTrans_app, postcomposing₂_obj_naturality_inv_toNatTrans_app, yoneda_mapComp_hom_as_app_toNatTrans_app
postcomp₂ 📖	CompOp	6 math math: postcomp₂_app_toFunctor_obj, postcomposing₂_map_as_app_toNatTrans_app, postcomp₂_naturality_hom_toNatTrans_app, postcomp₂_app_toFunctor_map, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app, postcomp₂_naturality_inv_toNatTrans_app
precomposingCat 📖	CompOp	22 math math: yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_inv_toNatTrans_app, precomposingCat_map, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_hom_toNatTrans_app, associatorNatIsoRightCat_inv_toNatTrans_app, postcomposing₂_obj_naturality_hom_toNatTrans_app, postcomp₂_naturality_hom_toNatTrans_app, precomposingCat_obj, yoneda₀_mapId_hom_toNatTrans_app, yoneda₀_mapId_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_hom_toNatTrans_app, yoneda₀_mapComp_inv_toNatTrans_app, leftUnitorNatIsoCat_inv_toNatTrans_app, leftUnitorNatIsoCat_hom_toNatTrans_app, associatorNatIsoMiddleCat_hom_toNatTrans_app, yoneda₀_mapComp_hom_toNatTrans_app, postcomp₂_naturality_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_inv_toNatTrans_app, associatorNatIsoMiddleCat_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_hom_toNatTrans_app, postcomposing₂_obj_naturality_inv_toNatTrans_app, associatorNatIsoRightCat_hom_toNatTrans_app
rightUnitorNatIsoCat 📖	CompOp	2 math math: rightUnitorNatIsoCat_hom_toNatTrans_app, rightUnitorNatIsoCat_inv_toNatTrans_app
yoneda 📖	CompOp	18 math math: yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_hom_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_map, yoneda_mapId_inv_as_app_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_hom_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str, yoneda_mapId_hom_as_app_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_obj, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, yoneda_mapComp_inv_as_app_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_inv_toNatTrans_app, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_hom_toNatTrans_app, yoneda_mapComp_hom_as_app_toNatTrans_app
yoneda₀ 📖	CompOp	23 math math: postcomp₂_app_toFunctor_obj, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, postcomposing₂_map_as_app_toNatTrans_app, postcomposing₂_obj_naturality_hom_toNatTrans_app, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, yoneda_mapId_inv_as_app_toNatTrans_app, postcomp₂_naturality_hom_toNatTrans_app, postcomp₂_app_toFunctor_map, yoneda₀_mapId_hom_toNatTrans_app, yoneda₀_mapId_inv_toNatTrans_app, yoneda₀_mapComp_inv_toNatTrans_app, postcomposing₂_obj_app_toFunctor_map, yoneda_mapId_hom_as_app_toNatTrans_app, yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app, postcomposing₂_obj_app_toFunctor_obj, yoneda₀_mapComp_hom_toNatTrans_app, yoneda_mapComp_inv_as_app_toNatTrans_app, postcomp₂_naturality_inv_toNatTrans_app, postcomposing₂_obj_naturality_inv_toNatTrans_app, yoneda_mapComp_hom_as_app_toNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associatorNatIsoLeftCat_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat postcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat.bicategory associatorNatIsoLeftCat associator	—	—
associatorNatIsoLeftCat_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Cat.str postcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat.bicategory associatorNatIsoLeftCat associator	—	—
associatorNatIsoMiddleCat_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat postcomposingCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp associatorNatIsoMiddleCat associator	—	—
associatorNatIsoMiddleCat_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat precomposingCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp associatorNatIsoMiddleCat associator	—	—
associatorNatIsoRightCat_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory precomp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat.bicategory associatorNatIsoRightCat associator	—	—
associatorNatIsoRightCat_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat precomp CategoryTheory.CategoryStruct.comp CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat.bicategory associatorNatIsoRightCat associator	—	—
leftUnitorNatIsoCat_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory precomp CategoryTheory.CategoryStruct.id CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj precomposingCat CategoryTheory.Cat.bicategory leftUnitorNatIsoCat CategoryTheory.CategoryStruct.comp leftUnitor	—	—
leftUnitorNatIsoCat_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str precomp CategoryTheory.CategoryStruct.id CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj precomposingCat CategoryTheory.Cat.bicategory leftUnitorNatIsoCat CategoryTheory.CategoryStruct.comp leftUnitor	—	—
postcomposingCat_map 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of CategoryTheory.Cat.Hom.instCategory postcomposingCat CategoryTheory.NatTrans.toCatHom₂ postcomp CategoryTheory.Functor CategoryTheory.Functor.category postcomposing	—	—
postcomposingCat_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of CategoryTheory.Cat.Hom.instCategory postcomposingCat CategoryTheory.Functor.toCatHom postcomp	—	—
postcomposing₂_map_as_app_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category postcomposing CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat CategoryTheory.Pseudofunctor.StrongTrans.Modification.app Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat.bicategory yoneda₀ postcomp₂ CategoryTheory.Pseudofunctor.StrongTrans.Hom.as CategoryTheory.Functor.map CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct CategoryTheory.Pseudofunctor.StrongTrans.homCategory postcomposing₂ whiskerLeft	—	—
postcomposing₂_obj_app_toFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of CategoryTheory.Pseudofunctor.StrongTrans.app Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory yoneda₀ CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct CategoryTheory.Pseudofunctor.StrongTrans.homCategory postcomposing₂ whiskerRight	—	—
postcomposing₂_obj_app_toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of CategoryTheory.Pseudofunctor.StrongTrans.app Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory yoneda₀ CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct CategoryTheory.Pseudofunctor.StrongTrans.homCategory postcomposing₂ CategoryTheory.CategoryStruct.comp	—	—
postcomposing₂_obj_naturality_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat Quiver.Hom.unop postcomposingCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.StrongTrans.naturality Opposite Bicategory.Opposite.bicategory yoneda₀ CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct CategoryTheory.Pseudofunctor.StrongTrans.homCategory postcomposing₂ associator	—	—
postcomposing₂_obj_naturality_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat precomposingCat Quiver.Hom.unop CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.StrongTrans.naturality Opposite Bicategory.Opposite.bicategory yoneda₀ CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct CategoryTheory.Pseudofunctor.StrongTrans.homCategory postcomposing₂ associator	—	—
postcomp₂_app_toFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of CategoryTheory.Pseudofunctor.StrongTrans.app Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory yoneda₀ postcomp₂ whiskerRight	—	—
postcomp₂_app_toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of CategoryTheory.Pseudofunctor.StrongTrans.app Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory yoneda₀ postcomp₂ CategoryTheory.CategoryStruct.comp	—	—
postcomp₂_naturality_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat Quiver.Hom.unop postcomposingCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.StrongTrans.naturality Opposite Bicategory.Opposite.bicategory yoneda₀ postcomp₂ associator	—	—
postcomp₂_naturality_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat precomposingCat Quiver.Hom.unop CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.StrongTrans.naturality Opposite Bicategory.Opposite.bicategory yoneda₀ postcomp₂ associator	—	—
precomposingCat_map 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of CategoryTheory.Cat.Hom.instCategory precomposingCat CategoryTheory.NatTrans.toCatHom₂ precomp CategoryTheory.Functor CategoryTheory.Functor.category precomposing	—	—
precomposingCat_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of CategoryTheory.Cat.Hom.instCategory precomposingCat CategoryTheory.Functor.toCatHom precomp	—	—
rightUnitorNatIsoCat_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory postcomp CategoryTheory.CategoryStruct.id CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj postcomposingCat CategoryTheory.Cat.bicategory rightUnitorNatIsoCat CategoryTheory.CategoryStruct.comp rightUnitor	—	—
rightUnitorNatIsoCat_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str postcomp CategoryTheory.CategoryStruct.id CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj postcomposingCat CategoryTheory.Cat.bicategory rightUnitorNatIsoCat CategoryTheory.CategoryStruct.comp rightUnitor	—	—
yoneda_mapComp_hom_as_app_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.str postcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat CategoryTheory.Cat.Hom₂.toNatTrans Prefunctor.obj Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctor.mkOfHomFunctors yoneda₀ postcomposing₂ CategoryTheory.Pseudofunctor.StrongTrans.app Prefunctor.map CategoryTheory.Pseudofunctor.StrongTrans.Modification.app CategoryTheory.Pseudofunctor.StrongTrans.Hom.as CategoryTheory.Iso.hom CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct CategoryTheory.Pseudofunctor.StrongTrans.homCategory CategoryTheory.Pseudofunctor.mapComp yoneda CategoryTheory.Iso.inv associator	—	—
yoneda_mapComp_inv_as_app_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat postcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Cat.Hom₂.toNatTrans Prefunctor.obj Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctor.mkOfHomFunctors yoneda₀ postcomposing₂ CategoryTheory.Pseudofunctor.StrongTrans.app Prefunctor.map CategoryTheory.Pseudofunctor.StrongTrans.Modification.app CategoryTheory.Pseudofunctor.StrongTrans.Hom.as CategoryTheory.Iso.inv CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct CategoryTheory.Pseudofunctor.StrongTrans.homCategory CategoryTheory.Pseudofunctor.mapComp yoneda CategoryTheory.Iso.hom associator	—	—
yoneda_mapId_hom_as_app_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory postcomp CategoryTheory.CategoryStruct.id CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom₂.toNatTrans Prefunctor.obj Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctor.mkOfHomFunctors yoneda₀ postcomposing₂ CategoryTheory.Pseudofunctor.StrongTrans.app Prefunctor.map CategoryTheory.Pseudofunctor.StrongTrans.Modification.app CategoryTheory.Pseudofunctor.StrongTrans.Hom.as CategoryTheory.Iso.hom CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct CategoryTheory.Pseudofunctor.StrongTrans.homCategory CategoryTheory.Pseudofunctor.mapId yoneda CategoryTheory.CategoryStruct.comp rightUnitor	—	—
yoneda_mapId_inv_as_app_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str postcomp CategoryTheory.CategoryStruct.id CategoryTheory.Cat.Hom₂.toNatTrans Prefunctor.obj Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctor.mkOfHomFunctors yoneda₀ postcomposing₂ CategoryTheory.Pseudofunctor.StrongTrans.app Prefunctor.map CategoryTheory.Pseudofunctor.StrongTrans.Modification.app CategoryTheory.Pseudofunctor.StrongTrans.Hom.as CategoryTheory.Iso.inv CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct CategoryTheory.Pseudofunctor.StrongTrans.homCategory CategoryTheory.Pseudofunctor.mapId yoneda CategoryTheory.CategoryStruct.comp rightUnitor	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category postcomposing CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat CategoryTheory.Pseudofunctor.StrongTrans.Modification.app Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat.bicategory yoneda₀ postcomp₂ CategoryTheory.Pseudofunctor.StrongTrans.Hom.as Prefunctor.obj CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda whiskerLeft	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of CategoryTheory.Pseudofunctor.StrongTrans.app Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory Prefunctor.map CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda whiskerRight	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of CategoryTheory.Pseudofunctor.StrongTrans.app Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory Prefunctor.map CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda CategoryTheory.CategoryStruct.comp	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat Quiver.Hom.unop postcomposingCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.StrongTrans.naturality Opposite Bicategory.Opposite.bicategory Prefunctor.map CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda associator	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory postcomposingCat precomposingCat Quiver.Hom.unop CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.StrongTrans.naturality Opposite Bicategory.Opposite.bicategory Prefunctor.map CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda associator	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory precomp CategoryTheory.CategoryStruct.comp Quiver.Hom.unop CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat.bicategory CategoryTheory.Pseudofunctor.mapComp Opposite Bicategory.Opposite.bicategory Prefunctor.obj CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda associator	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat Quiver.Hom.unop precomp CategoryTheory.CategoryStruct.comp CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat.bicategory CategoryTheory.Pseudofunctor.mapComp Opposite Bicategory.Opposite.bicategory Prefunctor.obj CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda associator	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory precomp CategoryTheory.CategoryStruct.id CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj precomposingCat CategoryTheory.Cat.bicategory CategoryTheory.Pseudofunctor.mapId Opposite Bicategory.Opposite.bicategory Prefunctor.obj CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda CategoryTheory.CategoryStruct.comp leftUnitor	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str precomp CategoryTheory.CategoryStruct.id CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj precomposingCat CategoryTheory.Cat.bicategory CategoryTheory.Pseudofunctor.mapId Opposite Bicategory.Opposite.bicategory Prefunctor.obj CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda CategoryTheory.CategoryStruct.comp leftUnitor	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category precomposing Opposite Bicategory.Opposite.bicategory Bicategory.Opposite.unopFunctor CategoryTheory.Cat.Hom₂.toNatTrans Prefunctor.obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor yoneda whiskerRight Quiver.Hom.unop Bicategory.Opposite.Hom2.unop2	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Prefunctor.obj CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory yoneda whiskerLeft Quiver.Hom.unop	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Prefunctor.obj CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory yoneda CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str 📖	mathematical	—	CategoryTheory.Bundled.str CategoryTheory.Category Prefunctor.obj Opposite CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory yoneda Opposite.unop	—	—
yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α 📖	mathematical	—	CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj Opposite CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Pseudofunctor CategoryTheory.Pseudofunctor.StrongTrans.instBicategory yoneda Opposite.unop	—	—
yoneda₀_mapComp_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory precomp CategoryTheory.CategoryStruct.comp Quiver.Hom.unop CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat.bicategory CategoryTheory.Pseudofunctor.mapComp Opposite Bicategory.Opposite.bicategory yoneda₀ associator	—	—
yoneda₀_mapComp_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory precomposingCat Quiver.Hom.unop precomp CategoryTheory.CategoryStruct.comp CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat.bicategory CategoryTheory.Pseudofunctor.mapComp Opposite Bicategory.Opposite.bicategory yoneda₀ associator	—	—
yoneda₀_mapId_hom_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory precomp CategoryTheory.CategoryStruct.id CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj precomposingCat CategoryTheory.Cat.bicategory CategoryTheory.Pseudofunctor.mapId Opposite Bicategory.Opposite.bicategory yoneda₀ CategoryTheory.CategoryStruct.comp leftUnitor	—	—
yoneda₀_mapId_inv_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.of CategoryTheory.Cat.str precomp CategoryTheory.CategoryStruct.id CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Functor.toCatHom CategoryTheory.Iso.inv CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj precomposingCat CategoryTheory.Cat.bicategory CategoryTheory.Pseudofunctor.mapId Opposite Bicategory.Opposite.bicategory yoneda₀ CategoryTheory.CategoryStruct.comp leftUnitor	—	—
yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category precomposing Opposite Bicategory.Opposite.bicategory Bicategory.Opposite.unopFunctor CategoryTheory.Cat.Hom₂.toNatTrans Prefunctor.obj CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda₀ whiskerRight Quiver.Hom.unop Bicategory.Opposite.Hom2.unop2	—	—
yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda₀ whiskerLeft Quiver.Hom.unop	—	—
yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Opposite.unop homCategory CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Opposite Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda₀ CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	—
yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str 📖	mathematical	—	CategoryTheory.Bundled.str CategoryTheory.Category Prefunctor.obj Opposite CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda₀ Opposite.unop	—	—
yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α 📖	mathematical	—	CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj Opposite CategoryTheory.CategoryStruct.toQuiver toCategoryStruct Bicategory.Opposite.bicategory CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor yoneda₀ Opposite.unop	—	—

---

← Back to Index