Yoneda template

yoneda.lean

import category_theory.yoneda
import tactic.apply_fun

.

open category_theory opposite

/-! # Yoneda -/

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

-- how to define a natural transformation
def nat_trans_hint (F : C ⥤ C) :
  F ⟶ F :=
{ app := _ }

@[simps]
def yoneda : C ⥤ (Cᵒᵖ ⥤ Type) :=
{ obj := _,
  map := _ }
.

lemma yoneda_faithful :
  faithful (yoneda C) :=
begin
  sorry
end

def yoneda_full :
  full (yoneda C) :=
begin
  sorry
end