prove that the yoneda embedding preserves limits

[semorrison]

We have everything we need for the statement:

import category_theory.yoneda
import category_theory.limits.preserves

open category_theory
open category_theory.limits

universes u

variables {C : Type u} [𝒞 : small_category C]

instance yoneda_preserves_limits : preserves_limits (@yoneda C 𝒞) := sorry

and it should be straightforward to give the construction.

This might be a good exercise for someone wanting to learn how to use the category theory library.

[semorrison]

This should probably go in src/category_theory/limits/yoneda.lean.

[semorrison]

A harder exercise is to explain the universe annotations .{u u+1 u+2} on preserves_limits, which I really better write a tutorial about...

(Actually the universe annotations I wrote were completely unnecessary.)

[semorrison]

(I noticed that map_cone_X is a missing simp lemma in category_theory/limits/cones.lean, which should probably be added as part of doing this.)