Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Bundled.str

{c : Type u → Type v} → (self : CategoryTheory.Bundled c) → c ↑self

The corresponding instance of the bundled type class

Defined in
Mathlib.CategoryTheory.ConcreteCategory.Bundled
Cited by
18 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Cat.Hom.equivFunctor_apply · cited by 0Hom.equivFunctor_applyCategoryTheory.Cat.Hom.equivFunctor_symm_apply · cited by 0Hom.equivFunctor_symm_app…CategoryTheory.Cat.opEquivalence_counitIso · cited by 0Cat.opEquivalence_counitI…CategoryTheory.Cat.opEquivalence_unitIso · cited by 0Cat.opEquivalence_unitIsoCategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp · cited by 0Join.pseudofunctorLeft_to…CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id · cited by 0Join.pseudofunctorLeft_to…CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app · cited by 0GrothendieckTopology.pseu…CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str · cited by 0Bicategory.yoneda₀_toPrel…Equiv.bundledInduced_str · cited by 0Equiv.bundledInduced_strCategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp · cited by 0Join.pseudofunctorRight_t…CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id · cited by 0Join.pseudofunctorRight_t…CategoryTheory.Bundled.map · cited by 0Bundled.mapCategoryTheory.Monoidal.leftUnitor_inv · cited by 0Monoidal.leftUnitor_invCategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str · cited by 0Bicategory.yoneda_toPrela…CategoryTheory.Monoidal.rightUnitor_inv · cited by 0Monoidal.rightUnitor_invCategoryTheory.Bundled.α · cited by 736Bundled.αCategoryTheory.Bundled · cited by 42CategoryTheory.BundledBundled.strCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by19

Results whose statement or proof uses this declaration.