Skip to content

Instantly share code, notes, and snippets.

@myuon
Created November 29, 2015 05:07
Show Gist options
  • Save myuon/7deee7f90984cebcd34a to your computer and use it in GitHub Desktop.
Save myuon/7deee7f90984cebcd34a to your computer and use it in GitHub Desktop.
Yoneda Lemma
import init.setoid
import data.set
open set
structure category [class] :=
(obj : Type)
(hom : obj → obj → Type)
(id : ∀ (x : obj), hom x x)
(comp : ∀ {a b c : obj}, hom b c → hom a b → hom a c)
(assoc : ∀ {a b c d} {f : hom a b} {g : hom b c} {h : hom c d},
comp h (comp g f) = comp (comp h g) f)
(id_left : ∀ {a b} {f : hom a b}, comp !id f = f)
(id_right : ∀ {a b} {f : hom a b}, comp f !id = f)
open category
namespace category
notation `∘` := comp
infixr `⟶`:25 := hom
notation f `∘[` C `]` g:25 := @comp C _ _ _ f g
definition op [instance] (C : category) : category :=
category.mk
(@obj C)
(λx y, @hom C y x)
(@id C)
(λa b c f g, comp g f)
(λa b c d f g h, eq.symm !assoc)
(λa b f, id_right)
(λa b f, id_left)
structure setmap {S S' : Type} (A : set S) (B : set S') : Type :=
(mapping : S → S')
(mapsin : ∀ x, x ∈ A → mapping x ∈ B)
open setmap
definition 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))
(take x, assume xin : x ∈ A, !mapsin (!mapsin xin))
axiom setmap_eq {A B : set Type} (f g : setmap A B) : (∀ x, mapping f x = mapping g x) → f = g
definition Sets [instance] : category :=
category.mk
(set Type)
(λx y, setmap x y)
(λx, setmap.mk (λu, u) (take 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)
definition homset {C : category} (a b : @obj C) : Type := set (@hom C a b)
definition Types [instance] : 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) = id b)
(isolr : (mapl ∘[C] mapr) = id a)
notation a `≅` b := @iso _ a b
notation a `≅[` C `]` b := @iso C a b
end category
open category
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 (@id C a) = @id 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 functor
namespace functor
variables {C D E : category}
definition functor_comp (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))
(λa, calc
fmap G (fmap F (@id C a)) = fmap G (@id D (fobj F a)) : preserve_id F
... = @id E (fobj G (fobj F a)) : preserve_id G)
(λa b c g f, calc
fmap G (fmap F (g ∘[C] f)) = fmap G (fmap F g ∘[D] fmap F f) : preserve_comp F
... = (fmap G (fmap F g) ∘[E] fmap G (fmap F f)) : preserve_comp G)
notation G `∘f` F := functor_comp G F
definition functor_id : functor C C :=
functor.mk
(λx, x)
(λa b f, f)
(λa, rfl)
(λa b c g f, rfl)
inductive eqArrow {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
end functor
open functor
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
namespace natrans
variables {C D : category} {F G H : functor C D}
notation F `⇒` G := natrans F G
definition natrans_comp (ε : G ⇒ H) (η : F ⇒ G) : F ⇒ H :=
natrans.mk
(λx, (component ε x ∘[D] component η x))
(λa b f, calc
((component ε b ∘[D] component η b) ∘[D] fmap F f) = (component ε b ∘[D] (component η b ∘[D] fmap F f)) : assoc
... = (component ε b ∘[D] (fmap G f ∘[D] component η a)) : naturality η
... = ((component ε b ∘[D] fmap G f) ∘[D] component η a) : assoc
... = ((fmap H f ∘[D] component ε a) ∘[D] component η a) : naturality ε
... = (fmap H f ∘[D] (component ε a ∘[D] component η a)) : assoc)
definition natrans_id : F ⇒ F :=
natrans.mk
(λx, @id D (fobj F x))
(λa b f, calc
(@id D (fobj F b) ∘[D] fmap F f) = fmap F f : @id_left
... = (fmap F f ∘[D] @id D (fobj F a)) : @id_right)
axiom natrans_eq {C D : category} {F G : functor C D} (α β : F ⇒ G) :
(∀ x, eqArrow (component α x) (component β x)) → α = β
end natrans
open natrans
-- one can define Sets-valued hom functor?
-- or Setoids-valued?
definition homfunctor (C : category) (r : @obj C) : functor (op C) Types :=
functor.mk
(λx, @hom C x r)
(λa b f, λu, (u ∘[C] f))
(λa, funext (take x, id_right))
(λa b c g f, funext (take u, assoc))
definition 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 (take u, assoc))
definition 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, Types ]
definition 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)))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment