Opposites

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

Statistics

Metric	Count
Definitions Hom2, unop2, bicategory, homCategory, op2, opFunctor, unopFunctor, op2, op2_unop, unop2, unop2_op	11
Theorems bicategory_associator_hom_unop2, bicategory_associator_inv_unop2, bicategory_homCategory_comp_unop2, bicategory_homCategory_id_unop2, bicategory_leftUnitor_hom_unop2, bicategory_leftUnitor_inv_unop2, bicategory_rightUnitor_hom_unop2, bicategory_rightUnitor_inv_unop2, bicategory_whiskerLeft_unop2, bicategory_whiskerRight_unop2, homCategory_comp_unop2, homCategory_id_unop2, op2_associator, op2_associator_hom, op2_associator_inv, op2_comp, op2_id, op2_id_unbop, op2_leftUnitor, op2_leftUnitor_hom, op2_leftUnitor_inv, op2_rightUnitor, op2_rightUnitor_hom, op2_rightUnitor_inv, op2_unop2, op2_whiskerLeft, op2_whiskerRight, opFunctor_map, opFunctor_obj, unop2_comp, unop2_id, unop2_id_bop, unop2_op2, unopFunctor_map, unopFunctor_obj, op2_hom_unop2, op2_inv_unop2, op2_unop_hom_unop2, op2_unop_inv_unop2, unop2_hom, unop2_inv, unop2_op2, unop2_op_hom, unop2_op_inv	44
Total	55

Bicategory.Opposite

Definitions

