Yoneda Lemma

Yoneda.lean

namespace cat
universes u v

@[class] structure category :=
  (obj : Type u)
  (hom : obj → obj → Type v)
  (cid : ∀ {x : obj}, hom x x)
  (comp : ∀ {x y z : obj}, hom y z → hom x y → hom x z)
  (assoc : ∀ {x y z w} {f : hom x y} {g : hom y z} {h : hom z w},
    comp h (comp g f) = comp (comp h g) f)
  (id_left : ∀ {x y} {f : hom x y}, comp cid f = f)
  (id_right : ∀ {x y} {f : hom x y}, comp f cid = f)
open category

notation `∘` := comp
infixr `⟶`:25 := hom

notation f `∘[` C `]` g:25 := @comp C _ _ _ f g

@[instance] def op (C : category) : category :=
  category.mk
    (@obj C)
    (λx y, @hom C y x)
    (@cid C)
    (λx y z f g, comp g f)
    (λx y z w f g h, eq.symm assoc)
    (λx y f, id_right)
    (λx y f, id_left)

structure setmap {S S' : Type u} (A : set S) (B : set S') : Type u :=
  (mapping : S → S')
  (mapsin : ∀ x, x ∈ A → mapping x ∈ B)
open setmap

def setmap_comp {A B C : set Type} (g : setmap B C) (f : setmap A B) : setmap A C :=
  setmap.mk
    (λx, mapping g (mapping f x))
    (assume x, assume xin : x ∈ A, g.mapsin (f.mapping x) (f.mapsin x xin))

axiom setmap_eq {A B : set Type} (f g : setmap A B) : (∀ x, mapping f x = mapping g x) → f = g

instance Sets : category :=
  category.mk
    (set Type)
    (λx y, setmap x y)
    (λx, setmap.mk (λu, u) (assume x, λp, p))
    (λa b c g f, setmap_comp g f)
    (λa b c d h g f, rfl)
    (λa b f, begin apply setmap_eq, intro x, apply rfl end)
    (λa b f, begin apply setmap_eq, intro x, apply rfl end)

def homset {C : category} (a b : @obj C) : Type := set (@hom C a b)

instance Types : category :=
  category.mk
    Type
    (λx y, x → y)
    (λx u, u)
    (λa b c g f, λu, g (f u))
    (λa b c d h g f, rfl)
    (λa b f, rfl)
    (λa b f, rfl)

structure iso {C : category} (a b : @obj C) :=
  (mapr : @hom C a b)
  (mapl : @hom C b a)
  (isorl : (mapr ∘[C] mapl) = @cid C b)
  (isolr : (mapl ∘[C] mapr) = @cid C a)

notation a `≅` b := @iso _ a b
notation a `≅[` C `]` b := @iso C a b

structure functor (C : category) (D : category) :=
  (fobj : @obj C → @obj D)
  (fmap : ∀ {a b : @obj C}, @hom C a b → @hom D (fobj a) (fobj b))
  (preserve_id : ∀ {a : @obj C}, @fmap a a (@cid C a) = @cid D (fobj a))
  (preserve_comp : ∀ {a b c : @obj C} {g : @hom C b c} {f : @hom C a b},
    fmap (g ∘[C] f) = (fmap g ∘[D] fmap f))
open cat.functor

def functor_comp {C D E : category} (G : functor D E) (F : functor C D) : functor C E :=
  functor.mk
    (λx, fobj G (fobj F x))
    (λa b f, fmap G (fmap F f))
    begin intros, rw [F.preserve_id, G.preserve_id] end
    begin intros, rw [F.preserve_comp, G.preserve_comp] end

notation G `∘f` F := functor_comp G F

def functor_id {C : category} : functor C C :=
  functor.mk
    (λx, x)
    (λa b f, f)
    (λa, rfl)
    (λa b c g f, rfl)

-- inductive eqArrow {C : category} {a b : @obj C} (f : @hom C a b) : ∀ {x y : @obj C}, @hom C x y → Type
-- | arr : ∀ {g : @hom C a b}, f = g → eqArrow f g

-- axiom functor_eq {C D : category} (F G : functor C D) :
--   (∀ {a b : @obj C} (f : @hom C a b), eqArrow (fmap F f) (fmap G f)) → F = G

-- definition Cat : category :=
--   category.mk
--     category
--     functor
--     @functor_id
--     @functor_comp
--     (λa b c d F G H, functor_eq _ _ (λa b f, !eqArrow.arr (calc
--       fmap (H ∘f (G ∘f F)) f = fmap H (fmap G (fmap F f)) : rfl
--       ... = fmap ((H ∘f G) ∘f F) f : rfl)))
--     (λa b F, functor_eq _ _ (λa b f, !eqArrow.arr rfl))
--     (λa b F, functor_eq _ _ (λa b f, !eqArrow.arr rfl))

structure natrans {C D : category} (F G : functor C D) :=
  (component : ∀ (x : @obj C), @hom D (fobj F x) (fobj G x))
  (naturality : ∀ {a b : @obj C} {f : @hom C a b},
    (component b ∘[D] fmap F f) = (fmap G f ∘[D] component a))
open natrans

notation F `⇒` G := natrans F G

def natrans_comp {C D : category} {F G H : functor C D} (ε : G ⇒ H) (η : F ⇒ G) : F ⇒ H :=
  natrans.mk
    (λx, (component ε x ∘[D] component η x))
    begin
      intros,
      rw [@assoc D, ←naturality ε],
      rw [←@assoc D, naturality η],
      rw [@assoc D],
    end

def natrans_id {C D : category} {F : functor C D} : F ⇒ F :=
  natrans.mk
    (λx, @cid D (fobj F x))
    begin intros, rw [@id_right D, @id_left D] end

-- axiom natrans_eq {C D : category} {F G : functor C D} (α β : F ⇒ G) :
--   (∀ x, eqArrow (component α x) (component β x)) → α = β

-- one can define Sets-valued hom functor?
-- or Setoids-valued?

def homfunctor (C : category) (r : @obj C) : functor (op C) cat.Types :=
  functor.mk
    (λx, @hom C x r)
    (λa b f, λu, (u ∘[C] f))
    (λa, funext (assume x, id_right))
    (λa b c g f, funext (assume u, assoc))

def homnat (C : category) {a b : @obj C} (f : @hom C a b) : (homfunctor C a) ⇒ (homfunctor C b) :=
  natrans.mk
    (λx, λu, f ∘[C] u)
    (λx y k, funext (assume u, assoc))

-- def funcat (c d : category) : category :=
--   category.mk
--     (functor c d)
--     natrans
--     (λx, natrans_id)
--     (λa b c, natrans_comp)
--     (λa b c d f g h, natrans_eq _ _ (λx, eqarrow.arr assoc))
--     (λa b f, natrans_eq _ _ (λx, eqarrow.arr id_left))
--     (λa b f, natrans_eq _ _ (λx, eqarrow.arr id_right))

-- notation `[` C `,` D `]` := funcat C D
-- notation `PSh[` C `]` := [ op C, cat.Types ]

-- def yoneda (C : category) : functor C PSh[C] :=
--   functor.mk
--     (λx, homfunctor C x)
--     (λa b f, homnat C f)
--     (λa, natrans_eq _ _ (λx, !eqArrow.arr (funext (λy, id_left))))
--     (λa b c g f, natrans_eq _ _ (λx, eqArrow.arr (funext (λy, calc _ = _ : assoc))))

-- lemma Yoneda (C : category) (F : functor (op C) Types) (r : @obj C) :
--   @hom PSh[C] (fobj (yoneda C) r) F ≅[Types] fobj F r
-- := iso.mk
--   (λα, component α r (@id C r))
--   (λu, natrans.mk
--     (λx f, fmap F f u)
--     (λa b f, funext (λ (x : a ⟶ r), calc
--       ((λf, fmap F f u) ∘[Types] (fmap (fobj (yoneda C) r) f)) x = fmap F (x ∘[C] f) u : rfl
--       ... = (fmap F (f ∘[op C] x)) u : rfl
--       ... = (fmap F f ∘[Types] fmap F x) u : congr_fun !preserve_comp
--       ... = ((fmap F f) ∘[Types] (λ (f : a ⟶ r), fmap F f u)) x : rfl)))
--   (calc
--     fmap F (@id C r) = @id Types (fobj F r) : !preserve_id)
--   (funext (λα, natrans_eq _ _ (λx, eqArrow.arr (funext (λu, calc
--     fmap F u (component α r (@id C r)) = (fmap F u ∘[Types] component α r) (@id C r) : rfl
--     ... = (component α x ∘[Types] fmap (fobj (yoneda C) r) u) (@id C r) : congr_fun !naturality
--     ... = component α x (@id C r ∘[C] u) : rfl
--     ... = component α x u : congr_arg _ id_left)))))

end cat