Free

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

Statistics

Metric	Count
Definitions Free, FreeBicategory, Hom₂, mk, bicategory, categoryStruct, homCategory, instInhabitedHomOfHom, liftHom, liftHom₂, of, quiver, instInhabitedFreeBicategory	13
Theorems comp_def, id_def, liftHom_comp, liftHom_id, liftHom₂_congr, lift_mapComp, lift_mapId, lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, mk_associator_hom, mk_associator_inv, mk_id, mk_left_unitor_hom, mk_left_unitor_inv, mk_right_unitor_hom, mk_right_unitor_inv, mk_vcomp, mk_whisker_left, mk_whisker_right, of_map, of_obj	22
Total	35

CategoryTheory

Definitions

Name	Category	Theorems
Free 📖	CompOp	8 math math: Free.embedding_obj, Free.lift_linear, Free.single_comp_single, Free.embedding_map, Free.lift_obj, Free.lift_additive, Free.lift_map_single, Free.lift_map
FreeBicategory 📖	CompOp	25 math math: FreeBicategory.mk_whisker_right, FreeBicategory.lift_mapId, FreeBicategory.mk_left_unitor_inv, FreeBicategory.liftHom_id, FreeBicategory.mk_right_unitor_inv, FreeBicategory.mk_vcomp, FreeBicategory.mk_id, FreeBicategory.mk_left_unitor_hom, FreeBicategory.preinclusion_map₂, FreeBicategory.of_map, FreeBicategory.mk_whisker_left, FreeBicategory.id_def, FreeBicategory.normalize_naturality, FreeBicategory.mk_associator_hom, FreeBicategory.comp_def, FreeBicategory.mk_associator_inv, FreeBicategory.locally_thin, FreeBicategory.of_obj, FreeBicategory.lift_mapComp, FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, FreeBicategory.preinclusion_obj, FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, FreeBicategory.mk_right_unitor_hom, FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, FreeBicategory.liftHom_comp
instInhabitedFreeBicategory 📖	CompOp	—

CategoryTheory.FreeBicategory

Definitions

