Facts about limits of functors into concrete categories
@[simp]
theorem
category_theory.limits.cone.naturality_concrete
{C : Type (u+1)}
[category_theory.large_category C]
[category_theory.concrete_category C]
{J : Type u}
[category_theory.small_category J]
{G : J ⥤ C}
(s : category_theory.limits.cone G)
{j j' : J}
(f : j ⟶ j')
(x : ↥(s.X)) :
Naturality of a cone over functors to a concrete category.
@[simp]
theorem
category_theory.limits.cocone.naturality_concrete
{C : Type (u+1)}
[category_theory.large_category C]
[category_theory.concrete_category C]
{J : Type u}
[category_theory.small_category J]
{G : J ⥤ C}
(s : category_theory.limits.cocone G)
{j j' : J}
(f : j ⟶ j')
(x : ↥(G.obj j)) :
Naturality of a cocone over functors into a concrete category.