Haskell style (i.e. using `Type` as a category) proof of the Yoneda lemma

yoneda.lean

import tactic

-- https://www.youtube.com/watch?v=l1FCXUi6Vlw

namespace yoneda

class functor (f : Type → Type) : Type 1 :=
(map : ∀ {α β : Type}, (α → β) → f α → f β)
(id_map : ∀ {α : Type}, map (id : α → α) = id)
(comp_map : ∀ {α β γ : Type} (g : α → β) (h : β → γ), map h ∘ map g = map (h ∘ g))

open yoneda.functor

class natural_transformation (f : Type → Type) (g : Type → Type) [functor f] [functor g] : Type 1 :=
(app : ∀ (α : Type), f α → g α)
(naturality : ∀ {α β : Type} (h : α → β), map h ∘ app α = app β ∘ map h)

open natural_transformation

@[reducible] def reader (ρ α : Type) : Type := ρ → α

instance {ρ : Type} : functor (reader ρ) :=
begin
  refine { map := _, id_map := _, comp_map := _ },
  { intros α β f g, exact f ∘ g },
  { intros α, ext, simp },
  { intros α β γ g h, ext, simp }
end

def yoneda (f : Type → Type) [functor f] (α : Type) : Type 1 :=
natural_transformation (reader α) f

def yoneda_lemma (f : Type → Type) [functor f] (α : Type) : yoneda f α ≃ f α :=
begin
  refine { to_fun := _, inv_fun := _, left_inv := _, right_inv := _ },
  { intro η,
    apply η.app,
    apply id },
  { intro x,
    refine { app := _, naturality := _ },
    { intros β g, exact map g x },
    { intros β γ g,
      ext y,
      simp [←function.comp_app (map g), yoneda.functor.comp_map],
      refl } },
  { intros η,
    cases η with η.app η.naturality,
    congr,
    ext β g,
    have h := η.naturality g,
    simp [←function.comp_app (map g), h, map] },
  { intros x,
    simp [yoneda.functor.id_map] }
end

end yoneda