Loogle!

Result

Found 1367 declarations mentioning TypeCat.Fun. Of these, only the first 200 are shown.

• TypeCat.Fun 📋 Mathlib.CategoryTheory.Types.Basic
  (X : Type u_1) (Y : Type u_2) : Type (max u_1 u_2)
• TypeCat.Fun.id 📋 Mathlib.CategoryTheory.Types.Basic
  (X : Type u_1) : TypeCat.Fun X X
• instConcreteCategoryTypeFun 📋 Mathlib.CategoryTheory.Types.Basic
  : CategoryTheory.ConcreteCategory (Type u) TypeCat.Fun
• TypeCat.Fun.mk 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u_1} {Y : Type u_2} (toFun : X → Y) : TypeCat.Fun X Y
• TypeCat.Fun.toFun 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u_1} {Y : Type u_2} (self : TypeCat.Fun X Y) : X → Y
• TypeCat.instFunLikeFun 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u_1} {Y : Type u_2} : FunLike (TypeCat.Fun X Y) X Y
• TypeCat.Fun.homEquiv 📋 Mathlib.CategoryTheory.Types.Basic
  (X Y : Type u) : TypeCat.Fun X Y ≃ (X → Y)
• TypeCat.Hom.hom 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : TypeCat.Hom X Y) : TypeCat.Fun X Y
• TypeCat.Hom.hom' 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (self : TypeCat.Hom X Y) : TypeCat.Fun X Y
• TypeCat.Fun.comp 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : TypeCat.Fun Y Z) (g : TypeCat.Fun X Y) : TypeCat.Fun X Z
• TypeCat.Hom.Simps.hom 📋 Mathlib.CategoryTheory.Types.Basic
  (X Y : Type u) (f : X ⟶ Y) : TypeCat.Fun X Y
• TypeCat.Fun.id_apply 📋 Mathlib.CategoryTheory.Types.Basic
  (X : Type u_1) (a : X) : (TypeCat.Fun.id X) a = a
• TypeCat.hom_ofHom 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X → Y) : TypeCat.Hom.hom (TypeCat.ofHom f) = { toFun := f }
• TypeCat.Fun.coe_mk 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u_1} {Y : Type u_2} (f : X → Y) : ⇑{ toFun := f } = f
• TypeCat.Fun.mk_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u_1} {Y : Type u_2} (f : X → Y) (x : X) : { toFun := f } x = f x
• TypeCat.Fun.ext 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u_1} {Y : Type u_2} {x y : TypeCat.Fun X Y} (toFun : x.toFun = y.toFun) : x = y
• TypeCat.Fun.toFun_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : TypeCat.Fun X Y) (x : X) : f.toFun x = f x
• TypeCat.Fun.ext_iff 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u_1} {Y : Type u_2} {x y : TypeCat.Fun X Y} : x = y ↔ x.toFun = y.toFun
• TypeCat.Hom.ext 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} {x y : TypeCat.Hom X Y} (hom' : x.hom' = y.hom') : x = y
• TypeCat.Hom.ext_iff 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} {x y : TypeCat.Hom X Y} : x = y ↔ x.hom' = y.hom'
• CategoryTheory.types_id_apply 📋 Mathlib.CategoryTheory.Types.Basic
  (X : Type u) (x : X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
• TypeCat.Fun.comp_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : TypeCat.Fun Y Z) (g : TypeCat.Fun X Y) (a✝ : X) : (f.comp g) a✝ = f.toFun (g.toFun a✝)
• TypeCat.ofHom_hom 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) : TypeCat.ofHom ⇑(TypeCat.Hom.hom f) = f
• TypeCat.ofHom_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X → Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (TypeCat.ofHom f)) x = f x
• CategoryTheory.types_id 📋 Mathlib.CategoryTheory.Types.Basic
  (X : Type u) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
• CategoryTheory.injective_of_mono 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) [hf : CategoryTheory.Mono f] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.surjective_of_epi 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) [hf : CategoryTheory.Epi f] : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.epi_iff_surjective 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.isIso_iff_bijective 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.isSplitEpi_iff_surjective 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) : CategoryTheory.IsSplitEpi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.mono_iff_injective 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.Iso.toEquiv_symm_fun 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (i : X ≅ Y) : ⇑i.toEquiv.symm = (CategoryTheory.ConcreteCategory.hom i.inv).toFun
• Equiv.toIso_hom 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (e : X ≃ Y) (x : X) : (CategoryTheory.ConcreteCategory.hom e.toIso.hom) x = e x
• Equiv.toIso_hom_hom_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (e : X ≃ Y) (x : X) : (CategoryTheory.ConcreteCategory.hom e.toIso.hom) x = e x
• TypeCat.ofHom_eq 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) : TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f) = f
• Equiv.toIso_inv 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (e : X ≃ Y) (x : Y) : (CategoryTheory.ConcreteCategory.hom e.toIso.inv) x = e.symm x
• Equiv.toIso_inv_hom_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (e : X ≃ Y) (x : Y) : (CategoryTheory.ConcreteCategory.hom e.toIso.inv) x = e.symm x
• CategoryTheory.Iso.toEquiv_fun 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (i : X ≅ Y) : ⇑i.toEquiv = ⇑(CategoryTheory.ConcreteCategory.hom i.hom)
• CategoryTheory.Iso.toEquiv_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (i : X ≅ Y) (a : X) : i.toEquiv a = (CategoryTheory.ConcreteCategory.hom i.hom) a
• CategoryTheory.ofTypeFunctor_map 📋 Mathlib.CategoryTheory.Types.Basic
  (m : Type u → Type v) [Functor m] [LawfulFunctor m] {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : (CategoryTheory.ofTypeFunctor m).map f = TypeCat.ofHom (Functor.map ⇑(TypeCat.Hom.hom f))
• CategoryTheory.Iso.toEquiv_symm_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (i : X ≅ Y) (a : Y) : i.toEquiv.symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a
• CategoryTheory.uliftFunctor_map 📋 Mathlib.CategoryTheory.Types.Basic
  {X x✝ : Type u} (f : X ⟶ x✝) : CategoryTheory.uliftFunctor.{v, u}.map f = TypeCat.ofHom fun x => { down := (CategoryTheory.ConcreteCategory.hom f) x.down }
• TypeCat.congr_arg 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) {x x' : X} (h : x = x') : (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom f) x'
• CategoryTheory.types_congr_hom 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} {f g : X ⟶ Y} (h : f = g) (x : X) : (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
• CategoryTheory.types_comp_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
• TypeCat.homEquiv_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y : Type u} (f : X ⟶ Y) : TypeCat.homEquiv f = ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.types_comp 📋 Mathlib.CategoryTheory.Types.Basic
  {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.FunctorToTypes.map_id_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} (a : F.obj X) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.id X))) a = a