Name	Category	Theorems
Hom2 📖	CompData	—
bicategory 📖	CompOp	57 math math: op2_associator, op2_associator_inv, op2_whiskerLeft, CategoryTheory.Bicategory.postcomp₂_app_toFunctor_obj, CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_inv_toNatTrans_app, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, bicategory_associator_hom_unop2, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_inv_toNatTrans_app, bicategory_leftUnitor_hom_unop2, op2_whiskerRight, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_hom_toNatTrans_app, CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, CategoryTheory.Bicategory.postcomposing₂_map_as_app_toNatTrans_app, bicategory_leftUnitor_inv_unop2, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, CategoryTheory.Bicategory.postcomposing₂_obj_naturality_hom_toNatTrans_app, op2_rightUnitor_inv, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_map, bicategory_whiskerRight_unop2, CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, CategoryTheory.Bicategory.yoneda_mapId_inv_as_app_toNatTrans_app, CategoryTheory.Bicategory.postcomp₂_naturality_hom_toNatTrans_app, op2_rightUnitor, op2_rightUnitor_hom, CategoryTheory.Bicategory.postcomp₂_app_toFunctor_map, op2_leftUnitor_hom, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, CategoryTheory.Bicategory.yoneda₀_mapId_hom_toNatTrans_app, CategoryTheory.Bicategory.yoneda₀_mapId_inv_toNatTrans_app, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_hom_toNatTrans_app, CategoryTheory.Bicategory.yoneda₀_mapComp_inv_toNatTrans_app, CategoryTheory.Bicategory.postcomposing₂_obj_app_toFunctor_map, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str, op2_leftUnitor_inv, CategoryTheory.Bicategory.yoneda_mapId_hom_as_app_toNatTrans_app, CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, op2_leftUnitor, bicategory_homCategory_id_unop2, bicategory_homCategory_comp_unop2, bicategory_associator_inv_unop2, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_obj, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.Bicategory.postcomposing₂_obj_app_toFunctor_obj, CategoryTheory.Bicategory.yoneda₀_mapComp_hom_toNatTrans_app, CategoryTheory.Bicategory.yoneda_mapComp_inv_as_app_toNatTrans_app, CategoryTheory.Bicategory.postcomp₂_naturality_inv_toNatTrans_app, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_inv_toNatTrans_app, op2_associator_hom, bicategory_rightUnitor_hom_unop2, bicategory_whiskerLeft_unop2, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_hom_toNatTrans_app, bicategory_rightUnitor_inv_unop2, CategoryTheory.Bicategory.postcomposing₂_obj_naturality_inv_toNatTrans_app, CategoryTheory.Bicategory.yoneda_mapComp_hom_as_app_toNatTrans_app
homCategory 📖	CompOp	26 math math: CategoryTheory.Iso.unop2_inv, bicategory_associator_hom_unop2, unop2_id_bop, unopFunctor_map, bicategory_leftUnitor_hom_unop2, CategoryTheory.Iso.op2_hom_unop2, bicategory_leftUnitor_inv_unop2, CategoryTheory.Iso.unop2_op_inv, opFunctor_obj, homCategory_comp_unop2, unopFunctor_obj, CategoryTheory.Iso.unop2_hom, op2_comp, op2_id, CategoryTheory.Iso.unop2_op_hom, CategoryTheory.Iso.op2_unop_inv_unop2, CategoryTheory.Iso.op2_unop_hom_unop2, unop2_comp, CategoryTheory.Iso.op2_inv_unop2, unop2_id, bicategory_associator_inv_unop2, opFunctor_map, homCategory_id_unop2, op2_id_unbop, bicategory_rightUnitor_hom_unop2, bicategory_rightUnitor_inv_unop2
op2 📖	CompOp	14 math math: op2_unop2, op2_associator_inv, op2_whiskerLeft, op2_whiskerRight, op2_rightUnitor_inv, op2_rightUnitor_hom, op2_comp, op2_leftUnitor_hom, op2_id, op2_leftUnitor_inv, unop2_op2, opFunctor_map, op2_id_unbop, op2_associator_hom
opFunctor 📖	CompOp	10 math math: bicategory_leftUnitor_hom_unop2, CategoryTheory.Iso.op2_hom_unop2, bicategory_leftUnitor_inv_unop2, opFunctor_obj, CategoryTheory.Iso.op2_unop_inv_unop2, CategoryTheory.Iso.op2_unop_hom_unop2, CategoryTheory.Iso.op2_inv_unop2, opFunctor_map, bicategory_rightUnitor_hom_unop2, bicategory_rightUnitor_inv_unop2
unopFunctor 📖	CompOp	4 math math: unopFunctor_map, CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, unopFunctor_obj, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bicategory_associator_hom_unop2 📖	mathematical	—	Hom2.unop2 Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Opposite.unop CategoryTheory.CategoryStruct.comp Quiver.Hom.unop CategoryTheory.Iso.hom Opposite Quiver.opposite homCategory CategoryTheory.Bicategory.associator bicategory CategoryTheory.Iso.inv CategoryTheory.Bicategory.homCategory	—	—
bicategory_associator_inv_unop2 📖	mathematical	—	Hom2.unop2 Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Opposite.unop CategoryTheory.CategoryStruct.comp Quiver.Hom.unop CategoryTheory.Iso.inv Opposite Quiver.opposite homCategory CategoryTheory.Bicategory.associator bicategory CategoryTheory.Iso.hom CategoryTheory.Bicategory.homCategory	—	—
bicategory_homCategory_comp_unop2 📖	mathematical	—	Hom2.unop2 CategoryTheory.CategoryStruct.comp Quiver.Hom Opposite Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory bicategory Opposite.unop Quiver.Hom.unop	—	—
bicategory_homCategory_id_unop2 📖	mathematical	—	Hom2.unop2 CategoryTheory.CategoryStruct.id Quiver.Hom Opposite Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory bicategory Opposite.unop Quiver.Hom.unop	—	—
bicategory_leftUnitor_hom_unop2 📖	mathematical	—	Hom2.unop2 Opposite.op Opposite.unop CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite homCategory opFunctor CategoryTheory.CategoryStruct.comp Quiver.Hom.unop CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom CategoryTheory.Bicategory.leftUnitor bicategory CategoryTheory.Bicategory.rightUnitor	—	—
bicategory_leftUnitor_inv_unop2 📖	mathematical	—	Hom2.unop2 Opposite.op Opposite.unop CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite homCategory opFunctor CategoryTheory.CategoryStruct.comp Quiver.Hom.unop CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv CategoryTheory.Bicategory.leftUnitor bicategory CategoryTheory.Bicategory.rightUnitor	—	—
bicategory_rightUnitor_hom_unop2 📖	mathematical	—	Hom2.unop2 Opposite.op Opposite.unop CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite homCategory opFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id Quiver.Hom.unop CategoryTheory.Iso.hom CategoryTheory.Bicategory.rightUnitor bicategory CategoryTheory.Bicategory.leftUnitor	—	—
bicategory_rightUnitor_inv_unop2 📖	mathematical	—	Hom2.unop2 Opposite.op Opposite.unop CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite homCategory opFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id Quiver.Hom.unop CategoryTheory.Iso.inv CategoryTheory.Bicategory.rightUnitor bicategory CategoryTheory.Bicategory.leftUnitor	—	—
bicategory_whiskerLeft_unop2 📖	mathematical	—	Hom2.unop2 Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.comp Quiver.Hom.unop CategoryTheory.Bicategory.whiskerLeft Opposite bicategory CategoryTheory.Bicategory.whiskerRight	—	—
bicategory_whiskerRight_unop2 📖	mathematical	—	Hom2.unop2 Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.comp Quiver.Hom.unop CategoryTheory.Bicategory.whiskerRight Opposite bicategory CategoryTheory.Bicategory.whiskerLeft	—	—
homCategory_comp_unop2 📖	mathematical	—	Hom2.unop2 CategoryTheory.CategoryStruct.comp Quiver.Hom Opposite Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory Opposite.unop CategoryTheory.Bicategory.homCategory Quiver.Hom.unop	—	—
homCategory_id_unop2 📖	mathematical	—	Hom2.unop2 CategoryTheory.CategoryStruct.id Quiver.Hom Opposite Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory Opposite.unop CategoryTheory.Bicategory.homCategory Quiver.Hom.unop	—	—
op2_associator 📖	mathematical	—	CategoryTheory.Iso.op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.associator CategoryTheory.Iso.symm Quiver.Hom Opposite CategoryTheory.CategoryStruct.toQuiver bicategory Opposite.op CategoryTheory.Bicategory.homCategory Quiver.Hom.op	—	—
op2_associator_hom 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.Iso.symm	—	—
op2_associator_inv 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.Iso.symm	—	—
op2_comp 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite Opposite.op homCategory Quiver.Hom.op	—	—
op2_id 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite Opposite.op homCategory Quiver.Hom.op	—	—
op2_id_unbop 📖	mathematical	—	op2 Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite homCategory	—	—
op2_leftUnitor 📖	mathematical	—	CategoryTheory.Iso.op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.leftUnitor CategoryTheory.Bicategory.rightUnitor Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	—
op2_leftUnitor_hom 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.Bicategory.rightUnitor	—	—
op2_leftUnitor_inv 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.Bicategory.rightUnitor	—	—
op2_rightUnitor 📖	mathematical	—	CategoryTheory.Iso.op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.rightUnitor CategoryTheory.Bicategory.leftUnitor Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	—
op2_rightUnitor_hom 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.Bicategory.leftUnitor	—	—
op2_rightUnitor_inv 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.Bicategory.leftUnitor	—	—
op2_unop2 📖	mathematical	—	op2 Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Hom2.unop2	—	—
op2_whiskerLeft 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Bicategory.whiskerRight Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	—
op2_whiskerRight 📖	mathematical	—	op2 CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.whiskerLeft Opposite bicategory Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	—
opFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite Opposite.op homCategory opFunctor op2	—	—
opFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite Opposite.op homCategory opFunctor Quiver.Hom.op	—	—
unop2_comp 📖	mathematical	—	Hom2.unop2 CategoryTheory.CategoryStruct.comp Quiver.Hom Opposite Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory Opposite.unop CategoryTheory.Bicategory.homCategory Quiver.Hom.unop	—	—
unop2_id 📖	mathematical	—	Hom2.unop2 CategoryTheory.CategoryStruct.id Quiver.Hom Opposite Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory Opposite.unop CategoryTheory.Bicategory.homCategory Quiver.Hom.unop	—	—
unop2_id_bop 📖	mathematical	—	Hom2.unop2 Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id Quiver.Hom Opposite Quiver.opposite CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.Bicategory.homCategory	—	—
unop2_op2 📖	mathematical	—	Hom2.unop2 Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct op2	—	—
unopFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom Opposite Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct homCategory Opposite.unop CategoryTheory.Bicategory.homCategory unopFunctor Hom2.unop2	—	—
unopFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom Opposite Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct homCategory Opposite.unop CategoryTheory.Bicategory.homCategory unopFunctor Quiver.Hom.unop	—	—

