ShrinkYoneda

📁 Source: Mathlib/CategoryTheory/ShrinkYoneda.lean

Statistics

Metric	Count
Definitions `shrink`, `shrinkCompUliftFunctorIso`, `shrinkMap`, `fullyFaithfulShrinkYoneda`, `shrinkYoneda`, `shrinkYonedaCompEvaluationCompUliftFunctorIsoUliftFunctor`, `shrinkYonedaEquiv`, `shrinkYonedaIsoYoneda`, `shrinkYonedaObjObjEquiv`, `shrinkYonedaRepresentableBy`, `shrinkYonedaUliftFunctorIso`, `uliftYonedaIsoShrinkYoneda`	12
Theorems `shrinkCompUliftFunctorIso_hom_app`, `shrinkCompUliftFunctorIso_inv_app_down`, `shrinkMap_app`, `shrink_map`, `shrink_obj`, `instFaithfulFunctorOppositeTypeShrinkYoneda`, `instFullFunctorOppositeTypeShrinkYoneda`, `instIsRepresentableObjFunctorOppositeTypeShrinkYoneda`, `instSmallOppositeObjFunctorTypeYoneda`, `map_shrinkYonedaEquiv`, `shrinkYonedaEquiv_comp`, `shrinkYonedaEquiv_naturality`, `shrinkYonedaEquiv_shrinkYoneda_map`, `shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm`, `shrinkYonedaEquiv_symm_map`, `shrinkYonedaEquiv_symm_map_assoc`, `shrinkYonedaIsoYoneda_hom_app_app`, `shrinkYonedaIsoYoneda_inv_app_app`, `shrinkYonedaObjObjEquiv_map_app`, `shrinkYonedaObjObjEquiv_map_app_assoc`, `shrinkYonedaObjObjEquiv_obj_map`, `shrinkYonedaObjObjEquiv_obj_map_assoc`, `shrinkYonedaObjObjEquiv_symm_comp`, `shrinkYonedaRepresentableBy_homEquiv`, `shrinkYoneda_map`, `shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm`, `shrinkYoneda_obj`, `shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm`	28
Total	40

CategoryTheory

Definitions