• CategoryTheory.Functor.sections_property 📋 Mathlib.CategoryTheory.Types.Basic
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} (s : ↑F.sections) {j j' : J} (f : j ⟶ j') : (CategoryTheory.ConcreteCategory.hom (F.map f)) (↑s j) = ↑s j'
• CategoryTheory.FunctorToTypes.map_comp_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp f g))) a = (CategoryTheory.ConcreteCategory.hom (F.map g)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) a)
• CategoryTheory.Functor.sectionsFunctor_map 📋 Mathlib.CategoryTheory.Types.Basic
  (J : Type u) [CategoryTheory.Category.{v, u} J] {F G : CategoryTheory.Functor J (Type w)} (φ : F ⟶ G) : (CategoryTheory.Functor.sectionsFunctor J).map φ = TypeCat.ofHom fun x => ⟨fun j => (CategoryTheory.ConcreteCategory.hom (φ.app j)) (↑x j), ⋯⟩
• CategoryTheory.FunctorToTypes.comp 📋 Mathlib.CategoryTheory.Types.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G H : CategoryTheory.Functor C (Type w)) {X : C} (σ : F ⟶ G) (τ : G ⟶ H) (x : F.obj X) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.CategoryStruct.comp σ τ).app X)) x = (CategoryTheory.ConcreteCategory.hom (τ.app X)) ((CategoryTheory.ConcreteCategory.hom (σ.app X)) x)
• CategoryTheory.FunctorToTypes.naturality_symm 📋 Mathlib.CategoryTheory.Types.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type u_1)} {G : CategoryTheory.Functor C (Type u_2)} (e : (j : C) → F.obj j ≃ G.obj j) (naturality : ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)) {j j' : C} (f : j ⟶ j') : ⇑(e j').symm ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) = ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm
• AddMonCat.forget_map 📋 Mathlib.Algebra.Category.MonCat.Basic
  {X Y : AddMonCat} (f : X ⟶ Y) : ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget AddMonCat).map f)) = ⇑(CategoryTheory.ConcreteCategory.hom f)
• MonCat.forget_map 📋 Mathlib.Algebra.Category.MonCat.Basic
  {X Y : MonCat} (f : X ⟶ Y) : ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget MonCat).map f)) = ⇑(CategoryTheory.ConcreteCategory.hom f)
• RingCat.forget_map_apply 📋 Mathlib.Algebra.Category.Ring.Basic
  {R S : RingCat} (f : R ⟶ S) (x : (CategoryTheory.forget RingCat).obj R) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget RingCat).map f)) x = (CategoryTheory.ConcreteCategory.hom f) x
• CommRingCat.forget_map_apply 📋 Mathlib.Algebra.Category.Ring.Basic
  {R S : CommRingCat} (f : R ⟶ S) (x : (CategoryTheory.forget CommRingCat).obj R) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget CommRingCat).map f)) x = (CategoryTheory.ConcreteCategory.hom f) x
• CategoryTheory.Functor.CorepresentableBy.id_homEquiv_symm_apply 📋 Mathlib.CategoryTheory.Yoneda
  (X : Type v) (x : X) (a : PUnit.{v + 1}) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.CorepresentableBy.id.homEquiv.symm x)) a = x
• CategoryTheory.Functor.CorepresentableBy.id_homEquiv_apply 📋 Mathlib.CategoryTheory.Yoneda
  (X : Type v) (a : PUnit.{v + 1} ⟶ X) : CategoryTheory.Functor.CorepresentableBy.id.homEquiv a = (CategoryTheory.ConcreteCategory.hom a) PUnit.unit
