(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Cartesian.
(** Title "Categories." *)
Comments "Some basic category theory.".
Section Category_def.
Section Category_def1.
Variable Ob : Type.
Variable Hom : Ob -> Ob -> Setoid.
Variable
  Hom_comp : forall a b c : Ob, MAP (cart (Hom b c) (Hom a b)) (Hom a c).
Variable Hom_id : forall a : Ob, Hom a a.

Definition Hom_comp_assoc :=
  forall (a b c d : Ob) (f : Hom a b) (g : Hom b c) (h : Hom c d),
  Equal (Hom_comp a b d (couple (Hom_comp b c d (couple h g)) f))
    (Hom_comp a c d (couple h (Hom_comp a b c (couple g f)))).

Definition Hom_comp_unit_l :=
  forall (a b : Ob) (f : Hom a b),
  Equal (Hom_comp a b b (couple (Hom_id b) f)) f.

Definition Hom_comp_unit_r :=
  forall (a b : Ob) (f : Hom a b),
  Equal (Hom_comp a a b (couple f (Hom_id a))) f.
End Category_def1.

Record category : Type := 
  {Ob :> Type;
   Hom : Ob -> Ob -> Setoid;
   Hom_comp : forall a b c : Ob, MAP (cart (Hom b c) (Hom a b)) (Hom a c);
   Hom_id : forall a : Ob, Hom a a;
   Hom_comp_assoc_prf : Hom_comp_assoc Hom_comp;
   Hom_comp_unit_l_prf : Hom_comp_unit_l Hom_comp Hom_id;
   Hom_comp_unit_r_prf : Hom_comp_unit_r Hom_comp Hom_id}.
Section Category_comp.
Variable C : category.

Definition comp_hom (a b c : C) (g : Hom b c) (f : Hom a b) :=
  Hom_comp a b c (couple g f).

Lemma comp_hom_compatible :
 forall (a b c : C) (x x' : Hom b c) (y y' : Hom a b),
 Equal x x' -> Equal y y' -> Equal (comp_hom x y) (comp_hom x' y').
(* Goal: forall (a b c : Ob C) (x x' : Carrier (@Hom C b c)) (y y' : Carrier (@Hom C a b)) (_ : @Equal (@Hom C b c) x x') (_ : @Equal (@Hom C a b) y y'), @Equal (@Hom C a c) (@comp_hom a b c x y) (@comp_hom a b c x' y') *)
intros a b c x x' y y' H' H'0; try assumption.
(* Goal: @Equal (@Hom C a c) (@comp_hom a b c x y) (@comp_hom a b c x' y') *)
unfold comp_hom in |- *; auto with algebra.
Qed.

Lemma comp_hom_assoc :
 forall (a b c d : C) (f : Hom a b) (g : Hom b c) (h : Hom c d),
 Equal (comp_hom (comp_hom h g) f) (comp_hom h (comp_hom g f)).
(* Goal: forall (a b c d : Ob C) (f : Carrier (@Hom C a b)) (g : Carrier (@Hom C b c)) (h : Carrier (@Hom C c d)), @Equal (@Hom C a d) (@comp_hom a b d (@comp_hom b c d h g) f) (@comp_hom a c d h (@comp_hom a b c g f)) *)
exact (Hom_comp_assoc_prf (c:=C)).
Qed.

Lemma comp_hom_unit_l :
 forall (a b : C) (f : Hom a b), Equal (comp_hom (Hom_id b) f) f.
(* Goal: forall (a b : Ob C) (f : Carrier (@Hom C a b)), @Equal (@Hom C a b) (@comp_hom a b b (@Hom_id C b) f) f *)
exact (Hom_comp_unit_l_prf (c:=C)).
Qed.

Lemma comp_hom_unit_r :
 forall (a b : C) (f : Hom a b), Equal (comp_hom f (Hom_id a)) f.
(* Goal: forall (a b : Ob C) (f : Carrier (@Hom C a b)), @Equal (@Hom C a b) (@comp_hom a a b f (@Hom_id C a)) f *)
exact (Hom_comp_unit_r_prf (c:=C)).
Qed.
End Category_comp.
Hint Resolve comp_hom_compatible comp_hom_assoc comp_hom_unit_l
  comp_hom_unit_r: algebra.
Section Full_subcat_def.
Variable C : category.
Variable C' : Type.
Variable i : C' -> C.

Definition fsubcat_Hom (a b : C') := Hom (i a) (i b).

Definition fsubcat_Hom_comp :
  forall a b c : C',
  MAP (cart (fsubcat_Hom b c) (fsubcat_Hom a b)) (fsubcat_Hom a c).
(* Goal: forall a b c : C', Carrier (MAP (cart (fsubcat_Hom b c) (fsubcat_Hom a b)) (fsubcat_Hom a c)) *)
intros a b c; try assumption.
(* Goal: Carrier (MAP (cart (fsubcat_Hom b c) (fsubcat_Hom a b)) (fsubcat_Hom a c)) *)
exact (Hom_comp (i a) (i b) (i c)).
Defined.

Definition fsubcat_Hom_id (a : C') := Hom_id (i a).

Definition full_subcat : category.
apply
 (Build_category (Ob:=C') (Hom:=fsubcat_Hom) (Hom_comp:=fsubcat_Hom_comp)
    (Hom_id:=fsubcat_Hom_id)).
(* Goal: @Hom_comp_unit_r C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
red in |- *.
(* Goal: forall (a b c d : C') (f : Carrier (fsubcat_Hom a b)) (g : Carrier (fsubcat_Hom b c)) (h : Carrier (fsubcat_Hom c d)), @Equal (fsubcat_Hom a d) (@Ap (cart (fsubcat_Hom b d) (fsubcat_Hom a b)) (fsubcat_Hom a d) (fsubcat_Hom_comp a b d) (@couple (fsubcat_Hom b d) (fsubcat_Hom a b) (@Ap (cart (fsubcat_Hom c d) (fsubcat_Hom b c)) (fsubcat_Hom b d) (fsubcat_Hom_comp b c d) (@couple (fsubcat_Hom c d) (fsubcat_Hom b c) h g)) f)) (@Ap (cart (fsubcat_Hom c d) (fsubcat_Hom a c)) (fsubcat_Hom a d) (fsubcat_Hom_comp a c d) (@couple (fsubcat_Hom c d) (fsubcat_Hom a c) h (@Ap (cart (fsubcat_Hom b c) (fsubcat_Hom a b)) (fsubcat_Hom a c) (fsubcat_Hom_comp a b c) (@couple (fsubcat_Hom b c) (fsubcat_Hom a b) g f)))) *)
(* Goal: @Hom_comp_unit_l C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
(* Goal: @Hom_comp_unit_r C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
unfold fsubcat_Hom, fsubcat_Hom_comp in |- *; simpl in |- *.
(* Goal: forall (a b c d : C') (f : Carrier (@Hom C (i a) (i b))) (g : Carrier (@Hom C (i b) (i c))) (h : Carrier (@Hom C (i c) (i d))), @Equal (@Hom C (i a) (i d)) (@Ap (cart (@Hom C (i b) (i d)) (@Hom C (i a) (i b))) (@Hom C (i a) (i d)) (@Hom_comp C (i a) (i b) (i d)) (@couple (@Hom C (i b) (i d)) (@Hom C (i a) (i b)) (@Ap (cart (@Hom C (i c) (i d)) (@Hom C (i b) (i c))) (@Hom C (i b) (i d)) (@Hom_comp C (i b) (i c) (i d)) (@couple (@Hom C (i c) (i d)) (@Hom C (i b) (i c)) h g)) f)) (@Ap (cart (@Hom C (i c) (i d)) (@Hom C (i a) (i c))) (@Hom C (i a) (i d)) (@Hom_comp C (i a) (i c) (i d)) (@couple (@Hom C (i c) (i d)) (@Hom C (i a) (i c)) h (@Ap (cart (@Hom C (i b) (i c)) (@Hom C (i a) (i b))) (@Hom C (i a) (i c)) (@Hom_comp C (i a) (i b) (i c)) (@couple (@Hom C (i b) (i c)) (@Hom C (i a) (i b)) g f)))) *)
(* Goal: @Hom_comp_unit_l C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
(* Goal: @Hom_comp_unit_r C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
intros a b c d f g h; try assumption.
(* Goal: @Equal (@Hom C (i a) (i d)) (@Ap (cart (@Hom C (i b) (i d)) (@Hom C (i a) (i b))) (@Hom C (i a) (i d)) (@Hom_comp C (i a) (i b) (i d)) (@couple (@Hom C (i b) (i d)) (@Hom C (i a) (i b)) (@Ap (cart (@Hom C (i c) (i d)) (@Hom C (i b) (i c))) (@Hom C (i b) (i d)) (@Hom_comp C (i b) (i c) (i d)) (@couple (@Hom C (i c) (i d)) (@Hom C (i b) (i c)) h g)) f)) (@Ap (cart (@Hom C (i c) (i d)) (@Hom C (i a) (i c))) (@Hom C (i a) (i d)) (@Hom_comp C (i a) (i c) (i d)) (@couple (@Hom C (i c) (i d)) (@Hom C (i a) (i c)) h (@Ap (cart (@Hom C (i b) (i c)) (@Hom C (i a) (i b))) (@Hom C (i a) (i c)) (@Hom_comp C (i a) (i b) (i c)) (@couple (@Hom C (i b) (i c)) (@Hom C (i a) (i b)) g f)))) *)
(* Goal: @Hom_comp_unit_l C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
(* Goal: @Hom_comp_unit_r C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
apply (Hom_comp_assoc_prf (c:=C)).
(* Goal: @Hom_comp_unit_r C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
red in |- *.
(* Goal: forall (a b : C') (f : Carrier (fsubcat_Hom a b)), @Equal (fsubcat_Hom a b) (@Ap (cart (fsubcat_Hom a b) (fsubcat_Hom a a)) (fsubcat_Hom a b) (fsubcat_Hom_comp a a b) (@couple (fsubcat_Hom a b) (fsubcat_Hom a a) f (fsubcat_Hom_id a))) f *)
unfold fsubcat_Hom, fsubcat_Hom_comp, fsubcat_Hom_id in |- *; simpl in |- *.
(* Goal: forall (a b : C') (f : Carrier (@Hom C (i a) (i b))), @Equal (@Hom C (i a) (i b)) (@Ap (cart (@Hom C (i a) (i b)) (@Hom C (i a) (i a))) (@Hom C (i a) (i b)) (@Hom_comp C (i a) (i a) (i b)) (@couple (@Hom C (i a) (i b)) (@Hom C (i a) (i a)) f (@Hom_id C (i a)))) f *)
intros a b f; try assumption.
(* Goal: @Equal (@Hom C (i a) (i b)) (@Ap (cart (@Hom C (i b) (i b)) (@Hom C (i a) (i b))) (@Hom C (i a) (i b)) (@Hom_comp C (i a) (i b) (i b)) (@couple (@Hom C (i b) (i b)) (@Hom C (i a) (i b)) (@Hom_id C (i b)) f)) f *)
(* Goal: @Hom_comp_unit_r C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
apply (Hom_comp_unit_l_prf (c:=C)).
(* Goal: @Hom_comp_unit_r C' fsubcat_Hom fsubcat_Hom_comp fsubcat_Hom_id *)
red in |- *.
(* Goal: forall (a b : C') (f : Carrier (fsubcat_Hom a b)), @Equal (fsubcat_Hom a b) (@Ap (cart (fsubcat_Hom a b) (fsubcat_Hom a a)) (fsubcat_Hom a b) (fsubcat_Hom_comp a a b) (@couple (fsubcat_Hom a b) (fsubcat_Hom a a) f (fsubcat_Hom_id a))) f *)
unfold fsubcat_Hom, fsubcat_Hom_comp, fsubcat_Hom_id in |- *; simpl in |- *.
(* Goal: forall (a b : C') (f : Carrier (@Hom C (i a) (i b))), @Equal (@Hom C (i a) (i b)) (@Ap (cart (@Hom C (i a) (i b)) (@Hom C (i a) (i a))) (@Hom C (i a) (i b)) (@Hom_comp C (i a) (i a) (i b)) (@couple (@Hom C (i a) (i b)) (@Hom C (i a) (i a)) f (@Hom_id C (i a)))) f *)
intros a b f; try assumption.
(* Goal: @Equal (@Hom C (i a) (i b)) (@Ap (cart (@Hom C (i a) (i b)) (@Hom C (i a) (i a))) (@Hom C (i a) (i b)) (@Hom_comp C (i a) (i a) (i b)) (@couple (@Hom C (i a) (i b)) (@Hom C (i a) (i a)) f (@Hom_id C (i a)))) f *)
apply (Hom_comp_unit_r_prf (c:=C)).
Defined.
End Full_subcat_def.
End Category_def.
Hint Resolve comp_hom_compatible comp_hom_assoc comp_hom_unit_l
  comp_hom_unit_r: algebra.