Yoneda embedding is fully faithful

yoneda_done.lean

import category_theory.yoneda
import tactic.apply_fun

.

open category_theory opposite

/-! # Yoneda -/


variables (C : Type) [category.{0} C]

@[simps]
def yoneda : C ⥤ (Cᵒᵖ ⥤ Type) :=
{ obj := λ X,
  { obj := λ Y, (unop Y ⟶ X),
    map := λ Y₁ Y₂ f g, f.unop ≫ g },
  map := λ X₁ X₂ f,
  { app := λ Y g, g ≫ f } }
.


lemma yoneda_map_id {X Y : C}
  (f : X ⟶ Y) :
  ((yoneda C).map f).app (op X) (𝟙 X) = f :=
begin
  simp,
  apply category.id_comp,
end

lemma yoneda_faithful :
  faithful (yoneda C) :=
{ map_injective' := begin
    intros X Y,
    intros f g hfg,
    rw ← yoneda_map_id C f,
    rw hfg,
    rw yoneda_map_id,
  end }

def yoneda_full :
  full (yoneda C) :=
begin
  fsplit,
  { intros X Y f,
    exact f.app (op X) (𝟙 X) },
  { intros X Y η,
    simp,
    ext Z g,
    simp,
    delta unop op id,
    refl, }
end