Name	Category	Theorems
Hom₂ 📖	CompData	8 math math: mk_left_unitor_inv, mk_right_unitor_inv, mk_id, mk_left_unitor_hom, mk_associator_hom, mk_associator_inv, lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, mk_right_unitor_hom
bicategory 📖	CompOp	16 math math: mk_whisker_right, lift_mapId, mk_left_unitor_inv, mk_right_unitor_inv, mk_left_unitor_hom, preinclusion_map₂, mk_whisker_left, normalize_naturality, mk_associator_hom, mk_associator_inv, lift_mapComp, lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, preinclusion_obj, lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, mk_right_unitor_hom, lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj
categoryStruct 📖	CompOp	12 math math: mk_left_unitor_inv, liftHom_id, mk_right_unitor_inv, mk_left_unitor_hom, mk_whisker_left, id_def, normalize_naturality, mk_associator_hom, comp_def, mk_associator_inv, mk_right_unitor_hom, liftHom_comp
homCategory 📖	CompOp	5 math math: mk_vcomp, mk_id, preinclusion_map₂, normalize_naturality, locally_thin
instInhabitedHomOfHom 📖	CompOp	—
liftHom 📖	CompOp	6 math math: lift_mapId, liftHom_id, lift_mapComp, lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, liftHom_comp
liftHom₂ 📖	CompOp	2 math math: liftHom₂_congr, lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂
of 📖	CompOp	2 math math: of_map, of_obj
quiver 📖	CompOp	5 math math: mk_vcomp, mk_id, of_map, locally_thin, of_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_def 📖	mathematical	—	Hom.comp CategoryTheory.CategoryStruct.comp CategoryTheory.FreeBicategory categoryStruct	—	—
id_def 📖	mathematical	—	Hom.id CategoryTheory.CategoryStruct.id CategoryTheory.FreeBicategory categoryStruct	—	—
liftHom_comp 📖	mathematical	—	liftHom CategoryTheory.CategoryStruct.comp CategoryTheory.FreeBicategory categoryStruct Prefunctor.obj CategoryTheory.CategoryStruct.toQuiver	—	—
liftHom_id 📖	mathematical	—	liftHom CategoryTheory.CategoryStruct.id CategoryTheory.FreeBicategory categoryStruct Prefunctor.obj CategoryTheory.CategoryStruct.toQuiver	—	—
liftHom₂_congr 📖	mathematical	Rel	liftHom₂	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Bicategory.whiskerLeft_id CategoryTheory.Bicategory.whiskerLeft_comp CategoryTheory.Bicategory.id_whiskerLeft CategoryTheory.Bicategory.comp_whiskerLeft CategoryTheory.Bicategory.id_whiskerRight CategoryTheory.Bicategory.comp_whiskerRight CategoryTheory.Bicategory.whiskerRight_id CategoryTheory.Bicategory.whiskerRight_comp CategoryTheory.Bicategory.whisker_assoc CategoryTheory.Bicategory.whisker_exchange CategoryTheory.Iso.hom_inv_id CategoryTheory.Iso.inv_hom_id CategoryTheory.Bicategory.pentagon CategoryTheory.Bicategory.triangle
lift_mapComp 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapComp CategoryTheory.FreeBicategory bicategory lift CategoryTheory.Iso.refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Prefunctor.obj CategoryTheory.Bicategory.homCategory liftHom CategoryTheory.CategoryStruct.comp	—	—
lift_mapId 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapId CategoryTheory.FreeBicategory bicategory lift CategoryTheory.Iso.refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Prefunctor.obj CategoryTheory.Bicategory.homCategory liftHom CategoryTheory.CategoryStruct.id	—	—
lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ 📖	mathematical	—	CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.FreeBicategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct bicategory Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor lift Hom₂ Rel Prefunctor.obj liftHom liftHom₂ liftHom₂_congr	—	—
lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map 📖	mathematical	—	Prefunctor.map CategoryTheory.FreeBicategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor lift liftHom	—	—
lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.FreeBicategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor lift	—	—
mk_associator_hom 📖	mathematical	—	Hom₂ CategoryTheory.CategoryStruct.comp CategoryTheory.FreeBicategory categoryStruct Rel CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.associator CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator	—	—
mk_associator_inv 📖	mathematical	—	Hom₂ CategoryTheory.CategoryStruct.comp CategoryTheory.FreeBicategory categoryStruct Rel CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.associator_inv CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator	—	—
mk_id 📖	mathematical	—	Hom₂ Rel Hom₂.id CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.FreeBicategory quiver CategoryTheory.Category.toCategoryStruct homCategory	—	—
mk_left_unitor_hom 📖	mathematical	—	Hom₂ CategoryTheory.CategoryStruct.comp CategoryTheory.FreeBicategory categoryStruct CategoryTheory.CategoryStruct.id Rel CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.left_unitor CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor	—	—
mk_left_unitor_inv 📖	mathematical	—	Hom₂ CategoryTheory.CategoryStruct.comp CategoryTheory.FreeBicategory categoryStruct CategoryTheory.CategoryStruct.id Rel CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.left_unitor_inv CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor	—	—
mk_right_unitor_hom 📖	mathematical	—	Hom₂ CategoryTheory.CategoryStruct.comp CategoryTheory.FreeBicategory categoryStruct CategoryTheory.CategoryStruct.id Rel CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.right_unitor CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor	—	—
mk_right_unitor_inv 📖	mathematical	—	Hom₂ CategoryTheory.CategoryStruct.comp CategoryTheory.FreeBicategory categoryStruct CategoryTheory.CategoryStruct.id Rel CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.right_unitor_inv CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor	—	—
mk_vcomp 📖	mathematical	—	Hom₂.vcomp CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.FreeBicategory quiver CategoryTheory.Category.toCategoryStruct homCategory	—	—
mk_whisker_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.FreeBicategory categoryStruct Hom₂.whisker_left CategoryTheory.Bicategory.whiskerLeft bicategory	—	—
mk_whisker_right 📖	mathematical	—	Hom.comp Hom₂.whisker_right CategoryTheory.Bicategory.whiskerRight CategoryTheory.FreeBicategory bicategory	—	—
of_map 📖	mathematical	—	Prefunctor.map CategoryTheory.FreeBicategory quiver of Hom.of	—	—
of_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.FreeBicategory quiver of	—	—

CategoryTheory.FreeBicategory.Hom₂

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

---

← Back to Index