S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj α.op
x : β
⊢ S.map ((↾fun x_1 => x) ≫ f).op s = S.map (↾fun x_1 => f x).op s
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj α.op
x : β
⊢ eval S β (S.map f.op s) x = eval S α s (f x)
simp_rw [eval, ← FunctorToTypes.map_comp_apply, ← op_comp]
no goals
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj α.op
x : β
⊢ S.map ((↾fun x_1 => x) ≫ f).op s = S.map (↾fun x_1 => f x).op s
rfl