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


(*****************************************************************************)
(*          Projet Formel - Calculus of Inductive Constructions V5.10        *)
(*****************************************************************************)
(*									     *)
(*	                      Comma Category (x|G)            		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

Require Export Functor.

Set Implicit Arguments.
Unset Strict Implicit.

(* (x|G) *)

Section comma_def.

Variables (A X : Category) (G : Functor A X) (x : X).

Structure Com_ob : Type :=  {Ob_com_ob : A; Mor_com_ob : x --> G Ob_com_ob}.

 Section com_arrow_def.

 Variable axf bxg : Com_ob.
 
 Definition Com_law (h : Ob_com_ob axf --> Ob_com_ob bxg) :=
   Mor_com_ob bxg =_S Mor_com_ob axf o FMor G h.

 Structure > Com_arrow : Type := 
   {Mor_com_arrow : Ob_com_ob axf --> Ob_com_ob bxg;
    Prf_com_law :> Com_law Mor_com_arrow}.

 (*** rewrite rules ***)

 (* *)

 Definition Equal_com_arrow (h h' : Com_arrow) :=
   Mor_com_arrow h =_S Mor_com_arrow h'.

 Lemma Equal_com_arrow_equiv : Equivalence Equal_com_arrow.
 Proof.
(* Goal: @Equivalence Com_arrow Equal_com_arrow *)
 apply Build_Equivalence; unfold Equal_com_arrow in |- *.
(* Goal: @Reflexive Com_arrow (fun h h' : Com_arrow => @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow h) (Mor_com_arrow h')) *)
(* Goal: @Partial_equivalence Com_arrow (fun h h' : Com_arrow => @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow h) (Mor_com_arrow h')) *)
 unfold Reflexive in |- *; intro f.
(* Goal: @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow f) (Mor_com_arrow f) *)
(* Goal: @Partial_equivalence Com_arrow (fun h h' : Com_arrow => @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow h) (Mor_com_arrow h')) *)
 apply Refl.
(* Goal: @Partial_equivalence Com_arrow (fun h h' : Com_arrow => @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow h) (Mor_com_arrow h')) *)
 apply Build_Partial_equivalence.
(* Goal: @Transitive Com_arrow (fun h h' : Com_arrow => @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow h) (Mor_com_arrow h')) *)
(* Goal: @Symmetric Com_arrow (fun h h' : Com_arrow => @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow h) (Mor_com_arrow h')) *)
 unfold Transitive in |- *; intros f g h H1 H2.
(* Goal: @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow f) (Mor_com_arrow h) *)
(* Goal: @Symmetric Com_arrow (fun h h' : Com_arrow => @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow h) (Mor_com_arrow h')) *)
 (* *) apply Trans with (Mor_com_arrow g); assumption. 
(* Goal: @Symmetric Com_arrow (fun h h' : Com_arrow => @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow h) (Mor_com_arrow h')) *)
 unfold Symmetric in |- *; intros f g H.
(* Goal: @Equal (@Hom A (Ob_com_ob axf) (Ob_com_ob bxg)) (Mor_com_arrow g) (Mor_com_arrow f) *)
 apply Sym; assumption.
 Qed.

 Canonical Structure Com_arrow_setoid : Setoid := Equal_com_arrow_equiv.

 End com_arrow_def. 

(* composition of two arrows in comma *)

 Section comp_com_def.

 Variables (axf bxg cxh : Com_ob) (f : Com_arrow axf bxg)
   (g : Com_arrow bxg cxh).

 Definition Comp_com_mor := Mor_com_arrow f o Mor_com_arrow g.

 Lemma Comp_com_law : Com_law Comp_com_mor.
 Proof.