Bicategory.Opposite.Hom2

Definitions

Name	Category	Theorems
unop2 📖	CompOp	28 math math: Bicategory.Opposite.op2_unop2, CategoryTheory.Iso.unop2_inv, Bicategory.Opposite.bicategory_associator_hom_unop2, Bicategory.Opposite.unop2_id_bop, Bicategory.Opposite.unopFunctor_map, Bicategory.Opposite.bicategory_leftUnitor_hom_unop2, CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.Iso.op2_hom_unop2, Bicategory.Opposite.bicategory_leftUnitor_inv_unop2, CategoryTheory.Iso.unop2_op_inv, Bicategory.Opposite.bicategory_whiskerRight_unop2, Bicategory.Opposite.homCategory_comp_unop2, CategoryTheory.Iso.unop2_hom, CategoryTheory.Iso.unop2_op_hom, CategoryTheory.Iso.op2_unop_inv_unop2, CategoryTheory.Iso.op2_unop_hom_unop2, Bicategory.Opposite.unop2_comp, Bicategory.Opposite.unop2_op2, CategoryTheory.Iso.op2_inv_unop2, Bicategory.Opposite.bicategory_homCategory_id_unop2, Bicategory.Opposite.unop2_id, Bicategory.Opposite.bicategory_homCategory_comp_unop2, Bicategory.Opposite.bicategory_associator_inv_unop2, CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, Bicategory.Opposite.homCategory_id_unop2, Bicategory.Opposite.bicategory_rightUnitor_hom_unop2, Bicategory.Opposite.bicategory_whiskerLeft_unop2, Bicategory.Opposite.bicategory_rightUnitor_inv_unop2

