Library category

Require Export Setoid.
Require Export Classes.SetoidClass.
Require Export Classes.Morphisms.
Require Export Program.

Set Implicit Arguments.
Unset Strict Implicit.

Class Cat (obj:Type)(mor: obj -> obj -> Type) := {
   mor_oid:> forall a b:obj, Setoid (mor a b);
  id: forall a, (mor a a);
  comp: forall {a b c},
           mor a b -> mor b c -> mor a c;
  comp_oid:> forall a b c: obj,
       Proper (equiv ==> equiv ==> equiv)
       (comp (a:=a) (b:=b) (c:=c));
  id_r: forall a b:obj, forall f: mor a b,
            comp f (id b) == f;
  id_l: forall a b, forall f: mor a b,
            comp (id a) f == f;
  Assoc: forall a b c d, forall (f: mor a b) (g:mor b c)
                                (h: mor c d),
           comp (comp f g) h == comp f (comp g h)
}.

Notation "x 'o' y" := (comp x y) (at level 50, left associativity).

Record Category := {
     obj:>Type;
     mor:obj -> obj -> Type;
     Cat_struct:> Cat mor}.

Notation "x ---> y" := (mor x y) (at level 50).

Existing Instance Cat_struct.

Section test.
Variable C: Category.
Variables a b: C.
Variable f: a ---> b.

Lemma idl2: id a o f == f.
Proof. apply id_l. Qed.

Lemma idr2: f o id b == f.
Proof. apply id_r. Qed.

Variables c d: C.
Variables (g: b ---> c) (h: c ---> d).

Lemma assoc2: (f o g) o h == f o (g o h).
Proof. apply Assoc. Qed.

End test.

Section cat_lemmata.

Variable ob: Type.
Variable hom: ob -> ob -> Type.
Variable C: Cat hom.
Variables a b: ob.
Variable f: hom a b.

Lemma idr: f o (id b) == f.
Proof.
apply (id_r).
Qed.

Lemma idl: id a o f == f.
Proof.
apply (id_l).
Qed.

Variables (c d: ob) (g: hom b c) (h: hom c d).
Lemma assoc: (f o g) o h == f o (g o h).
Proof.
apply (Assoc).
Qed.

Lemma hom_refl : f == f.
Proof.
apply (Equivalence_Reflexive).
Qed.

Variables f' f'': hom a b.

Lemma hom_sym : f == f' -> f' == f.
Proof.
apply (Equivalence_Symmetric).
Qed.

Lemma hom_trans :
           f == f' -> f' == f'' -> f == f''.
Proof.
apply (Equivalence_Transitive).
Qed.

End cat_lemmata.

Section Equal_hom.
Variable ob:Type.
Variable hom : ob -> ob -> Type.
Variable C: Cat hom.

Inductive Equal_hom (a b: ob) (f : hom a b) :
forall c d : ob, (hom c d) -> Prop :=
    Build_Equal_hom : forall g : hom a b, f == g -> Equal_hom f g.

Notation "f === g" := (Equal_hom f g) (at level 55).

Lemma Equal_hom_refl (a b: ob) (f: hom a b) :
            f === f.
Proof. intros a b f.
apply Build_Equal_hom.
apply hom_refl.
Qed.

Lemma Equal_hom_sym (a b c d: ob) (f: hom a b) (g: hom c d):
             f === g -> g === f.
Proof. intros a b c d f g H.
elim H. intros g0 H'.
apply Build_Equal_hom.
apply hom_sym.
auto.
Qed.

Lemma Equal_hom_trans (a b c d e e': ob)
                    (f: hom a b)
                    (g: hom c d)
                    (h: hom e e'):
       f === g -> g === h -> f === h.
Proof. intros a b c d e e' f g h H.
elim H. intros g0 Hg0 Hx.
elim Hx. intros g1 Hg1.
apply Build_Equal_hom.
apply hom_trans with g0; auto.
Qed.

End Equal_hom.

Implicit Arguments Equal_hom [ob hom C a b c d].

Notation "f === g" := (Equal_hom f g) (at level 55).

Section transport.

Require Import ProofIrrelevance.

Variable ob: Type.
Variable hom: ob -> ob -> Type.
Variable C: Cat hom.

Definition hom_transport (a b: ob)(f: hom a b) (a' b': ob)
          (H: a' = a) (H': b' = b) : hom a' b'.
intros a b f a' b' H H'. rewrite H; rewrite H'. exact f. Defined.

Lemma hom_transport_pi (a b: ob) (f: hom a b) (a' b': ob)
           (H1 H2 : a' = a) (Hb Hb2: b' = b):
      hom_transport f H1 Hb = hom_transport f H2 Hb2.
Proof. intros.
rewrite (proof_irrelevance (a' = a) H1 H2).
rewrite (proof_irrelevance (b' = b) Hb Hb2).
auto. Qed.

Lemma hom_transport_id (a b: ob) (f: hom a b)
              (Ha: a = a) (Hb: b = b):
         hom_transport f Ha Hb = f.
Proof. intros.
rewrite (proof_irrelevance (a = a) Ha (refl_equal)).
rewrite (proof_irrelevance (b = b) Hb (refl_equal)).
auto. Qed.

Lemma Equal_hom_imp_setoideq (a b: ob)(f: hom a b)
        (a' b': ob) (g: hom a' b')(H: f === g)(Ha: a' = a) (Hb: b' = b) :
          hom_transport f Ha Hb == g .
Proof.
destruct 1.
intros Ha Hb.
rewrite hom_transport_id.
auto.
Qed.

Lemma Equal_hom_imp_setoideq2 (a b: ob) (f g: hom a b):
           f === g -> f == g.
Proof. intros a b f g H.
rewrite <- (@hom_transport_id a b f (refl_equal) (refl_equal)).
apply Equal_hom_imp_setoideq.
auto.
Qed.

Section Equal_hom_lemmata.
Variables a b c d: ob.
Variable f: hom a b.
Variable g: hom c d.

Hypothesis H: f === g.

Lemma Equal_hom_src: a = c.
elim H.
auto.
Qed.

Lemma Equal_hom_tgt: b = d.
elim H. auto. Qed.

End Equal_hom_lemmata.

End transport.