(* Goal: @Com_law axf cxh Comp_com_mor *)
 unfold Com_law, Comp_com_mor in |- *.
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob cxh))) (Mor_com_ob cxh) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob cxh) (@Comp A (Ob_com_ob axf) (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow axf bxg f) (@Mor_com_arrow bxg cxh g)))) *)
 (* *) apply Trans with (Mor_com_ob bxg o FMor G (Mor_com_arrow g)).
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob cxh))) (Mor_com_ob cxh) (@Comp X x (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob bxg) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g))) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob cxh))) (@Comp X x (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob bxg) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob cxh) (@Comp A (Ob_com_ob axf) (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow axf bxg f) (@Mor_com_arrow bxg cxh g)))) *)
 apply (Prf_com_law g).
 (* *) apply
        Trans
         with
           (Mor_com_ob axf
            o FMor G (Mor_com_arrow f) o FMor G (Mor_com_arrow g)).
 (* *) apply
        Trans
         with
           ((Mor_com_ob axf o FMor G (Mor_com_arrow f))
            o FMor G (Mor_com_arrow g)).
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob cxh))) (@Comp X x (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob bxg) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g))) (@Comp X x (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob bxg)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob bxg) (@Mor_com_arrow axf bxg f))) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g))) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob cxh))) (@Comp X x (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob bxg)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob bxg) (@Mor_com_arrow axf bxg f))) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@Comp X (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob bxg) (@Mor_com_arrow axf bxg f)) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g)))) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob cxh))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@Comp X (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob bxg) (@Mor_com_arrow axf bxg f)) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g)))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob cxh) (@Comp A (Ob_com_ob axf) (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow axf bxg f) (@Mor_com_arrow bxg cxh g)))) *)
 apply Comp_r; apply (Prf_com_law f).
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob cxh))) (@Comp X x (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob bxg)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob bxg) (@Mor_com_arrow axf bxg f))) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@Comp X (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob bxg) (@Mor_com_arrow axf bxg f)) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g)))) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob cxh))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@Comp X (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob bxg) (@Mor_com_arrow axf bxg f)) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g)))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob cxh) (@Comp A (Ob_com_ob axf) (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow axf bxg f) (@Mor_com_arrow bxg cxh g)))) *)
 apply Ass1.
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob cxh))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@Comp X (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob bxg)) (@FOb A X G (Ob_com_ob cxh)) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob bxg) (@Mor_com_arrow axf bxg f)) (@FMor A X G (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow bxg cxh g)))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob cxh)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob cxh) (@Comp A (Ob_com_ob axf) (Ob_com_ob bxg) (Ob_com_ob cxh) (@Mor_com_arrow axf bxg f) (@Mor_com_arrow bxg cxh g)))) *)
 apply Comp_l; apply FComp1.
 Qed.

 Canonical Structure Comp_com_arrow := Build_Com_arrow Comp_com_law.

 End comp_com_def.
 
(* composition operator *)

Lemma Comp_com_congl : Congl_law Comp_com_arrow.
Proof.
(* Goal: @Congl_law Com_ob Com_arrow_setoid Comp_com_arrow *)
unfold Congl_law in |- *; simpl in |- *.
(* Goal: forall (a b c : Com_ob) (f g : Com_arrow a b) (h : Com_arrow b c) (_ : @Equal_com_arrow a b f g), @Equal_com_arrow a c (@Comp_com_arrow a b c f h) (@Comp_com_arrow a b c g h) *)
intros a b c f1; elim f1; intros h e f2.
(* Goal: forall (h0 : Com_arrow b c) (_ : @Equal_com_arrow a b (@Build_Com_arrow a b h e) f2), @Equal_com_arrow a c (@Comp_com_arrow a b c (@Build_Com_arrow a b h e) h0) (@Comp_com_arrow a b c f2 h0) *)
elim f2; intros h' e' f3; elim f3; intros h'' e''.
(* Goal: forall _ : @Equal_com_arrow a b (@Build_Com_arrow a b h e) (@Build_Com_arrow a b h' e'), @Equal_com_arrow a c (@Comp_com_arrow a b c (@Build_Com_arrow a b h e) (@Build_Com_arrow b c h'' e'')) (@Comp_com_arrow a b c (@Build_Com_arrow a b h' e') (@Build_Com_arrow b c h'' e'')) *)
unfold Equal_com_arrow in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (Ob_com_ob b) (Ob_com_ob a)) h (@Comp_com_mor b a a (@Build_Com_arrow b a h e) (Id_Comma a)) *)
unfold Comp_com_mor in |- *; simpl in |- *.
(* Goal: forall _ : @Equal (@Hom A (Ob_com_ob b) (Ob_com_ob c)) h h', @Equal (@Hom A (Ob_com_ob a) (Ob_com_ob c)) (@Comp A (Ob_com_ob a) (Ob_com_ob b) (Ob_com_ob c) h'' h) (@Comp A (Ob_com_ob a) (Ob_com_ob b) (Ob_com_ob c) h'' h') *)
intro H; apply Comp_l; trivial.
Qed.

