DescentDataAsCoalgebra

📁 Source: Mathlib/CategoryTheory/Sites/Descent/DescentDataAsCoalgebra.lean

Statistics

Metric	Count
Definitions `DescentDataAsCoalgebra`, `hom`, `coalgebraEquivalence`, `hom`, `instCategory`, `isoMk`, `obj`, `toDescentDataAsCoalgebra`, `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso`	9
Theorems `comm`, `comm_assoc`, `ext`, `ext_iff`, `coalgebraEquivalence_counitIso_hom_app_f`, `coalgebraEquivalence_counitIso_inv_app_f`, `coalgebraEquivalence_functor_map_f`, `coalgebraEquivalence_functor_obj_A`, `coalgebraEquivalence_functor_obj_a`, `coalgebraEquivalence_inverse_map_hom`, `coalgebraEquivalence_inverse_obj_hom`, `coalgebraEquivalence_inverse_obj_obj`, `coalgebraEquivalence_unitIso_hom_app_hom`, `coalgebraEquivalence_unitIso_inv_app_hom`, `coassoc`, `coassoc_assoc`, `comp_hom`, `comp_hom_assoc`, `counit`, `counit_assoc`, `hom_ext`, `hom_ext_iff`, `id_hom`, `isoMk_hom_hom`, `isoMk_inv_hom`, `isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison`, `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f`, `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f`, `toDescentDataAsCoalgebra_map_hom`, `toDescentDataAsCoalgebra_obj_hom`, `toDescentDataAsCoalgebra_obj_obj`	31
Total	40

CategoryTheory.Pseudofunctor

Definitions