• CategoryTheory.yonedaEquiv_symm_app_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x
• CategoryTheory.Functor.CorepresentableBy.homEquiv_eq 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) {Y : C} (f : X ⟶ Y) : e.homEquiv f = (CategoryTheory.ConcreteCategory.hom (F.map f)) (e.homEquiv (CategoryTheory.CategoryStruct.id X))
• CategoryTheory.Functor.CorepresentableBy.homEquiv_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} (self : F.CorepresentableBy X) {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y) : self.homEquiv (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.ConcreteCategory.hom (F.map g)) (self.homEquiv f)
• CategoryTheory.Functor.CorepresentableBy.mk 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} (homEquiv : {Y : C} → (X ⟶ Y) ≃ F.obj Y) (homEquiv_comp : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), homEquiv (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.ConcreteCategory.hom (F.map g)) (homEquiv f) := by cat_disch) : F.CorepresentableBy X
• CategoryTheory.yonedaMap_app_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v₁, u_1} D] (F : CategoryTheory.Functor C D) {Y : C} {X : Cᵒᵖ} (f : Opposite.unop X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yonedaMap F Y).app X)) f = F.map f
• CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) {Y Y' : C} (y : F.obj Y) (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (e.homEquiv.symm y) g = e.homEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map g)) y)
• CategoryTheory.uliftYonedaMap_app_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {Y : C} {X : Cᵒᵖ} (f : Opposite.unop X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.uliftYonedaMap F Y).app X)) { down := f } = { down := F.map f }
• CategoryTheory.Functor.coreprW_hom_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [F.IsCorepresentable] (X : C) (f : F.coreprX ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.coreprW.hom.app X)) f = (CategoryTheory.ConcreteCategory.hom (F.map f)) F.coreprx
• CategoryTheory.Coyoneda.fullyFaithful_preimage 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y) : CategoryTheory.Coyoneda.fullyFaithful.preimage f = Quiver.Hom.op ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.unop X))) (CategoryTheory.CategoryStruct.id (Opposite.unop X)))
• CategoryTheory.Functor.uliftCoyonedaCoreprXIso_hom_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type (max v v₁))) [F.IsCorepresentable] (X : C) (f : ULift.{v, v₁} (F.coreprX ⟶ X)) : (CategoryTheory.ConcreteCategory.hom (F.uliftCoyonedaCoreprXIso.hom.app X)) f = (CategoryTheory.ConcreteCategory.hom (F.map f.down)) F.coreprx
• CategoryTheory.Functor.RepresentableBy.homEquiv_eq 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) {X : C} (f : X ⟶ Y) : e.homEquiv f = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (e.homEquiv (CategoryTheory.CategoryStruct.id Y))
• CategoryTheory.Functor.RepresentableBy.homEquiv_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (self : F.RepresentableBy Y) {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y) : self.homEquiv (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (self.homEquiv g)
• CategoryTheory.Functor.RepresentableBy.mk 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (homEquiv : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X)) (homEquiv_comp : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), homEquiv (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (homEquiv g) := by cat_disch) : F.RepresentableBy Y
• CategoryTheory.Functor.RepresentableBy.homEquiv_unop_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {Y : C} (h : F.RepresentableBy Y) {X : Cᵒᵖ} {X' : C} (f : Opposite.op X' ⟶ X) (g : X' ⟶ Y) : h.homEquiv (CategoryTheory.CategoryStruct.comp f.unop g) = (CategoryTheory.ConcreteCategory.hom (F.map f)) (h.homEquiv g)
• CategoryTheory.Yoneda.fullyFaithful_preimage 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y) : CategoryTheory.Yoneda.fullyFaithful.preimage f = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) (CategoryTheory.CategoryStruct.id X)
• CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) {X X' : C} (x : F.obj (Opposite.op X')) (f : X ⟶ X') : CategoryTheory.CategoryStruct.comp f (e.homEquiv.symm x) = e.homEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) x)
• CategoryTheory.Functor.reprW_hom_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [F.IsRepresentable] (X : Cᵒᵖ) (f : Opposite.unop X ⟶ F.reprX) : (CategoryTheory.ConcreteCategory.hom (F.reprW.hom.app X)) f = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) F.reprx
• CategoryTheory.uliftCoyonedaEquiv_symm_apply_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {F : CategoryTheory.Functor C (Type (max w v₁))} (x : F.obj (Opposite.unop X)) (Y : C) : (CategoryTheory.uliftCoyonedaEquiv.symm x).app Y = TypeCat.ofHom fun y => (CategoryTheory.ConcreteCategory.hom (F.map y.down)) x
• CategoryTheory.uliftCoyonedaEquiv_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {F : CategoryTheory.Functor C (Type (max w v₁))} (τ : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) : CategoryTheory.uliftCoyonedaEquiv τ = (CategoryTheory.ConcreteCategory.hom (τ.app (Opposite.unop X))) { down := CategoryTheory.CategoryStruct.id (Opposite.unop X) }
• CategoryTheory.Functor.uliftYonedaReprXIso_hom_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max v v₁))) [F.IsRepresentable] (X : Cᵒᵖ) (f : ULift.{v, v₁} (Opposite.unop X ⟶ F.reprX)) : (CategoryTheory.ConcreteCategory.hom (F.uliftYonedaReprXIso.hom.app X)) f = (CategoryTheory.ConcreteCategory.hom (F.map f.down.op)) F.reprx
• CategoryTheory.coyonedaEquiv_symm_app_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)} (x : F.obj X) (Y : C) (f : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyonedaEquiv.symm x).app Y)) f = (CategoryTheory.ConcreteCategory.hom (F.map f)) x
• CategoryTheory.coyonedaEquiv_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)} (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) : CategoryTheory.coyonedaEquiv f = (CategoryTheory.ConcreteCategory.hom (f.app X)) (CategoryTheory.CategoryStruct.id X)
• CategoryTheory.sectionsFunctorNatIsoCoyoneda_hom_app_hom_apply_app_hom_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : CategoryTheory.Functor C (Type (max u₁ u₂))) (x : ↑X✝.sections) (j : C) (x✝ : ((CategoryTheory.Functor.const C).obj X).obj j) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.sectionsFunctorNatIsoCoyoneda X).hom.app X✝)) x).app j)) x✝ = ↑x j
• CategoryTheory.uliftYonedaEquiv_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (τ : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) : CategoryTheory.uliftYonedaEquiv τ = (CategoryTheory.ConcreteCategory.hom (τ.app (Opposite.op X))) { down := CategoryTheory.CategoryStruct.id X }
• CategoryTheory.map_coyonedaEquiv 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type v₁)} (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.coyonedaEquiv f) = (CategoryTheory.ConcreteCategory.hom (f.app Y)) g
• CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_hom_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : Cᵒᵖ) (X✝ : C) (x : (F.comp (CategoryTheory.uliftCoyoneda.{v₁, v₂, u₂}.obj (Opposite.op (F.obj (Opposite.unop X))))).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftCoyonedaCompWhiskeringLeft.hom.app X).app X✝)) x).down = hF.preimage x.down
• CategoryTheory.sectionsFunctorNatIsoCoyoneda_inv_app_hom_apply_coe 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : CategoryTheory.Functor C (Type (max u₁ u₂))) (x : (CategoryTheory.Functor.const C).obj X ⟶ X✝) (j : C) : ↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.sectionsFunctorNatIsoCoyoneda X).inv.app X✝)) x) j = (CategoryTheory.ConcreteCategory.hom (x.app j)) default
• CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_inv_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : Cᵒᵖ) (X✝ : C) (x : (CategoryTheory.uliftCoyoneda.{v₂, v₁, u₁}.obj (Opposite.op (Opposite.unop X))).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftCoyonedaCompWhiskeringLeft.inv.app X).app X✝)) x).down = F.map x.down
• CategoryTheory.uliftYonedaEquiv_symm_apply_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) : (CategoryTheory.uliftYonedaEquiv.symm x).app Y = TypeCat.ofHom fun y => (CategoryTheory.ConcreteCategory.hom (F.map y.down.op)) x
• CategoryTheory.yonedaEquiv_symm_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) : (CategoryTheory.yonedaEquiv.symm x).app Y = TypeCat.ofHom fun f => (CategoryTheory.ConcreteCategory.hom (F.map (Quiver.Hom.op f))) x
• CategoryTheory.yonedaEquiv_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) : CategoryTheory.yonedaEquiv f = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) (CategoryTheory.CategoryStruct.id X)
• CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_hom_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (x : (F.op.comp (CategoryTheory.uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X))).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftYonedaCompWhiskeringLeft.hom.app X).app X✝)) x).down = hF.preimage x.down
• CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_inv_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (x : (CategoryTheory.uliftYoneda.{v₂, v₁, u₁}.obj X).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftYonedaCompWhiskeringLeft.inv.app X).app X✝)) x).down = F.map x.down
• CategoryTheory.coyonedaEquiv_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor C (Type v₁)} (α : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (β : F ⟶ G) : CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.ConcreteCategory.hom (β.app X)) (CategoryTheory.coyonedaEquiv α)
• CategoryTheory.coyonedaPairing_map 📋 Mathlib.CategoryTheory.Yoneda
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : C × CategoryTheory.Functor C (Type v₁)) (α : P ⟶ Q) (β : (CategoryTheory.coyonedaPairing C).obj P) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyonedaPairing C).map α)) β = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map α.1.op) (CategoryTheory.CategoryStruct.comp β α.2)
• CategoryTheory.uliftCoyonedaEquiv_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {F G : CategoryTheory.Functor C (Type (max w v₁))} (α : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) (β : F ⟶ G) : CategoryTheory.uliftCoyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.ConcreteCategory.hom (β.app (Opposite.unop X))) (CategoryTheory.uliftCoyonedaEquiv α)
• CategoryTheory.Yoneda.obj_map_id 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Opposite.op X ⟶ Opposite.op Y) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yoneda.obj X).map f)) (CategoryTheory.CategoryStruct.id X) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yoneda.map f.unop).app (Opposite.op Y))) (CategoryTheory.CategoryStruct.id Y)
• CategoryTheory.coyonedaEquiv_naturality 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type v₁)} (f : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.coyonedaEquiv f) = CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map g.op) f)
• CategoryTheory.coyonedaEquiv_symm_map 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : CategoryTheory.Functor C (Type v₁)} (t : F.obj X) : CategoryTheory.coyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map f.op) (CategoryTheory.coyonedaEquiv.symm t)
• CategoryTheory.Functor.sectionsEquivHom_naturality 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C (Type u₂)} (f : F ⟶ G) (X : Type u₂) [Unique X] (x : ↑F.sections) : (G.sectionsEquivHom X) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.sectionsFunctor C).map f)) x) = CategoryTheory.CategoryStruct.comp ((F.sectionsEquivHom X) x) f
• CategoryTheory.map_yonedaEquiv' 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.yonedaEquiv f) = (CategoryTheory.ConcreteCategory.hom (f.app Y)) g.unop
• CategoryTheory.map_yonedaEquiv 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.map g.op)) (CategoryTheory.yonedaEquiv f) = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op Y))) g
• CategoryTheory.uliftCoyonedaEquiv_naturality 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor C (Type (max w v₁))} (f : CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj (Opposite.op X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.uliftCoyonedaEquiv f) = CategoryTheory.uliftCoyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map g.op) f)
• CategoryTheory.uliftCoyonedaEquiv_symm_map 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : CategoryTheory.Functor C (Type (max w v₁))} (t : F.obj X) : CategoryTheory.uliftCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map f.op) (CategoryTheory.uliftCoyonedaEquiv.symm t)
• CategoryTheory.coyonedaEvaluation_map_down 📋 Mathlib.CategoryTheory.Yoneda
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : C × CategoryTheory.Functor C (Type v₁)) (α : P ⟶ Q) (x : (CategoryTheory.coyonedaEvaluation C).obj P) : ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyonedaEvaluation C).map α)) x).down = (CategoryTheory.ConcreteCategory.hom (α.2.app Q.1)) ((CategoryTheory.ConcreteCategory.hom (P.2.map α.1)) x.down)
• CategoryTheory.uliftCoyonedaEquiv_symm_map_assoc 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) {F : CategoryTheory.Functor C (Type (max w v₁))} (t : F.obj X) {Z : CategoryTheory.Functor C (Type (max w v₁))} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map f.op) (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyonedaEquiv.symm t) h)
• CategoryTheory.Functor.sectionsEquivHom_naturality_symm 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C (Type u₂)} (f : F ⟶ G) (X : Type u₂) [Unique X] (τ : (CategoryTheory.Functor.const C).obj X ⟶ F) : (G.sectionsEquivHom X).symm (CategoryTheory.CategoryStruct.comp τ f) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.sectionsFunctor C).map f)) ((F.sectionsEquivHom X).symm τ)
• CategoryTheory.uliftYonedaEquiv_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (α : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) (β : F ⟶ G) : CategoryTheory.uliftYonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.ConcreteCategory.hom (β.app (Opposite.op X))) (CategoryTheory.uliftYonedaEquiv α)
• CategoryTheory.yonedaEquiv_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (α : CategoryTheory.yoneda.obj X ⟶ F) (β : F ⟶ G) : CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.ConcreteCategory.hom (β.app (Opposite.op X))) (CategoryTheory.yonedaEquiv α)
• CategoryTheory.yonedaEquiv_naturality 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) (g : Y ⟶ X) : (CategoryTheory.ConcreteCategory.hom (F.map g.op)) (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g) f)
• CategoryTheory.yonedaEquiv_symm_naturality_right 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {F F' : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : F ⟶ F') (x : F.obj (Opposite.op X)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yonedaEquiv.symm x) f = CategoryTheory.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) x)
• CategoryTheory.uliftYonedaEquiv_naturality 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (f : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.uliftYonedaEquiv f) = CategoryTheory.uliftYonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{w, v₁, u₁}.map g.unop) f)
• CategoryTheory.yonedaEquiv_naturality' 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g.unop) f)
• CategoryTheory.yonedaEquiv_symm_naturality_left 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X X' : C} (f : X' ⟶ X) (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) (x : F.obj (Opposite.op X)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) (CategoryTheory.yonedaEquiv.symm x) = CategoryTheory.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) x)
• CategoryTheory.uliftYonedaEquiv_symm_map 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (t : F.obj X) : CategoryTheory.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{w, v₁, u₁}.map f.unop) (CategoryTheory.uliftYonedaEquiv.symm t)
• CategoryTheory.yonedaEquiv_symm_map 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (t : F.obj X) : CategoryTheory.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f.unop) (CategoryTheory.yonedaEquiv.symm t)
• CategoryTheory.uliftYonedaEquiv_symm_comp 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} {X : Cᵒᵖ} (x : F.obj X) (f : F ⟶ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv.symm x) f = CategoryTheory.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op (Opposite.unop X)))) x)
• CategoryTheory.yonedaEvaluation_map_down 📋 Mathlib.CategoryTheory.Yoneda
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (α : P ⟶ Q) (x : (CategoryTheory.yonedaEvaluation C).obj P) : ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yonedaEvaluation C).map α)) x).down = (CategoryTheory.ConcreteCategory.hom (α.2.app Q.1)) ((CategoryTheory.ConcreteCategory.hom (P.2.map α.1)) x.down)
• CategoryTheory.uliftYonedaEquiv_symm_comp_assoc 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} {X : Cᵒᵖ} (x : F.obj X) (f : F ⟶ G) {Z : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv.symm x) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op (Opposite.unop X)))) x)) h
• CategoryTheory.uliftYonedaEquiv_symm_map_assoc 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (t : F.obj X) {Z : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{w, v₁, u₁}.map f.unop) (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv.symm t) h)
• CategoryTheory.Adjunction.compCoyonedaIso_inv_app_app_hom_apply 📋 Mathlib.CategoryTheory.Adjunction.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : Cᵒᵖ) (X✝ : D) (x : Opposite.unop X ⟶ G.obj X✝) : (CategoryTheory.ConcreteCategory.hom ((adj.compCoyonedaIso.inv.app X).app X✝)) x = CategoryTheory.CategoryStruct.comp (F.map x) (adj.counit.app X✝)
• CategoryTheory.Adjunction.compCoyonedaIso_hom_app_app_hom_apply 📋 Mathlib.CategoryTheory.Adjunction.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : Cᵒᵖ) (X✝ : D) (x : F.obj (Opposite.unop X) ⟶ X✝) : (CategoryTheory.ConcreteCategory.hom ((adj.compCoyonedaIso.hom.app X).app X✝)) x = CategoryTheory.CategoryStruct.comp (adj.unit.app (Opposite.unop X)) (G.map x)
• CategoryTheory.Adjunction.compUliftCoyonedaIso_inv_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Adjunction.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : Cᵒᵖ) (X✝ : D) (x : ULift.{max v₂ w, v₁} (Opposite.unop X ⟶ G.obj X✝)) : ((CategoryTheory.ConcreteCategory.hom ((adj.compUliftCoyonedaIso.inv.app X).app X✝)) x).down = CategoryTheory.CategoryStruct.comp (F.map x.down) (adj.counit.app X✝)
• CategoryTheory.Adjunction.compUliftCoyonedaIso_hom_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Adjunction.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : Cᵒᵖ) (X✝ : D) (x : ULift.{max v₁ w, v₂} (F.obj (Opposite.unop X) ⟶ X✝)) : ((CategoryTheory.ConcreteCategory.hom ((adj.compUliftCoyonedaIso.hom.app X).app X✝)) x).down = CategoryTheory.CategoryStruct.comp (adj.unit.app (Opposite.unop X)) (G.map x.down)
• CategoryTheory.Adjunction.compYonedaIso_hom_app_app_hom_apply 📋 Mathlib.CategoryTheory.Adjunction.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : D) (X✝ : Cᵒᵖ) (x : Opposite.unop X✝ ⟶ G.obj X) : (CategoryTheory.ConcreteCategory.hom ((adj.compYonedaIso.hom.app X).app X✝)) x = CategoryTheory.CategoryStruct.comp (F.map x) (adj.counit.app X)
• CategoryTheory.Adjunction.compYonedaIso_inv_app_app_hom_apply 📋 Mathlib.CategoryTheory.Adjunction.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : D) (X✝ : Cᵒᵖ) (x : F.obj (Opposite.unop X✝) ⟶ X) : (CategoryTheory.ConcreteCategory.hom ((adj.compYonedaIso.inv.app X).app X✝)) x = CategoryTheory.CategoryStruct.comp (adj.unit.app (Opposite.unop X✝)) (G.map x)
• CategoryTheory.Limits.Cone.equiv_hom_hom_apply_fst 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Cone.equiv F).hom) c).fst = Opposite.op c.pt
• CategoryTheory.Limits.Cone.equiv_hom_hom_apply_snd 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Cone.equiv F).hom) c).snd = c.π
• CategoryTheory.Limits.Cone.equiv_inv_hom_apply_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : (X : Cᵒᵖ) × ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Cone.equiv F).inv) c).pt = Opposite.unop c.fst
• CategoryTheory.Limits.Cone.equiv_inv_hom_apply_π 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : (X : Cᵒᵖ) × ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Cone.equiv F).inv) c).π = c.snd
• CategoryTheory.typeToCat_map 📋 Mathlib.CategoryTheory.Category.Cat
  {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : CategoryTheory.typeToCat.map f = (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑(CategoryTheory.ConcreteCategory.hom f))).toCatHom