CategoryTheory.Iso

Definitions

Name	Category	Theorems
op2 📖	CompOp	6 math math: Bicategory.Opposite.op2_associator, unop2_op2, op2_hom_unop2, Bicategory.Opposite.op2_rightUnitor, op2_inv_unop2, Bicategory.Opposite.op2_leftUnitor
op2_unop 📖	CompOp	2 math math: op2_unop_inv_unop2, op2_unop_hom_unop2
unop2 📖	CompOp	3 math math: unop2_op2, unop2_inv, unop2_hom
unop2_op 📖	CompOp	2 math math: unop2_op_inv, unop2_op_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op2_hom_unop2 📖	mathematical	—	Bicategory.Opposite.Hom2.unop2 Opposite.op CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite Bicategory.Opposite.homCategory Bicategory.Opposite.opFunctor hom Quiver.Hom.op op2	—	—
op2_inv_unop2 📖	mathematical	—	Bicategory.Opposite.Hom2.unop2 Opposite.op CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite Bicategory.Opposite.homCategory Bicategory.Opposite.opFunctor inv Quiver.Hom.op op2	—	—
op2_unop_hom_unop2 📖	mathematical	—	Bicategory.Opposite.Hom2.unop2 Opposite.op Opposite.unop CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite Bicategory.Opposite.homCategory Bicategory.Opposite.opFunctor hom op2_unop	—	—
op2_unop_inv_unop2 📖	mathematical	—	Bicategory.Opposite.Hom2.unop2 Opposite.op Opposite.unop CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Opposite Quiver.opposite Bicategory.Opposite.homCategory Bicategory.Opposite.opFunctor inv op2_unop	—	—
unop2_hom 📖	mathematical	—	hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Opposite.unop CategoryTheory.Bicategory.homCategory Quiver.Hom.unop unop2 Bicategory.Opposite.Hom2.unop2 Opposite Quiver.opposite Bicategory.Opposite.homCategory	—	—
unop2_inv 📖	mathematical	—	inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Opposite.unop CategoryTheory.Bicategory.homCategory Quiver.Hom.unop unop2 Bicategory.Opposite.Hom2.unop2 Opposite Quiver.opposite Bicategory.Opposite.homCategory	—	—
unop2_op2 📖	mathematical	—	op2 Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct unop2	—	—
unop2_op_hom 📖	mathematical	—	hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory unop2_op Bicategory.Opposite.Hom2.unop2 Opposite.op Opposite Quiver.opposite Bicategory.Opposite.homCategory	—	—
unop2_op_inv 📖	mathematical	—	inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory unop2_op Bicategory.Opposite.Hom2.unop2 Opposite.op Opposite Quiver.opposite Bicategory.Opposite.homCategory	—	—

---

← Back to Index