Lemma Comp_com_congr : Congr_law Comp_com_arrow.
Proof.
(* Goal: @Congr_law Com_ob Com_arrow_setoid Comp_com_arrow *)
unfold Congr_law in |- *; simpl in |- *.
(* Goal: forall (a b c : Com_ob) (f g : Com_arrow a b) (h : Com_arrow b c) (_ : @Equal_com_arrow a b f g), @Equal_com_arrow a c (@Comp_com_arrow a b c f h) (@Comp_com_arrow a b c g h) *)
intros a b c f1; elim f1; intros h e f2.
(* Goal: forall (h0 : Com_arrow b c) (_ : @Equal_com_arrow a b (@Build_Com_arrow a b h e) f2), @Equal_com_arrow a c (@Comp_com_arrow a b c (@Build_Com_arrow a b h e) h0) (@Comp_com_arrow a b c f2 h0) *)
elim f2; intros h' e' f3; elim f3; intros h'' e''.
(* Goal: forall _ : @Equal_com_arrow a b (@Build_Com_arrow a b h e) (@Build_Com_arrow a b h' e'), @Equal_com_arrow a c (@Comp_com_arrow a b c (@Build_Com_arrow a b h e) (@Build_Com_arrow b c h'' e'')) (@Comp_com_arrow a b c (@Build_Com_arrow a b h' e') (@Build_Com_arrow b c h'' e'')) *)
unfold Equal_com_arrow in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (Ob_com_ob b) (Ob_com_ob a)) h (@Comp_com_mor b a a (@Build_Com_arrow b a h e) (Id_Comma a)) *)
unfold Comp_com_mor in |- *; simpl in |- *.
(* Goal: forall _ : @Equal (@Hom A (Ob_com_ob a) (Ob_com_ob b)) h h', @Equal (@Hom A (Ob_com_ob a) (Ob_com_ob c)) (@Comp A (Ob_com_ob a) (Ob_com_ob b) (Ob_com_ob c) h h'') (@Comp A (Ob_com_ob a) (Ob_com_ob b) (Ob_com_ob c) h' h'') *)
intro H; apply Comp_r; trivial.
Qed.

Definition Comp_Comma := Build_Comp Comp_com_congl Comp_com_congr. 

Lemma Assoc_Comma : Assoc_law Comp_Comma.
Proof.
(* Goal: @Assoc_law Com_ob Com_arrow_setoid Comp_Comma *)
unfold Assoc_law in |- *; intros a b c d f1; elim f1.
(* Goal: forall (Mor_com_arrow : Carrier (@Hom A (Ob_com_ob a) (Ob_com_ob b))) (Prf_com_law : @Com_law a b Mor_com_arrow) (g : Carrier (Com_arrow_setoid b c)) (h : Carrier (Com_arrow_setoid c d)), @Equal (Com_arrow_setoid a d) (@Cat_comp Com_ob Com_arrow_setoid Comp_Comma a b d (@Build_Com_arrow a b Mor_com_arrow Prf_com_law) (@Cat_comp Com_ob Com_arrow_setoid Comp_Comma b c d g h)) (@Cat_comp Com_ob Com_arrow_setoid Comp_Comma a c d (@Cat_comp Com_ob Com_arrow_setoid Comp_Comma a b c (@Build_Com_arrow a b Mor_com_arrow Prf_com_law) g) h) *)
intros h1 e1 f2; elim f2; intros h2 e2 f3.
(* Goal: @Equal (Com_arrow_setoid a d) (@Cat_comp Com_ob Com_arrow_setoid Comp_Comma a b d (@Build_Com_arrow a b h1 e1) (@Cat_comp Com_ob Com_arrow_setoid Comp_Comma b c d (@Build_Com_arrow b c h2 e2) f3)) (@Cat_comp Com_ob Com_arrow_setoid Comp_Comma a c d (@Cat_comp Com_ob Com_arrow_setoid Comp_Comma a b c (@Build_Com_arrow a b h1 e1) (@Build_Com_arrow b c h2 e2)) f3) *)
elim f3; intros h3 e3.
(* Goal: forall _ : @Equal_com_arrow a b (@Build_Com_arrow a b h e) (@Build_Com_arrow a b h' e'), @Equal_com_arrow a c (@Comp_com_arrow a b c (@Build_Com_arrow a b h e) (@Build_Com_arrow b c h'' e'')) (@Comp_com_arrow a b c (@Build_Com_arrow a b h' e') (@Build_Com_arrow b c h'' e'')) *)
simpl in |- *; unfold Equal_com_arrow in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (Ob_com_ob b) (Ob_com_ob a)) h (@Comp_com_mor b a a (@Build_Com_arrow b a h e) (Id_Comma a)) *)
unfold Comp_com_mor in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (Ob_com_ob b) (Ob_com_ob a)) h (@Comp_com_mor b a a (@Build_Com_arrow b a h e) (Id_Comma a)) *)
unfold Comp_com_mor in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (Ob_com_ob a) (Ob_com_ob d)) (@Comp A (Ob_com_ob a) (Ob_com_ob b) (Ob_com_ob d) h1 (@Comp A (Ob_com_ob b) (Ob_com_ob c) (Ob_com_ob d) h2 h3)) (@Comp A (Ob_com_ob a) (Ob_com_ob c) (Ob_com_ob d) (@Comp A (Ob_com_ob a) (Ob_com_ob b) (Ob_com_ob c) h1 h2) h3) *)
apply Ass.
Qed.

