Inductive False : Prop :=.
Inductive True : Prop := I.
Inductive eq {T : Type} (x : T) : T -> Prop := refl : eq x x.
Inductive and (X Y : Type) : Type :=
| both : X -> Y -> and X Y.
Inductive or (X Y : Type) : Type :=
| inleft : X -> or X Y
| inright : Y -> or X Y.
Inductive Sigma (T : Type) (P : T -> Type) : Type :=
| witnessS : forall t : T, P t -> Sigma T P.
Inductive Exists (T : Type) (P : T -> Prop) : Prop :=
| witnessE : forall t : T, P t -> Exists T P.

Definition pi1 {T} {P} (S : Sigma T P) : T :=
  match S with
    | witnessS t _ => t
  end.

Theorem symm (T : Type) (x y : T) : eq x y -> eq y x.
intro E; elim E; apply refl.
Defined.

Theorem trans (T : Type) (x y z : T) : eq x y -> eq y z -> eq x z.
intro E; elim E.
intro E'; elim E'.
apply refl.
Defined.

Definition Relation (T : Type) := T -> T -> Prop.

Record Equivalence {T : Type} (R : Relation T) :=
  { equivalence_reflexivity : forall x, R x x
  ; equivalence_symmetry : forall x y, R x y -> R y x
  ; equivalence_transitivity : forall x y z, R x y -> R y z -> R x z
  }.

Theorem eq_Equivalence (T : Type) : Equivalence (@eq T).
apply Build_Equivalence.
intros x; apply refl.
intros x y; apply symm.
intros x y z; apply trans.
Defined.

Theorem eq_f_Equivalence (X T : Type) (f : X -> T) : Equivalence (fun x x' => @eq T (f x) (f x')).
apply Build_Equivalence.
intros x; apply refl.
intros x y; apply symm.
intros x y z; apply trans.
Defined.

Definition Respectful
  {A : Type} (R : Relation A)
  {B : Type} (S : Relation B)
  (f : A -> B) : Prop :=
  forall a a', R a a' -> S (f a) (f a').

Record Category
  (Ob : Type) (Hom : Ob -> Ob -> Type)
  (ObEq : Relation Ob) (HomEq : forall X Y, Relation (Hom X Y)) :=
  { identity : forall {X}, Hom X X
  ; compose : forall {X Y Z}, Hom X Y -> Hom Y Z -> Hom X Z
  ; compose_respectful_left : forall {X Y Z} (f : Hom X Y),
    Respectful (HomEq Y Z) (HomEq X Z) (fun g => compose f g)
  ; compose_respectful_right : forall {X Y Z} (g : Hom Y Z),
    Respectful (HomEq X Y) (HomEq X Z) (fun f => compose f g)
  ; category_ObEq_equivalence : Equivalence ObEq
  ; category_HomEq_equivalence : forall X Y, Equivalence (HomEq X Y)
  ; category_associativity : forall X Y Z W,
    forall (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
      HomEq _ _ (compose (compose f g) h) (compose f (compose g h))
  ; category_left_identity : forall X Y,
    forall (f : Hom X Y),
      HomEq _ _ (compose identity f) f
  ; category_right_identity : forall X Y,
    forall (f : Hom X Y),
      HomEq _ _ (compose f identity) f
  }.


Section Setoids.

Record Setoid :=
  { carrier : Type
  ; relation : Relation carrier
  ; setoid_relation_eq : Equivalence relation
  }.

Definition Morphism (X Y : Setoid) :=
  Sigma (carrier X -> carrier Y) (fun f => Respectful (relation X) (relation Y) f).

Definition Morphism_Identity (X : Setoid) : Morphism X X.
apply (witnessS (carrier X -> carrier X) _ (fun x => x)).
unfold Respectful; intros; assumption.
Defined.

Definition Morphism_Compose (X Y Z : Setoid) (f : Morphism X Y) (g : Morphism Y Z) : Morphism X Z.
apply (witnessS (carrier X -> carrier Z) _ (fun x => pi1 g (pi1 f x))).
destruct f; destruct g.
unfold Respectful in *; simpl; intros.
apply r0.
apply r.
assumption.
Defined.

Definition Morphism_equality (X Y : Setoid) (m m' : Morphism X Y) :=
  forall x : carrier X,
    relation Y (pi1 m x) (pi1 m' x).

Definition Setoid_Isomorphism (S T : Setoid) : Prop :=
  Exists (and (Morphism S T) (Morphism T S)) (fun fg =>
    match fg with
      | both f g => and
         (Morphism_equality _ _ (Morphism_Compose _ _ _ f g)
                               (Morphism_Identity _))
         (Morphism_equality _ _ (Morphism_Compose _ _ _ g f)
                               (Morphism_Identity _))
    end).

Theorem Equivalence_Setoid_Isomorphism : Equivalence (fun X Y : Setoid => Setoid_Isomorphism X Y).
apply Build_Equivalence; unfold Setoid_Isomorphism.

intro; apply (witnessE _ _ (both _ _ (Morphism_Identity _) (Morphism_Identity _))).
assert (Morphism_equality x x
        (Morphism_Compose x x x (Morphism_Identity x) (Morphism_Identity x))
        (Morphism_Identity x));
unfold Morphism_equality; unfold Morphism_Compose; simpl.

intros; apply (setoid_relation_eq x).
constructor.
apply H.
apply H.

intros x y [[l r] [l' r']].
apply (witnessE _ _ (both _ _ r l)).
apply (both _ _ r' l').

intros x y z [[l r] [l' r']] [[r'' h] [r''' h']].
pose (Morphism_Compose _ _ _ l r'') as m.
pose (Morphism_Compose _ _ _ h r) as m'.
apply (witnessE _ _ (both _ _ m m')).
constructor;
unfold Morphism_equality in *; unfold Morphism_Compose in *; simpl in *; clear m; clear m';
intros.

eapply equivalence_transitivity.
apply (setoid_relation_eq x).
Focus 2.
apply l'.
assert (relation y (pi1 h (pi1 r'' (pi1 l x0))) (pi1 l x0)).
apply r'''.
unfold Morphism in r.
destruct r.
simpl.
apply r.
assumption.

eapply equivalence_transitivity.
apply (setoid_relation_eq z).
Focus 2.
apply h'.
assert (relation y (pi1 l (pi1 r (pi1 h x0))) (pi1 h x0)).
apply r'.
unfold Morphism in r'.
destruct r''.
simpl.
apply r0.
assumption.
Defined.

End Setoids.

Section SET.
  Definition SET : Category
    Setoid (fun X Y => Morphism X Y)
    (fun X Y => Setoid_Isomorphism X Y) (fun X Y f g => Morphism_equality X Y f g).
  Print Build_Category.
  apply (Build_Category
    Setoid (fun X Y => Morphism X Y)
    (fun X Y => Setoid_Isomorphism X Y) (fun X Y f g => Morphism_equality X Y f g)
    (fun X => Morphism_Identity X)
    (fun X Y Z f g => Morphism_Compose X Y Z f g));
  unfold Respectful in *;
  unfold Morphism_equality in *;
  unfold Morphism_Compose in *;
  simpl in *; intros.

  apply H.

  pose (H x).
  destruct g; simpl in *.
  unfold Respectful in *.
  apply r0.
  apply r.

  apply Equivalence_Setoid_Isomorphism.

  apply Build_Equivalence.
  intros; apply equivalence_reflexivity.
  apply (setoid_relation_eq Y).
  intros; apply equivalence_symmetry.
  apply (setoid_relation_eq Y).
  apply H.
  intros; eapply equivalence_transitivity.
  apply (setoid_relation_eq Y).
  apply H.
  apply H0.

  apply equivalence_reflexivity.
  apply (setoid_relation_eq W).
  apply equivalence_reflexivity.
  apply (setoid_relation_eq Y).
  apply equivalence_reflexivity.
  apply (setoid_relation_eq Y).
  Defined.
End SET.

(*

Definition SET : Category Set (fun X Y => X -> Y) (eq) (fun _ _ f g => forall x, eq (f x) (g x)).
apply (Build_Category
  Set (fun X Y => X -> Y) (eq) (fun _ _ f g => forall x, eq (f x) (g x))
  (fun X x => x)
  (fun X Y Z f g x => g (f x))).

unfold Respectful; intros.
apply H.

unfold Respectful; intros.
elim (H x).
apply refl.

apply eq_Equivalence.

intros; apply Build_Equivalence.
intros; apply refl.
intros; apply symm.
apply H.
intros; eapply trans.
apply H.
apply H0.

intros; apply refl.

intros; apply refl.

intros; apply refl.
Defined.

*)

Record Functor
  {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq)
  {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq') :=
  { MapOb : Ob -> Ob'
  ; MapHom : forall X Y : Ob, Hom X Y -> Hom' (MapOb X) (MapOb Y)
  ; functor_respectful : forall X Y : Ob,
    Respectful (@HomEq X Y) (@HomEq' (MapOb X) (MapOb Y)) (MapHom X Y)
  ; functor_identity : forall X,
    HomEq' _ _ (identity _ _ _ _ D) (MapHom X X (identity _ _ _ _ C))
  ; functor_compose : forall X Y Z,
    forall (f : Hom X Y) (g : Hom Y Z),
      HomEq' _ _ (MapHom _ _ (compose _ _ _ _ C f g))
                 (compose _ _ _ _ D (MapHom _ _ f) (MapHom _ _ g))
  }.

Section Opposite.
  Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).

  Definition Op : Category Ob (fun Y X => Hom X Y) ObEq (fun X Y f g => HomEq Y X f g).
  apply (Build_Category
    Ob (fun Y X => Hom X Y) ObEq (fun X Y f g => HomEq Y X f g)
    (fun X => identity _ _ _ _ C)
    (fun X Y Z f g => compose _ _ _ _ C g f)).

  unfold Respectful; intros.
  apply compose_respectful_right.
  assumption.

  unfold Respectful; intros.
  apply compose_respectful_left.
  assumption.

  apply (category_ObEq_equivalence _ _ _ _ C).
  intros X Y; pose (category_HomEq_equivalence _ _ _ _ C) as E.
  destruct (E Y X) as [axR axS axT].
  apply Build_Equivalence; assumption.

  intros.
  apply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ C).
  apply category_associativity.

  intros.
  apply category_right_identity.

  intros.
  apply category_left_identity.
  Defined.
End Opposite.

Section Functors.
  Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
  Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
  Context {Ob'' Hom'' ObEq'' HomEq''} (E : Category Ob'' Hom'' ObEq'' HomEq'').

  Definition Functor_equality (F G : Functor C D) : Prop :=
    and (forall X, ObEq' (MapOb C D F X) (MapOb C D F X))
        (forall X Y (f : Hom X Y), HomEq' _ _ (MapHom C D F X Y f) (MapHom C D G X Y f)).

  Definition Identity_Functor : Functor C C.
  apply (Build_Functor
    _ _ _ _ C
    _ _ _ _ C
    (fun X => X)
    (fun X Y f => f)
  ).

  unfold Respectful; intros; assumption.

  intros; apply equivalence_reflexivity.
  apply (category_HomEq_equivalence _ _ _ _ C X X).

  intros; apply equivalence_reflexivity.
  apply (category_HomEq_equivalence _ _ _ _ C X Z).
  Defined.

  Definition Compose_Functors (F : Functor C D) (G : Functor D E) : Functor C E.
  apply (Build_Functor
    _ _ _ _ C
    _ _ _ _ E
    (fun X => MapOb _ _ G (MapOb _ _ F X))
    (fun X Y f => MapHom _ _ G _ _ (MapHom _ _ F _ _ f))
  ).

  unfold Respectful; intros.
  apply functor_respectful.
  apply functor_respectful.
  assumption.

  intros.
  apply equivalence_transitivity with
    (y := MapHom D E G (MapOb C D F X) (MapOb C D F X)
      (identity Ob' Hom' ObEq' HomEq' D)).
  apply (category_HomEq_equivalence _ _ _ _ E _ _).
  apply functor_identity.

  apply functor_respectful.
  apply functor_identity.

  intros.
  assert (
    HomEq' _ _
    (MapHom C D F X Z (compose Ob Hom ObEq HomEq C f g))
    (compose _ _ _ _ D
      (MapHom C D F X Y f)
      (MapHom C D F Y Z g))) as lemma by apply functor_compose.
  Print functor_respectful.
  pose (functor_respectful D E G _ _ _ _ lemma) as lemma'.
  eapply equivalence_transitivity.
  apply (category_HomEq_equivalence _ _ _ _ E _ _).
  apply lemma'.
  apply (functor_compose D E G).
  Defined.
End Functors.

Section Isomorphism.
  Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).

  Record Isomorphism {X Y : Ob} (iso : Hom X Y) :=
    { inverse : Hom Y X
    ; isomorphism_left_inverse : HomEq _ _ (compose _ _ _ _ C inverse iso) (identity _ _ _ _ C)
    ; isomorphism_right_inverse : HomEq _ _ (compose _ _ _ _ C iso inverse) (identity _ _ _ _ C)
    }.

End Isomorphism.

Section Terminal.
  Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).

  Record Terminal :=
    { terminal_object : Ob
    ; terminal_morphism : forall X, Hom X terminal_object
    ; terminal_morphism_unique : forall X (f : Hom X terminal_object),
      HomEq _ _ f (terminal_morphism X)
    }.

  Theorem Terminal_Isomorphism (terminal : Terminal) :
    Isomorphism C (terminal_morphism terminal (terminal_object terminal)).
  apply (Build_Isomorphism
    C _ _ _
    (terminal_morphism terminal (terminal_object terminal))).
  apply equivalence_transitivity with (y := terminal_morphism terminal (terminal_object terminal)).
  apply (category_HomEq_equivalence _ _ _ _ C _ _).
  apply terminal_morphism_unique.
  apply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ C _ _).
  apply terminal_morphism_unique.

  apply equivalence_transitivity with (y := terminal_morphism terminal (terminal_object terminal)).
  apply (category_HomEq_equivalence _ _ _ _ C _ _).
  apply terminal_morphism_unique.
  apply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ C _ _).
  apply terminal_morphism_unique.
  Defined.

End Terminal.

Section Initial.
  Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).

  Definition Initial := @Terminal Ob (fun Y X => Hom X Y) (fun X Y f g => HomEq Y X f g).

  Definition initial_object (i : Initial) := terminal_object i.

  Definition initial_morphism (i : Initial) : forall X, Hom (initial_object i) X.
  destruct i as [termOb termMor termUniq].
  simpl.
  intro; apply termMor.
  Defined.

  Definition initial_morphism_unique (i : Initial) : forall X (f : Hom (initial_object i) X), HomEq _ _ f (initial_morphism i X).
  destruct i as [termOb termMor termUniq]; simpl.
  intros.
  apply termUniq.
  Defined.

  Theorem Initial_Isomorphism (i : Initial) :
    Isomorphism C (initial_morphism i (initial_object i)).

    pose (@Terminal_Isomorphism _ _ _ _ (Op C) i) as t.
    destruct t as [tInv tInvL tInvR]; simpl in *.

    destruct i as [iObj iMor iUniq]; simpl in *.

    apply Build_Isomorphism with (inverse := tInv).

    apply tInvR.

    apply tInvL.
  Defined.
End Initial.

Section NaturalTransform.
  Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
  Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
  Context (F : Functor C D) (G : Functor C D).

  Record NaturalTransform :=
    { eta_ : forall X, Hom' (MapOb _ _ F X) (MapOb _ _ G X)
    ; naturality : forall X Y,
      forall f : Hom X Y,
        HomEq' _ _ (compose _ _ _ _ D (MapHom _ _ F _ _ f) (eta_ Y))
                   (compose _ _ _ _ D (eta_ X) (MapHom _ _ G _ _ f))
    }.
End NaturalTransform.

Section CategoryOfSmallCats.

Record SmallCategory :=
  { S : Set
  ; R : Relation S
  ; Hom : S -> S -> Set
  ; HomR : forall X Y, Relation (Hom X Y)
  ; smallCategory_carrier : Category S Hom R HomR
  }.

Definition SmallCategory_Isomorphism : Relation SmallCategory.
unfold Relation.
intros [S_C R_C Hom_C HomR_C C] [S_D R_D Hom_D HomR_D D].
Admitted.

Definition SmallFunctor (C : SmallCategory) (D : SmallCategory) := Functor (smallCategory_carrier C) (smallCategory_carrier D).

Axiom SmallFunctor_Isomorphism : forall C D, Relation (SmallFunctor C D).

Definition CAT : Category SmallCategory SmallFunctor SmallCategory_Isomorphism SmallFunctor_Isomorphism.
Print Build_Category.
apply (Build_Category
  SmallCategory SmallFunctor SmallCategory_Isomorphism SmallFunctor_Isomorphism
  (fun X =>
    Identity_Functor (smallCategory_carrier X))
  (fun X Y Z f g =>
    Compose_Functors (smallCategory_carrier X)
                     (smallCategory_carrier Y)
                     (smallCategory_carrier Z)
                     f g)).
Admitted.

End CategoryOfSmallCats.

Section NaturalTransforms.
  Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
  Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
  Context (F : Functor C D) (G : Functor C D) (H : Functor C D).

  Context (eta : NaturalTransform C D F G).
  Context (nu : NaturalTransform C D G H).

  Definition Identity_NaturalTransform'' : NaturalTransform C C (Identity_Functor C) (Identity_Functor C).
  Print Build_NaturalTransform.
  apply (Build_NaturalTransform
    C C (Identity_Functor C) (Identity_Functor C)
    (fun X => identity _ _ _ _ C)).
  simpl; intros.
  eapply equivalence_transitivity.
  apply (category_HomEq_equivalence _ _ _ _ C).
  apply category_right_identity.
  apply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ C).
  apply category_left_identity.
  Defined.

  Definition Identity_NaturalTransform : NaturalTransform C D F F.
  Print Build_NaturalTransform.
  apply (Build_NaturalTransform
    C D F F
    (fun X => identity _ _ _ _ D)).
  simpl; intros.
  eapply equivalence_transitivity.
  apply (category_HomEq_equivalence _ _ _ _ D).
  apply category_right_identity.
  apply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ D).
  apply category_left_identity.
  Defined.

  Definition Compose_NaturalTransformations : NaturalTransform C D F H.
  Print Build_NaturalTransform.
  Print eta_.
  apply (Build_NaturalTransform
    C D F H
    (fun X => compose _ _ _ _ D (eta_ C D F G eta X) (eta_ C D G H nu X))).
  intros.
  apply equivalence_transitivity with
    (y := compose _ _ _ _ D
      (compose Ob' Hom' ObEq' HomEq' D (MapHom C D F X Y f)
        (eta_ C D F G eta Y))
      (eta_ C D G H nu Y)).
  apply (category_HomEq_equivalence _ _ _ _ D).
  eapply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ D).
  apply (category_associativity).
  apply equivalence_transitivity with
    (y := compose _ _ _ _ D (eta_ C D F G eta _)
      (compose _ _ _ _ D (MapHom C D G _ _ f)
        (eta_ C D G H nu Y))).
  apply (category_HomEq_equivalence _ _ _ _ D).

  eapply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ D).
  eapply equivalence_transitivity with
    (y := compose Ob' Hom' ObEq' HomEq' D
      (compose Ob' Hom' ObEq' HomEq' D (eta_ C D F G eta _)
        (MapHom C D G X Y f)) (eta_ C D G H nu Y)).
  apply (category_HomEq_equivalence _ _ _ _ D).
  eapply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ D).
  apply category_associativity.
  apply compose_respectful_right.
  eapply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ D).
  apply naturality.

  eapply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ D).
  eapply equivalence_transitivity with
    (y := compose Ob' Hom' ObEq' HomEq' D (eta_ C D F G eta X)
      (compose Ob' Hom' ObEq' HomEq' D
        (eta_ C D G H nu X) (MapHom C D H X Y f))).
  apply (category_HomEq_equivalence _ _ _ _ D).
  apply category_associativity.
  apply compose_respectful_left.
  eapply equivalence_symmetry.
  apply (category_HomEq_equivalence _ _ _ _ D).
  apply naturality.
  Defined.

End NaturalTransforms.

Section FunctorCategory.
  Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
  Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').

  Definition FunctorCategory : Category
    (Functor C D) (NaturalTransform C D)
    (fun F G => forall c, F c = G c) (fun _ _ _ _ => True).
  Print Identity_NaturalTransform.
  apply (Build_Category
    (Functor C D) (NaturalTransform C D)
    (fun F G => _) (fun _ _ _ _ => True)
    (fun F => Identity_NaturalTransform C D F)
    (fun F G H eta nu => Compose_NaturalTransformations C D F G H eta nu)).


(*
*** Local Variables: ***
*** coq-prog-args: ("-emacs-U" "-nois") ***
*** End: ***
*)