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)))))