(* Id *)

Lemma Id_com_law : forall axf : Com_ob, Com_law (Id (Ob_com_ob axf)).
Proof.
(* Goal: forall axf : Com_ob, @Com_law axf axf (@Id A (Ob_com_ob axf)) *)
intro axf; unfold Com_law in |- *.
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob axf))) (Mor_com_ob axf) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob axf)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob axf) (@Id A (Ob_com_ob axf)))) *)
(* *) apply Trans with (Mor_com_ob axf o Id (G (Ob_com_ob axf))).
(* Goal: @Equal (@Hom A (Ob_com_ob b) (Ob_com_ob a)) h (@Comp A (Ob_com_ob b) (Ob_com_ob a) (Ob_com_ob a) h (@Id A (Ob_com_ob a))) *)
apply Idr.
(* Goal: @Equal (@Hom X x (@FOb A X G (Ob_com_ob axf))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob axf)) (Mor_com_ob axf) (@Id X (@FOb A X G (Ob_com_ob axf)))) (@Comp X x (@FOb A X G (Ob_com_ob axf)) (@FOb A X G (Ob_com_ob axf)) (Mor_com_ob axf) (@FMor A X G (Ob_com_ob axf) (Ob_com_ob axf) (@Id A (Ob_com_ob axf)))) *)
apply Comp_l; apply FId1.
Qed.

Canonical Structure Id_Comma (axf : Com_ob) :=
  Build_Com_arrow (Id_com_law axf).

Lemma Idl_Comma : Idl_law Comp_Comma Id_Comma.
Proof.
(* Goal: @Idl_law Com_ob Com_arrow_setoid Comp_Comma Id_Comma *)
unfold Idl_law in |- *; intros a b f1; elim f1; intros h e.
(* Goal: forall _ : @Equal_com_arrow a b (@Build_Com_arrow a b h e) (@Build_Com_arrow a b h' e'), @Equal_com_arrow a c (@Comp_com_arrow a b c (@Build_Com_arrow a b h e) (@Build_Com_arrow b c h'' e'')) (@Comp_com_arrow a b c (@Build_Com_arrow a b h' e') (@Build_Com_arrow b c h'' e'')) *)
simpl in |- *; unfold Equal_com_arrow in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (Ob_com_ob b) (Ob_com_ob a)) h (@Comp_com_mor b a a (@Build_Com_arrow b a h e) (Id_Comma a)) *)
unfold Comp_com_mor in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (Ob_com_ob a) (Ob_com_ob b)) (@Comp A (Ob_com_ob a) (Ob_com_ob a) (Ob_com_ob b) (@Id A (Ob_com_ob a)) h) h *)
apply Idl.
Qed.

Lemma Idr_Comma : Idr_law Comp_Comma Id_Comma.
Proof.
(* Goal: @Idr_law Com_ob Com_arrow_setoid Comp_Comma Id_Comma *)
unfold Idr_law in |- *; intros a b f1; elim f1; intros h e.
(* Goal: forall _ : @Equal_com_arrow a b (@Build_Com_arrow a b h e) (@Build_Com_arrow a b h' e'), @Equal_com_arrow a c (@Comp_com_arrow a b c (@Build_Com_arrow a b h e) (@Build_Com_arrow b c h'' e'')) (@Comp_com_arrow a b c (@Build_Com_arrow a b h' e') (@Build_Com_arrow b c h'' e'')) *)
simpl in |- *; unfold Equal_com_arrow in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (Ob_com_ob b) (Ob_com_ob a)) h (@Comp_com_mor b a a (@Build_Com_arrow b a h e) (Id_Comma a)) *)
unfold Comp_com_mor in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (Ob_com_ob b) (Ob_com_ob a)) h (@Comp A (Ob_com_ob b) (Ob_com_ob a) (Ob_com_ob a) h (@Id A (Ob_com_ob a))) *)
apply Idr.
Qed.

Canonical Structure Comma := Build_Category Assoc_Comma Idl_Comma Idr_Comma.

End comma_def.