Name	Category	Theorems
`DescentDataAsCoalgebra` 📖	CompData	21 math math: `isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison`, `DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_hom`, `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f`, `toDescentDataAsCoalgebra_obj_obj`, `DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_inv_app_hom`, `toDescentDataAsCoalgebra_map_hom`, `toDescentDataAsCoalgebra_obj_hom`, `DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_a`, `DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom`, `DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_hom_app_f`, `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f`, `DescentDataAsCoalgebra.id_hom`, `DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_hom_app_hom`, `DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_obj`, `DescentDataAsCoalgebra.comp_hom_assoc`, `DescentDataAsCoalgebra.coalgebraEquivalence_functor_map_f`, `DescentDataAsCoalgebra.isoMk_inv_hom`, `DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_A`, `DescentDataAsCoalgebra.isoMk_hom_hom`, `DescentDataAsCoalgebra.comp_hom`, `DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_inv_app_f`
`toDescentDataAsCoalgebra` 📖	CompOp	6 math math: `isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison`, `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f`, `toDescentDataAsCoalgebra_obj_obj`, `toDescentDataAsCoalgebra_map_hom`, `toDescentDataAsCoalgebra_obj_hom`, `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f`
`toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso` 📖	CompOp	2 math math: `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f`, `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `DescentDataAsCoalgebra` `DescentDataAsCoalgebra.instCategory` `toDescentDataAsCoalgebra` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.comparison`	—	`CategoryTheory.Functor.isEquivalence_iff_of_iso` `CategoryTheory.Functor.isEquivalence_trans` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Functor.isEquivalence_of_comp_right`
`toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Functor.comp` `DescentDataAsCoalgebra` `DescentDataAsCoalgebra.instCategory` `toDescentDataAsCoalgebra` `CategoryTheory.Equivalence.functor` `DescentDataAsCoalgebra.coalgebraEquivalence` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Comonad.comparison` `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso` `CategoryTheory.CategoryStruct.id`	—	—
`toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Functor.comp` `DescentDataAsCoalgebra` `DescentDataAsCoalgebra.instCategory` `toDescentDataAsCoalgebra` `CategoryTheory.Equivalence.functor` `DescentDataAsCoalgebra.coalgebraEquivalence` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Comonad.comparison` `toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso` `CategoryTheory.CategoryStruct.id`	—	—
`toDescentDataAsCoalgebra_map_hom` 📖	mathematical	—	`DescentDataAsCoalgebra.Hom.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Functor.map` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.NatTrans.app` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Bicategory.Adjunction.unit` `CategoryTheory.Bicategory.Adj.Hom.adj` `DescentDataAsCoalgebra` `DescentDataAsCoalgebra.instCategory` `toDescentDataAsCoalgebra`	—	—
`toDescentDataAsCoalgebra_obj_hom` 📖	mathematical	—	`DescentDataAsCoalgebra.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `DescentDataAsCoalgebra` `DescentDataAsCoalgebra.instCategory` `toDescentDataAsCoalgebra` `CategoryTheory.Functor.map` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.NatTrans.app` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Bicategory.Adjunction.unit` `CategoryTheory.Bicategory.Adj.Hom.adj`	—	—
`toDescentDataAsCoalgebra_obj_obj` 📖	mathematical	—	`DescentDataAsCoalgebra.obj` `CategoryTheory.Functor.obj` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `DescentDataAsCoalgebra` `DescentDataAsCoalgebra.instCategory` `toDescentDataAsCoalgebra` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op`	—	—

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra

Definitions

Name	Category	Theorems
`coalgebraEquivalence` 📖	CompOp	12 math math: `coalgebraEquivalence_inverse_obj_hom`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f`, `coalgebraEquivalence_unitIso_inv_app_hom`, `coalgebraEquivalence_functor_obj_a`, `coalgebraEquivalence_inverse_map_hom`, `coalgebraEquivalence_counitIso_hom_app_f`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f`, `coalgebraEquivalence_unitIso_hom_app_hom`, `coalgebraEquivalence_inverse_obj_obj`, `coalgebraEquivalence_functor_map_f`, `coalgebraEquivalence_functor_obj_A`, `coalgebraEquivalence_counitIso_inv_app_f`
`hom` 📖	CompOp	14 math math: `counit`, `coalgebraEquivalence_inverse_obj_hom`, `coalgebraEquivalence_unitIso_inv_app_hom`, `coassoc_assoc`, `Hom.comm`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_hom`, `coalgebraEquivalence_functor_obj_a`, `coalgebraEquivalence_counitIso_hom_app_f`, `coalgebraEquivalence_unitIso_hom_app_hom`, `coalgebraEquivalence_functor_map_f`, `coassoc`, `Hom.comm_assoc`, `counit_assoc`, `coalgebraEquivalence_counitIso_inv_app_f`
`instCategory` 📖	CompOp	21 math math: `CategoryTheory.Pseudofunctor.isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison`, `coalgebraEquivalence_inverse_obj_hom`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_obj`, `coalgebraEquivalence_unitIso_inv_app_hom`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_map_hom`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_hom`, `coalgebraEquivalence_functor_obj_a`, `coalgebraEquivalence_inverse_map_hom`, `coalgebraEquivalence_counitIso_hom_app_f`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f`, `id_hom`, `coalgebraEquivalence_unitIso_hom_app_hom`, `coalgebraEquivalence_inverse_obj_obj`, `comp_hom_assoc`, `coalgebraEquivalence_functor_map_f`, `isoMk_inv_hom`, `coalgebraEquivalence_functor_obj_A`, `isoMk_hom_hom`, `comp_hom`, `coalgebraEquivalence_counitIso_inv_app_f`
`isoMk` 📖	CompOp	2 math math: `isoMk_inv_hom`, `isoMk_hom_hom`
`obj` 📖	CompOp	19 math math: `counit`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_obj`, `coalgebraEquivalence_unitIso_inv_app_hom`, `coassoc_assoc`, `Hom.comm`, `coalgebraEquivalence_counitIso_hom_app_f`, `id_hom`, `coalgebraEquivalence_unitIso_hom_app_hom`, `coalgebraEquivalence_inverse_obj_obj`, `comp_hom_assoc`, `coalgebraEquivalence_functor_map_f`, `coassoc`, `isoMk_inv_hom`, `Hom.comm_assoc`, `coalgebraEquivalence_functor_obj_A`, `counit_assoc`, `isoMk_hom_hom`, `comp_hom`, `coalgebraEquivalence_counitIso_inv_app_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coalgebraEquivalence_counitIso_hom_app_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Functor.comp` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.Coalgebra.a` `obj` `Unique.instInhabited` `hom` `Hom.hom` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `coalgebraEquivalence` `CategoryTheory.CategoryStruct.id`	—	—
`coalgebraEquivalence_counitIso_inv_app_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Functor.comp` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.Coalgebra.a` `obj` `Unique.instInhabited` `hom` `Hom.hom` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `coalgebraEquivalence` `CategoryTheory.CategoryStruct.id`	—	—
`coalgebraEquivalence_functor_map_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `obj` `Unique.instInhabited` `hom` `CategoryTheory.Functor.map` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Equivalence.functor` `coalgebraEquivalence` `Hom.hom`	—	—
`coalgebraEquivalence_functor_obj_A` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Equivalence.functor` `coalgebraEquivalence` `obj` `Unique.instInhabited`	—	—
`coalgebraEquivalence_functor_obj_a` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Equivalence.functor` `coalgebraEquivalence` `hom` `Unique.instInhabited`	—	—
`coalgebraEquivalence_inverse_map_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.Functor.map` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Equivalence.inverse` `coalgebraEquivalence` `CategoryTheory.Comonad.Coalgebra.Hom.f`	—	—
`coalgebraEquivalence_inverse_obj_hom` 📖	mathematical	—	`hom` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Equivalence.inverse` `coalgebraEquivalence` `CategoryTheory.Comonad.Coalgebra.a`	—	—
`coalgebraEquivalence_inverse_obj_obj` 📖	mathematical	—	`obj` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Equivalence.inverse` `coalgebraEquivalence` `CategoryTheory.Comonad.Coalgebra.A`	—	—
`coalgebraEquivalence_unitIso_hom_app_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `obj` `Unique.instInhabited` `hom` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `coalgebraEquivalence` `CategoryTheory.eqToHom`	—	—
`coalgebraEquivalence_unitIso_inv_app_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Adjunction.toComonad` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Adjunction.ofCat` `CategoryTheory.Bicategory.Adj.Hom.adj` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `obj` `Unique.instInhabited` `hom` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `coalgebraEquivalence` `CategoryTheory.eqToHom`	—	—
`coassoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `obj` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `hom` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Bicategory.Adjunction.unit` `CategoryTheory.Bicategory.Adj.Hom.adj`	—	—
`coassoc_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `obj` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `hom` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Bicategory.Adjunction.unit` `CategoryTheory.Bicategory.Adj.Hom.adj`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `coassoc`
`comp_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `obj`	—	—
`comp_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `obj` `Hom.hom` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_hom`
`counit` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `obj` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.CategoryStruct.id` `hom` `CategoryTheory.NatTrans.app` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Bicategory.Adjunction.counit` `CategoryTheory.Bicategory.Adj.Hom.adj`	—	—
`counit_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `obj` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `hom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Cat.Hom₂.toNatTrans` `CategoryTheory.Bicategory.Adjunction.counit` `CategoryTheory.Bicategory.Adj.Hom.adj`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `counit`
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`id_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `obj`	—	—
`isoMk_hom_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `isoMk` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `obj`	—	—
`isoMk_inv_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.Iso.inv` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra` `instCategory` `isoMk` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `obj`	—	—

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	16 math math: `ext_iff`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_inv_app_hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.hom_ext_iff`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_map_hom`, `comm`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_hom_app_f`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.id_hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_hom_app_hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.comp_hom_assoc`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_map_f`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk_inv_hom`, `comm_assoc`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk_hom_hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.comp_hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_inv_app_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.obj` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.hom` `CategoryTheory.Functor.map` `hom`	—	—
`comm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.Bicategory.Adj.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `Opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Category.opposite` `CategoryTheory.Bicategory.Adj` `CategoryTheory.Bicategory.Adj.inst` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Opposite.op` `CategoryTheory.Cat.str` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.obj` `CategoryTheory.Functor.obj` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.Bicategory.Adj.Hom.l` `Prefunctor.map` `Quiver.Hom.toLoc` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Bicategory.Adj.Hom.r` `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.hom` `CategoryTheory.Functor.map` `hom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm`
`ext` 📖	—	`hom`	—	—	—
`ext_iff` 📖	mathematical	—	`hom`	—	`ext`

---

← Back to Index