• CategoryTheory.Limits.sigmaConst_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (X : C) {X✝ Y✝ : Type w} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.sigmaConst.obj X).map f = CategoryTheory.Limits.Sigma.map' ⇑(CategoryTheory.ConcreteCategory.hom f) fun x => CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.sigmaFunctor_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (X : C) {X✝ Y✝ : Type w} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.sigmaFunctor.obj X).map f = CategoryTheory.Limits.Sigma.map' ⇑(CategoryTheory.ConcreteCategory.hom f) fun x => CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.piConst_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) {X✝ Y✝ : Type wᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.piConst.obj X).map f = CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom f.unop) fun x => CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.piFunctor_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (X : C) {X✝ Y✝ : Type wᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.piFunctor.obj X).map f = CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom f.unop) fun x => CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.sigmaConst_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (n : Type w) : (CategoryTheory.Limits.sigmaConst.map f).app n = CategoryTheory.Limits.Sigma.map fun x => f
• CategoryTheory.Limits.sigmaFunctor_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : Type w) : (CategoryTheory.Limits.sigmaFunctor.map f).app T = CategoryTheory.Limits.Sigma.map fun x => f
• CategoryTheory.Limits.piConst_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (n : Type wᵒᵖ) : (CategoryTheory.Limits.piConst.map f).app n = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.Limits.piFunctor_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : Type wᵒᵖ) : (CategoryTheory.Limits.piFunctor.map f).app T = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.Limits.MonoFactorisation.fac_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {f : F ⟶ G} {X : C} (H : CategoryTheory.Limits.MonoFactorisation f) (x : F.obj X) : (CategoryTheory.ConcreteCategory.hom (H.m.app X)) ((CategoryTheory.ConcreteCategory.hom (H.e.app X)) x) = (CategoryTheory.ConcreteCategory.hom (f.app X)) x
• ModuleCat.forget_map 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  (R : Type u) [Ring R] {M N : ModuleCat R} (f : M ⟶ N) : ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget (ModuleCat R)).map f)) = ⇑(CategoryTheory.ConcreteCategory.hom f)
• AlgCat.free_map 📋 Mathlib.Algebra.Category.AlgCat.Basic
  (R : Type u) [CommRing R] {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : (AlgCat.free R).map f = AlgCat.ofHom ((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)))
