To defined hom functor...?

Yoneda.v

Require Import FunctionalExtensionality.

Module Category.

Axiom proof_irrelevance : forall (P : Prop) (u v : P), u = v.

Reserved Notation "a ~> b" (at level 90).
Reserved Notation "a o; b" (at level 45, right associativity).

Class Category : Type :=
{
  obj : Type
; hom : obj -> obj -> Type where "a ~> b" := (hom a b)

; id : forall {A : obj}, A ~> A
; compose : forall {A B C : obj}, (B ~> C) -> (A ~> B) -> (A ~> C)
    where "a o; b" := (compose a b)

; left_identity : forall (A B : obj) (f : A ~> B), id o; f = f
; right_identity : forall (A B : obj) (f : A ~> B), f o; id = f
; associativity : forall (A B C D : obj) (f : A ~> B) (g : B ~> C) (h : C ~> D),
                    (h o; g) o; f = h o; (g o; f)

}.

Hint Resolve left_identity.
Hint Resolve right_identity.
Hint Resolve associativity.

Coercion obj : Category >-> Sortclass.

Infix "~>" := hom.
Infix "o;" := compose.

Definition Sets : Category.
apply Build_Category with
  (obj := Type)
  (hom := (fun A B => A -> B))
  (id := (fun _ A => A))
  (compose := (fun _ _ _ f g x => f (g x))).
- intros.
  extensionality x.
  tauto.
- intros.
  extensionality x.
  tauto.
- intros.
  extensionality x.
  tauto.
Defined.

Definition opposite (C: Category) : Category.
apply Build_Category with
  (obj := @obj C)
  (hom := (fun A B => @hom C B A))
  (id := @id C)
  (compose := (fun _ _ _ f g => g o; f)).
- intros.
  rewrite right_identity. tauto.
- intros.
  rewrite left_identity. tauto.
- intros.
  rewrite associativity. tauto.
Defined.

Notation "C ^op" := (opposite C) (at level 45).

Definition iso_pair {C: Category} {X Y: C} (f: X ~> Y) (g: Y ~> X) :=
  g o; f = id /\ f o; g = id.
Definition iso_arr {C: Category} {X Y: C} (f: X ~> Y) :=
  exists (g: Y ~> X), iso_pair f g.

Class Functor (C D: Category) :=
{
  fobj : C -> D
; fmap : forall {A B : C}, (A ~> B) -> (fobj A ~> fobj B)

; preserve_id : forall (A : C), fmap (@id C A) = @id D (fobj A)
; covariant : forall (A B C : C) (f : A ~> B) (g : B ~> C),
                fmap (g o; f) = (fmap g) o; (fmap f)
}.

Hint Resolve preserve_id.
Hint Resolve covariant.

Class ContraFunctor (C D: Category) :=
{
  fobj' : C -> D
; fmap' : forall {A B : C}, (A ~> B) -> (fobj' B ~> fobj' A)

; preserve_id' : forall (A : C), fmap' (@id C A) = @id D (fobj' A)
; contravariant : forall (A B C : C) (f : A ~> B) (g : B ~> C),
                    fmap' (g o; f) = (fmap' f) o; (fmap' g)
}.

Hint Resolve preserve_id'.
Hint Resolve contravariant.

Coercion fobj : Functor >-> Funclass.

Lemma fun_irrelevance (C D: Category) :
  forall (a: C -> D) (f g: forall {X Y: C}, (X ~> Y) -> (a X ~> a Y)) i i' c c',
    @f = @g ->
    {| fobj := a; fmap := @f; preserve_id := i; covariant := c |} =
    {| fobj := a; fmap := @g; preserve_id := i'; covariant := c' |}.
Proof.
  intros.
  subst. f_equal.
  apply proof_irrelevance.
  apply proof_irrelevance.
Qed.

Definition Id {C : Category} : Functor C C.
apply Build_Functor with
  (fobj := fun x => x)
  (fmap := fun _ _ f => f).
- tauto.
- tauto.
Defined.

Definition composedFunctor {C D E: Category}
           (F: Functor D E) (G: Functor C D) : Functor C E.
apply Build_Functor with
  (fobj := fun X => F (G X))
  (fmap := fun _ _ f => @fmap D E F _ _ (@fmap C D G _ _ f)).
- intros.
  do 2 rewrite preserve_id. tauto.
- intros.
  rewrite covariant.
  rewrite covariant. tauto.
Defined.

Class Nat {C D : Category} (F : Functor C D) (G : Functor C D) :=
{
  component : forall (A : C), (F A ~> G A)
; naturality : forall (A B : C) (f : A ~> B),
    (component B) o; (fmap f) = (fmap f) o; (component A)
}.

Hint Resolve naturality.

Definition IdNat {C D : Category} (F : Functor C D) : Nat F F.
apply Build_Nat with
  (component := fun (A : C) => @id D (fobj A)).
- intros.
  rewrite <- preserve_id.
  rewrite <- covariant.
  rewrite left_identity.
  rewrite <- preserve_id.
  rewrite <- covariant.
  rewrite right_identity.
  tauto.
Defined.

Definition composedNat {C D : Category} {F G H : Functor C D}
           (s: Nat G H) (t: Nat F G) : Nat F H.
apply Build_Nat with
  (component := fun (A : C) => (@component C D G H s A) o; (@component C D F G t A)).
- intros.
  rewrite associativity.
  rewrite naturality.
  rewrite <- associativity.
  rewrite naturality.
  rewrite <- associativity.
  tauto.
Defined.

Lemma nat_irrelevance (C D: Category) (F G: Functor C D):
  forall (s t: forall X, F X ~> G X) n m,
    s = t ->
    {| component := s; naturality := n |} =
    {| component := t; naturality := m |}.
Proof.
- intros.
  subst. f_equal.
  apply proof_irrelevance.
  
Qed.

Instance FunCat (C: Category) (D: Category) : Category :=
{
  obj := Functor C D
; hom := @Nat C D
; id := @IdNat C D
; compose := @composedNat C D
}.
Proof.
- intros.
  destruct f.
  apply nat_irrelevance.
  extensionality A0.
  simpl.
  rewrite left_identity. tauto.

- intros.
  destruct f.
  apply nat_irrelevance.
  extensionality A0.
  simpl.
  rewrite right_identity. tauto.

- intros.
  apply nat_irrelevance.
  extensionality A0.
  simpl.
  rewrite associativity.
  tauto.
Qed.

Notation "[ C , D ]" := (FunCat C D) (at level 90, right associativity).
Notation "PSh( X )" := ([X^op,Sets]).

Definition fmap_HomFunctor (C: Category) (X: C) : Functor C Sets.
(*
Error:

apply Build_Functor with
  (fobj := fun Y => hom X Y)
  (fmap := fun _ _ f g => f o; g).
*)