Name	Category	Theorems
`fullyFaithfulShrinkYoneda` 📖	CompOp	—
`shrinkYoneda` 📖	CompOp	49 math math: `Presieve.shrinkFunctorHomEquiv_apply_coe`, `shrinkYoneda_map`, `shrinkYonedaEquiv_comp`, `shrinkYonedaEquiv_symm_map_assoc`, `Functor.Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app_assoc`, `Sieve.W_shrinkFunctor_ι_of_mem`, `Functor.Elements.coconeπOpCompShrinkYonedaObj_pt`, `Presieve.shrinkFunctorHomEquiv_symm_apply_app`, `shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm`, `shrinkYoneda_obj`, `Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp`, `shrinkYonedaObjObjEquiv_map_app`, `shrinkYonedaObjObjEquiv_map_app_assoc`, `GrothendieckTopology.pointBotFunctor_map_hom`, `shrinkYonedaEquiv_naturality`, `instFaithfulFunctorOppositeTypeShrinkYoneda`, `shrinkYonedaObjObjEquiv_obj_map_assoc`, `Sieve.shrinkFunctorUliftFunctorIso_inv_ι`, `Functor.Elements.instHasInitialObjOppositeTypeFlipShrinkYonedaOp`, `GrothendieckTopology.pointBotPresheafFiberIso_inv`, `shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm`, `Sieve.shrinkFunctorUliftFunctorIso_inv_ι_assoc`, `shrinkYonedaObjObjEquiv_symm_comp`, `Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map`, `Functor.Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app`, `Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply`, `Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation`, `GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map`, `shrinkYonedaRepresentableBy_homEquiv`, `Sieve.shrinkFunctorIsoFunctor_hom_app_coe`, `GrothendieckTopology.Point.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app`, `shrinkYonedaIsoYoneda_inv_app_app`, `Sieve.shrinkFunctor_obj`, `shrinkYonedaObjObjEquiv_obj_map`, `instPreservesLimitsOfSizeFunctorOppositeTypeShrinkYoneda`, `GrothendieckTopology.instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId`, `Functor.Elements.coconeπOpCompShrinkYonedaObj_ι_app`, `Presieve.extension_iff_amalgamation`, `GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber`, `instFullFunctorOppositeTypeShrinkYoneda`, `shrinkYonedaIsoYoneda_hom_app_app`, `shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm`, `map_shrinkYonedaEquiv`, `Sieve.shrinkFunctorIsoFunctor_inv_app_coe`, `GrothendieckTopology.pointBot_fiber`, `shrinkYonedaEquiv_symm_map`, `instIsRepresentableObjFunctorOppositeTypeShrinkYoneda`, `shrinkYonedaEquiv_shrinkYoneda_map`, `GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map`
`shrinkYonedaCompEvaluationCompUliftFunctorIsoUliftFunctor` 📖	CompOp	—
`shrinkYonedaEquiv` 📖	CompOp	9 math math: `shrinkYonedaEquiv_comp`, `shrinkYonedaEquiv_symm_map_assoc`, `shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm`, `shrinkYonedaEquiv_naturality`, `Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation`, `Presieve.extension_iff_amalgamation`, `map_shrinkYonedaEquiv`, `shrinkYonedaEquiv_symm_map`, `shrinkYonedaEquiv_shrinkYoneda_map`
`shrinkYonedaIsoYoneda` 📖	CompOp	2 math math: `shrinkYonedaIsoYoneda_inv_app_app`, `shrinkYonedaIsoYoneda_hom_app_app`
`shrinkYonedaObjObjEquiv` 📖	CompOp	25 math math: `Presieve.shrinkFunctorHomEquiv_apply_coe`, `Presieve.shrinkFunctorHomEquiv_symm_apply_app`, `shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm`, `shrinkYonedaObjObjEquiv_map_app`, `shrinkYonedaObjObjEquiv_map_app_assoc`, `shrinkYonedaObjObjEquiv_obj_map_assoc`, `GrothendieckTopology.pointBotPresheafFiberIso_inv`, `shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm`, `shrinkYonedaObjObjEquiv_symm_comp`, `Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map`, `Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply`, `shrinkYonedaRepresentableBy_homEquiv`, `Sieve.shrinkFunctorIsoFunctor_hom_app_coe`, `GrothendieckTopology.Point.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app`, `shrinkYonedaIsoYoneda_inv_app_app`, `Sieve.shrinkFunctor_obj`, `shrinkYonedaObjObjEquiv_obj_map`, `GrothendieckTopology.instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId`, `Functor.Elements.coconeπOpCompShrinkYonedaObj_ι_app`, `GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber`, `shrinkYonedaIsoYoneda_hom_app_app`, `shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm`, `map_shrinkYonedaEquiv`, `Sieve.shrinkFunctorIsoFunctor_inv_app_coe`, `shrinkYonedaEquiv_shrinkYoneda_map`
`shrinkYonedaRepresentableBy` 📖	CompOp	1 math math: `shrinkYonedaRepresentableBy_homEquiv`
`shrinkYonedaUliftFunctorIso` 📖	CompOp	2 math math: `Sieve.shrinkFunctorUliftFunctorIso_inv_ι`, `Sieve.shrinkFunctorUliftFunctorIso_inv_ι_assoc`
`uliftYonedaIsoShrinkYoneda` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulFunctorOppositeTypeShrinkYoneda` 📖	mathematical	—	`Functor.Faithful` `Functor` `Opposite` `Category.opposite` `types` `Functor.category` `shrinkYoneda`	—	`Functor.FullyFaithful.faithful`
`instFullFunctorOppositeTypeShrinkYoneda` 📖	mathematical	—	`Functor.Full` `Functor` `Opposite` `Category.opposite` `types` `Functor.category` `shrinkYoneda`	—	`Functor.FullyFaithful.full`
`instIsRepresentableObjFunctorOppositeTypeShrinkYoneda` 📖	mathematical	—	`Functor.IsRepresentable` `Functor.obj` `Functor` `Opposite` `Category.opposite` `types` `Functor.category` `shrinkYoneda`	—	`Functor.RepresentableBy.isRepresentable`
`instSmallOppositeObjFunctorTypeYoneda` 📖	mathematical	—	`FunctorToTypes.Small` `Opposite` `Category.opposite` `Functor.obj` `Functor` `types` `Functor.category` `yoneda`	—	`instSmallHomOfLocallySmall`
`map_shrinkYonedaEquiv` 📖	mathematical	—	`Functor.map` `Opposite` `Category.opposite` `types` `Opposite.op` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `Functor.category` `Functor.obj` `shrinkYoneda` `EquivLike.toFunLike` `Equiv.instEquivLike` `shrinkYonedaEquiv` `NatTrans.app` `Opposite.unop` `Equiv.symm` `shrinkYonedaObjObjEquiv`	—	`instSmallOppositeObjFunctorTypeYoneda` `Equiv.symm_apply_apply` `Category.comp_id`
`shrinkYonedaEquiv_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `Opposite` `Category.opposite` `types` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `Functor.obj` `shrinkYoneda` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `shrinkYonedaEquiv` `CategoryStruct.comp` `NatTrans.app`	—	—
`shrinkYonedaEquiv_naturality` 📖	mathematical	—	`Functor.map` `Opposite` `Category.opposite` `types` `Opposite.op` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `Functor.category` `Functor.obj` `shrinkYoneda` `EquivLike.toFunLike` `Equiv.instEquivLike` `shrinkYonedaEquiv` `CategoryStruct.comp`	—	`instSmallOppositeObjFunctorTypeYoneda` `Equiv.symm_apply_apply` `Category.id_comp` `Category.comp_id` `NatTrans.naturality`
`shrinkYonedaEquiv_shrinkYoneda_map` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `Opposite` `Category.opposite` `types` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `Functor.obj` `shrinkYoneda` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `shrinkYonedaEquiv` `Functor.map` `Opposite.unop` `Equiv.symm` `shrinkYonedaObjObjEquiv`	—	`instSmallOppositeObjFunctorTypeYoneda` `Equiv.symm_apply_apply` `Category.id_comp`
`shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm` 📖	mathematical	—	`NatTrans.app` `Opposite` `Category.opposite` `types` `Functor.obj` `Functor` `Functor.category` `shrinkYoneda` `DFunLike.coe` `Equiv` `Opposite.op` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `shrinkYonedaEquiv` `Opposite.unop` `shrinkYonedaObjObjEquiv` `Functor.map` `Quiver.Hom.op`	—	`Equiv.surjective` `Equiv.symm_apply_apply` `map_shrinkYonedaEquiv`
`shrinkYonedaEquiv_symm_map` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Functor.obj` `Opposite` `Category.opposite` `types` `Opposite.op` `Opposite.unop` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `shrinkYoneda` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `shrinkYonedaEquiv` `Functor.map` `CategoryStruct.comp` `Quiver.Hom.unop`	—	`Equiv.injective` `Equiv.surjective` `shrinkYonedaEquiv_naturality` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply`
`shrinkYonedaEquiv_symm_map_assoc` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Opposite` `Category.opposite` `types` `Category.toCategoryStruct` `Functor.category` `Functor.obj` `shrinkYoneda` `Opposite.unop` `DFunLike.coe` `Equiv` `Opposite.op` `Quiver.Hom` `CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `shrinkYonedaEquiv` `Functor.map` `Quiver.Hom.unop`	—	`Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shrinkYonedaEquiv_symm_map`
`shrinkYonedaIsoYoneda_hom_app_app` 📖	mathematical	—	`NatTrans.app` `Opposite` `Category.opposite` `types` `Functor.obj` `Functor` `Functor.category` `shrinkYoneda` `locallySmall_of_univLE` `UnivLE.self` `yoneda` `Iso.hom` `shrinkYonedaIsoYoneda` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `EquivLike.toFunLike` `Equiv.instEquivLike` `shrinkYonedaObjObjEquiv`	—	`locallySmall_of_univLE` `UnivLE.self`
`shrinkYonedaIsoYoneda_inv_app_app` 📖	mathematical	—	`NatTrans.app` `Opposite` `Category.opposite` `types` `Functor.obj` `Functor` `Functor.category` `yoneda` `shrinkYoneda` `locallySmall_of_univLE` `UnivLE.self` `Iso.inv` `shrinkYonedaIsoYoneda` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `shrinkYonedaObjObjEquiv`	—	`locallySmall_of_univLE` `UnivLE.self`
`shrinkYonedaObjObjEquiv_map_app` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Functor.obj` `Opposite` `Category.opposite` `types` `Functor` `Functor.category` `shrinkYoneda` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `EquivLike.toFunLike` `Equiv.instEquivLike` `shrinkYonedaObjObjEquiv` `NatTrans.app` `Functor.map` `CategoryStruct.comp`	—	`instSmallOppositeObjFunctorTypeYoneda` `Equiv.symm_apply_apply`
`shrinkYonedaObjObjEquiv_map_app_assoc` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Opposite.unop` `DFunLike.coe` `Equiv` `Functor.obj` `Opposite` `Category.opposite` `types` `Functor` `Functor.category` `shrinkYoneda` `Quiver.Hom` `CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `shrinkYonedaObjObjEquiv` `NatTrans.app` `Functor.map`	—	`Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shrinkYonedaObjObjEquiv_map_app`
`shrinkYonedaObjObjEquiv_obj_map` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Functor.obj` `Opposite` `Category.opposite` `types` `Functor` `Functor.category` `shrinkYoneda` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `EquivLike.toFunLike` `Equiv.instEquivLike` `shrinkYonedaObjObjEquiv` `Functor.map` `CategoryStruct.comp` `Quiver.Hom.unop`	—	`instSmallOppositeObjFunctorTypeYoneda` `Equiv.symm_apply_apply`
`shrinkYonedaObjObjEquiv_obj_map_assoc` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Opposite.unop` `DFunLike.coe` `Equiv` `Functor.obj` `Opposite` `Category.opposite` `types` `Functor` `Functor.category` `shrinkYoneda` `Quiver.Hom` `CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `shrinkYonedaObjObjEquiv` `Functor.map` `Quiver.Hom.unop`	—	`Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shrinkYonedaObjObjEquiv_obj_map`
`shrinkYonedaObjObjEquiv_symm_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `Opposite.op` `Functor.obj` `Opposite` `Category.opposite` `types` `Functor` `Functor.category` `shrinkYoneda` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `shrinkYonedaObjObjEquiv` `CategoryStruct.comp` `Functor.map` `Quiver.Hom.op`	—	`shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm`
`shrinkYonedaRepresentableBy_homEquiv` 📖	mathematical	—	`Functor.RepresentableBy.homEquiv` `Functor.obj` `Functor` `Opposite` `Category.opposite` `types` `Functor.category` `shrinkYoneda` `shrinkYonedaRepresentableBy` `Equiv.symm` `Opposite.op` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `shrinkYonedaObjObjEquiv`	—	—
`shrinkYoneda_map` 📖	mathematical	—	`Functor.map` `Functor` `Opposite` `Category.opposite` `types` `Functor.category` `shrinkYoneda` `FunctorToTypes.shrinkMap` `Functor.obj` `yoneda` `instSmallOppositeObjFunctorTypeYoneda`	—	`instSmallOppositeObjFunctorTypeYoneda`
`shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm` 📖	mathematical	—	`NatTrans.app` `Opposite` `Category.opposite` `types` `Functor.obj` `Functor` `Functor.category` `shrinkYoneda` `Functor.map` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `shrinkYonedaObjObjEquiv` `CategoryStruct.comp`	—	`instSmallOppositeObjFunctorTypeYoneda` `Equiv.symm_apply_apply`
`shrinkYoneda_obj` 📖	mathematical	—	`Functor.obj` `Functor` `Opposite` `Category.opposite` `types` `Functor.category` `shrinkYoneda` `FunctorToTypes.shrink` `yoneda` `instSmallOppositeObjFunctorTypeYoneda`	—	—
`shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm` 📖	mathematical	—	`Functor.map` `Opposite` `Category.opposite` `types` `Functor.obj` `Functor` `Functor.category` `shrinkYoneda` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `shrinkYonedaObjObjEquiv` `CategoryStruct.comp` `Quiver.Hom.unop`	—	`instSmallOppositeObjFunctorTypeYoneda` `Equiv.symm_apply_apply`

CategoryTheory.FunctorToTypes

Definitions

Name	Category	Theorems
`shrink` 📖	CompOp	6 math math: `shrinkMap_app`, `CategoryTheory.shrinkYoneda_obj`, `shrink_map`, `shrinkCompUliftFunctorIso_hom_app`, `shrinkCompUliftFunctorIso_inv_app_down`, `shrink_obj`
`shrinkCompUliftFunctorIso` 📖	CompOp	2 math math: `shrinkCompUliftFunctorIso_hom_app`, `shrinkCompUliftFunctorIso_inv_app_down`
`shrinkMap` 📖	CompOp	2 math math: `CategoryTheory.shrinkYoneda_map`, `shrinkMap_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shrinkCompUliftFunctorIso_hom_app` 📖	mathematical	`Small`	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.Functor.comp` `shrink` `CategoryTheory.uliftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `shrinkCompUliftFunctorIso` `DFunLike.coe` `Equiv` `CategoryTheory.Functor.obj` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Equiv.symm`	—	—
`shrinkCompUliftFunctorIso_inv_app_down` 📖	mathematical	`Small`	`CategoryTheory.Functor.obj` `CategoryTheory.types` `shrink` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.uliftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `shrinkCompUliftFunctorIso` `DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Equiv.symm`	—	—
`shrinkMap_app` 📖	mathematical	`Small`	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `shrink` `shrinkMap` `CategoryTheory.Functor.obj` `DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Equiv.symm`	—	—
`shrink_map` 📖	mathematical	`Small`	`CategoryTheory.Functor.map` `CategoryTheory.types` `shrink` `Shrink` `CategoryTheory.Functor.obj` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Equiv.symm`	—	—
`shrink_obj` 📖	mathematical	`Small`	`CategoryTheory.Functor.obj` `CategoryTheory.types` `shrink` `Shrink`	—	—

---

← Back to Index