• AlgCat.forget_map 📋 Mathlib.Algebra.Category.AlgCat.Basic
  (R : Type u) [CommRing R] {A B : AlgCat R} (f : A ⟶ B) : ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget (AlgCat R)).map f)) = ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.Functor.ranges_directed 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] (F : CategoryTheory.Functor C (Type u_1)) (j : C) : Directed (fun x1 x2 => x1 ⊇ x2) fun f => Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f.snd))
• CategoryTheory.Functor.ιColimitType_map 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)) {j j' : J} (f : j ⟶ j') (x : F.obj j) : F.ιColimitType j' ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = F.ιColimitType j x
• CategoryTheory.Functor.CoconeTypes.ι_naturality_apply 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes) {j j' : J} (f : j ⟶ j') (x : F.obj j) : c.ι j' ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = c.ι j x
• CategoryTheory.Functor.CoconeTypes.mk 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (pt : Type w₁) (ι : (j : J) → F.obj j → pt) (ι_naturality : ∀ {j j' : J} (f : j ⟶ j'), ι j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = ι j := by aesop) : F.CoconeTypes
• CategoryTheory.Functor.CoconeTypes.ι_naturality 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (self : F.CoconeTypes) {j j' : J} (f : j ⟶ j') : self.ι j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = self.ι j
• CategoryTheory.Functor.ιColimitType_eq_of_map_eq_map 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)) {j j' : J} (x : F.obj j) (y : F.obj j') {k : J} (f : j ⟶ k) (f' : j' ⟶ k) (H : (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f')) y) : F.ιColimitType j x = F.ιColimitType j' y
• CategoryTheory.Functor.CoconeTypes.precompose 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes) {G : CategoryTheory.Functor J (Type w₀')} (app : (j : J) → G.obj j → F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) = ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ app j) : G.CoconeTypes
• CategoryTheory.Functor.CoconeTypes.precompose_pt 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes) {G : CategoryTheory.Functor J (Type w₀')} (app : (j : J) → G.obj j → F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) = ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ app j) : (c.precompose app naturality).pt = c.pt
• CategoryTheory.Functor.CoconeTypes.precompose_ι 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes) {G : CategoryTheory.Functor J (Type w₀')} (app : (j : J) → G.obj j → F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) = ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ app j) : (c.precompose app naturality).ι = fun j => c.ι j ∘ app j
• CategoryTheory.Functor.CoconeTypes.IsColimit.precompose 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) {G : CategoryTheory.Functor J (Type w₀')} (e : (j : J) → G.obj j ≃ F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) = ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)) : (c.precompose (fun {j'} => ⇑(e j')) ⋯).IsColimit
• CategoryTheory.Functor.CoconeTypes.IsColimitCore.precompose 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimitCore) {G : CategoryTheory.Functor J (Type w₀')} (e : (j : J) → G.obj j ≃ F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) = ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)) : (c.precompose (fun {j'} => ⇑(e j')) ⋯).IsColimitCore
• CategoryTheory.Functor.CoconeTypes.isColimit_precompose_iff 📋 Mathlib.CategoryTheory.Limits.Types.ColimitType
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes) {G : CategoryTheory.Functor J (Type w₀')} (e : (j : J) → G.obj j ≃ F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) = ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)) : (c.precompose (fun {j'} => ⇑(e j')) ⋯).IsColimit ↔ c.IsColimit
• CategoryTheory.Limits.Types.jointly_surjective' 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] (x : CategoryTheory.Limits.colimit F) : ∃ j y, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) y = x
• CategoryTheory.Limits.Types.colimitEquivColimitType_apply 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasColimit F] (j : J) (x : F.obj j) : (CategoryTheory.Limits.Types.colimitEquivColimitType F) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) = Quot.mk F.ColimitTypeRel ⟨j, x⟩
• CategoryTheory.Limits.Types.colimitEquivColimitType_symm_apply 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasColimit F] (j : J) (x : F.obj j) : (CategoryTheory.Limits.Types.colimitEquivColimitType F).symm (Quot.mk F.ColimitTypeRel ⟨j, x⟩) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x
• CategoryTheory.Limits.Types.colimit_eq 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} (w : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j')) x') : Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', x'⟩
• CategoryTheory.Limits.Types.jointly_surjective 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (x : t.pt) : ∃ j y, (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) y = x
• CategoryTheory.Limits.Types.jointly_surjective_of_isColimit 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (x : t.pt) : ∃ j y, (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) y = x
• CategoryTheory.Limits.Types.Colimit.w_apply 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] {j j' : J} {x : F.obj j} (f : j ⟶ j') : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j')) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x
• CategoryTheory.Limits.Types.colimit_sound 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} (f : j ⟶ j') (w : (CategoryTheory.ConcreteCategory.hom (F.map f)) x = x') : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j')) x'
• CategoryTheory.Functor.coconeTypesEquiv_symm_apply_ι 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) (c : CategoryTheory.Limits.Cocone F) (j : J) (a : F.obj j) : (F.coconeTypesEquiv.symm c).ι j a = (CategoryTheory.ConcreteCategory.hom (c.ι.app j)) a
• CategoryTheory.Limits.Types.colimit_sound' 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} {j'' : J} (f : j ⟶ j'') (f' : j' ⟶ j'') (w : (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f')) x') : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j')) x'
• CategoryTheory.Limits.Types.Colimit.ι_desc_apply 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasColimit F] (s : CategoryTheory.Limits.Cocone F) (j : J) (x : F.obj j) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.desc F s)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) = (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x
• CategoryTheory.Limits.Types.Colimit.ι_map_apply 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F G : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimitsOfShape J (Type u)] (α : F ⟶ G) (j : J) (x : F.obj j) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colim.map α)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι G j)) ((CategoryTheory.ConcreteCategory.hom (α.app j)) x)
• CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] [CategoryTheory.Limits.HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i)) xi = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) xj ↔ ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
• CategoryTheory.Limits.Types.FilteredColimit.jointly_surjective_of_isColimit₂ 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) (x₁ x₂ : t.pt) : ∃ j x₁' x₂', (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x₁' = x₁ ∧ (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x₂' = x₂
• CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] [CategoryTheory.Limits.HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.Types.colimitCocone F).ι.app i)) xi = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.Types.colimitCocone F).ι.app j)) xj ↔ CategoryTheory.Limits.Types.FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩
• CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) {i : J} (x y : F.obj i) : (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) y ↔ ∃ j f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) y
• CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) {i j : J} {xi : F.obj i} {xj : F.obj j} : (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi = (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) xj ↔ ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
• CategoryTheory.Limits.Types.FilteredColimit.isColimitOf' 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] (t : CategoryTheory.Limits.Cocone F) (hsurj : ∀ (x : t.pt), ∃ i xi, x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi) (hinj : ∀ (i : J) (x y : (fun X => X) (F.obj i)), (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) y → ∃ k f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) y) : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Limits.Types.FilteredColimit.isColimitOf 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) (t : CategoryTheory.Limits.Cocone F) (hsurj : ∀ (x : t.pt), ∃ i xi, x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi) (hinj : ∀ (i j : J) (xi : (fun X => X) (F.obj i)) (xj : (fun X => X) (F.obj j)), (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi = (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) xj → ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj) : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Limits.Types.Limit.mk 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), (CategoryTheory.ConcreteCategory.hom (F.map f)) (x j) = x j') : CategoryTheory.Limits.limit F
• CategoryTheory.Limits.Types.limit_ext 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x y : CategoryTheory.Limits.limit F) (w : ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) y) : x = y
• CategoryTheory.Limits.Types.limit_ext_iff 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasLimit F] {x y : CategoryTheory.Limits.limit F} : x = y ↔ ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) y
• CategoryTheory.Limits.Types.Limit.π_mk 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), (CategoryTheory.ConcreteCategory.hom (F.map f)) (x j) = x j') (j : J) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) (CategoryTheory.Limits.Types.Limit.mk F x h) = x j
• CategoryTheory.Limits.Types.limitEquivSections_apply 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x : CategoryTheory.Limits.limit F) (j : J) : ↑((CategoryTheory.Limits.Types.limitEquivSections F) x) j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x
• CategoryTheory.Limits.Types.limit_ext' 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F' : CategoryTheory.Functor J (Type v)) (x y : CategoryTheory.Limits.limit F') (w : ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) y) : x = y
• CategoryTheory.Limits.Types.limit_ext'_iff 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F' : CategoryTheory.Functor J (Type v)} {x y : CategoryTheory.Limits.limit F'} : x = y ↔ ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) y
• CategoryTheory.Limits.Types.limit_ext_iff' 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F' : CategoryTheory.Functor J (Type v)) (x y : CategoryTheory.Limits.limit F') : x = y ↔ ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) y
• CategoryTheory.Limits.Types.limitEquivSections_symm_apply 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x : ↑F.sections) (j : J) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) ((CategoryTheory.Limits.Types.limitEquivSections F).symm x) = ↑x j
• CategoryTheory.Limits.Types.isLimit_iff 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cone F) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x = s j
• CategoryTheory.Limits.Types.limitConeIsLimit_lift 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type (max v u))) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Types.limitConeIsLimit F).lift s = TypeCat.ofHom fun v => ⟨fun j => (CategoryTheory.ConcreteCategory.hom (s.π.app j)) v, ⋯⟩
• CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) (x : ↑F.sections) (j : J) : (CategoryTheory.ConcreteCategory.hom (c.π.app j)) ((CategoryTheory.Limits.Types.isLimitEquivSections t).symm x) = ↑x j
• CategoryTheory.Limits.Types.isLimitEquivSections_apply 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) (j : J) (x : c.pt) : ↑((CategoryTheory.Limits.Types.isLimitEquivSections t) x) j = (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x
• CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Types.Small.limitConeIsLimit F).lift s = TypeCat.ofHom fun v => (equivShrink ↑F.sections) ⟨fun j => (CategoryTheory.ConcreteCategory.hom (s.π.app j)) v, ⋯⟩
• CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map 📋 Mathlib.CategoryTheory.Limits.Types.Images
  {F : CategoryTheory.Functor ℕᵒᵖ (Type u)} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (hF : ∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (c.π.app (Opposite.op 0)))
• CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux 📋 Mathlib.CategoryTheory.Limits.Types.Images
  {F : CategoryTheory.Functor ℕᵒᵖ (Type u)} (hF : ∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.Types.limitCone F).π.app (Opposite.op 0)))
• CategoryTheory.FunctorToTypes.shrink_map 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w')) [CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} F).map f = TypeCat.ofHom (⇑(equivShrink (F.obj Y✝)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(equivShrink (F.obj X✝)).symm)
• CategoryTheory.FunctorToTypes.shrinkMap_app 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w')} (τ : F ⟶ G) [CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F] [CategoryTheory.FunctorToTypes.Small.{w, w', v, u} G] (X : C) : (CategoryTheory.FunctorToTypes.shrinkMap τ).app X = TypeCat.ofHom (⇑(equivShrink (G.obj X)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (τ.app X)) ∘ ⇑(equivShrink (F.obj X)).symm)
• CategoryTheory.shrinkCoyonedaObjObjEquiv_obj_map 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y) : CategoryTheory.shrinkCoyonedaObjObjEquiv ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).map g)) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv f) g
• CategoryTheory.shrinkCoyonedaObjObjEquiv_obj_map_assoc 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y) {Z : C} (h : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).map g)) f)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv f) (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.shrinkCoyoneda_obj_map 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).map g)) f = CategoryTheory.shrinkCoyonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv f) g)
• CategoryTheory.shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : Opposite.unop X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).map g)) (CategoryTheory.shrinkCoyonedaObjObjEquiv.symm f) = CategoryTheory.shrinkCoyonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.shrinkCoyonedaObjObjEquiv_map_app 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X X' : Cᵒᵖ} {Y : C} (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') : CategoryTheory.shrinkCoyonedaObjObjEquiv ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.map g).app Y)) f) = CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.shrinkCoyonedaObjObjEquiv f)
• CategoryTheory.shrinkCoyonedaObjObjEquiv_map_app_assoc 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X X' : Cᵒᵖ} {Y : C} (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.map g).app Y)) f)) h = CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv f) h)
• CategoryTheory.shrinkCoyonedaEquiv_comp 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {P Q : CategoryTheory.Functor C (Type w)} (α : CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X ⟶ P) (β : P ⟶ Q) : CategoryTheory.shrinkCoyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.ConcreteCategory.hom (β.app (Opposite.unop X))) (CategoryTheory.shrinkCoyonedaEquiv α)
• CategoryTheory.shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X X' : Cᵒᵖ} {Y : C} (f : Opposite.unop X ⟶ Y) (g : X ⟶ X') : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.map g).app Y)) (CategoryTheory.shrinkCoyonedaObjObjEquiv.symm f) = CategoryTheory.shrinkCoyonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g.unop f)
• CategoryTheory.shrinkCoyonedaObjObjEquiv_symm_comp 📋 Mathlib.CategoryTheory.ShrinkYoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) : CategoryTheory.shrinkCoyonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g f) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj (Opposite.op Y')).map f)) (CategoryTheory.shrinkCoyonedaObjObjEquiv.symm g)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59