(* 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        *)
(*****************************************************************************)
(*									     *)
(*	       Category Parallel Arrowd (used in Equalizers)		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)


Require Export BasicTypes.
Require Export Category.

Set Implicit Arguments.
Unset Strict Implicit.

Section pa_def.

Variables (C : Category) (a b : C) (I : Type) (k : I -> (a --> b)).

Inductive PA_ob : Type :=
  | PA1 : PA_ob
  | PA2 : PA_ob.

Inductive PA_mor : PA_ob -> PA_ob -> Type :=
  | PA_I1 : PA_mor PA1 PA1
  | PA_I2 : PA_mor PA2 PA2
  | PA_f : I -> PA_mor PA1 PA2.

(* sche'mas d'e'limination pour PA_mor *)

Lemma PA_11_P :
 (PA_mor PA1 PA1 -> Prop) -> forall x y : PA_ob, PA_mor x y -> Prop.
Proof.
(* Goal: forall (_ : forall _ : PA_mor PA2 PA1, Type) (x y : PA_ob) (_ : PA_mor x y), Type *)
intros P x y; elim x; elim y.
(* Goal: forall _ : PA_mor PA2 PA1, Type *)
(* Goal: forall _ : PA_mor PA2 PA2, Type *)
exact P.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
Defined.

Lemma PA_11_ind :
 forall P : PA_mor PA1 PA1 -> Prop, P PA_I1 -> forall x : PA_mor PA1 PA1, P x.
Proof.
(* Goal: forall (P : forall _ : PA_mor PA1 PA1, Prop) (_ : P PA_I1) (x : PA_mor PA1 PA1), P x *)
intros P PP1 x.
(* Goal: P x *)
change (PA_11_P P x) in |- *.
apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_11_P P f));
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 PA2 o4 (PA_f i) h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
 simpl in |- *.
(* Goal: P PA_I1 *)
(* Goal: True *)
(* Goal: forall _ : I, True *)
exact PP1.
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
trivial.
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
trivial.
Qed.

Lemma PA_22_P :
 (PA_mor PA2 PA2 -> Prop) -> forall x y : PA_ob, PA_mor x y -> Prop.
Proof.
(* Goal: forall (_ : forall _ : PA_mor PA2 PA1, Type) (x y : PA_ob) (_ : PA_mor x y), Type *)
intros P x y; elim x; elim y.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
(* Goal: forall _ : PA_mor PA2 PA1, Type *)
(* Goal: forall _ : PA_mor PA2 PA2, Type *)
exact P.
Defined.

Lemma PA_22_ind :
 forall P : PA_mor PA2 PA2 -> Prop, P PA_I2 -> forall x : PA_mor PA2 PA2, P x.
Proof.
(* Goal: forall (P : forall _ : PA_mor PA2 PA2, Prop) (_ : P PA_I2) (x : PA_mor PA2 PA2), P x *)
intros P PP2 x.
(* Goal: P x *)
change (PA_22_P P x) in |- *.
apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_22_P P f));
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 PA2 o4 (PA_f i) h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
 simpl in |- *.
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
trivial.
(* Goal: P PA_I2 *)
(* Goal: forall _ : I, True *)
exact PP2.
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
trivial.
Qed.

Lemma PA_12_P :
 (PA_mor PA1 PA2 -> Prop) -> forall x y : PA_ob, PA_mor x y -> Prop.
Proof.
(* Goal: forall (_ : forall _ : PA_mor PA2 PA1, Type) (x y : PA_ob) (_ : PA_mor x y), Type *)
intros P x y; elim x; elim y.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
(* Goal: forall _ : PA_mor PA2 PA1, Type *)
(* Goal: forall _ : PA_mor PA2 PA2, Type *)
exact P.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
Defined.

Lemma PA_12_ind :
 forall P : PA_mor PA1 PA2 -> Prop,
 (forall i : I, P (PA_f i)) -> forall x : PA_mor PA1 PA2, P x.
Proof.
(* Goal: forall (P : forall _ : PA_mor PA1 PA2, Prop) (_ : forall i : I, P (PA_f i)) (x : PA_mor PA1 PA2), P x *)
intros P Pf x.
(* Goal: P x *)
change (PA_12_P P x) in |- *.
apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_12_P P f));
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 PA2 o4 (PA_f i) h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
 simpl in |- *.
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
trivial.
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
trivial.
(* Goal: forall i : I, P (PA_f i) *)
exact Pf.
Qed.

Lemma PA_21_P :
 (PA_mor PA2 PA1 -> Prop) -> forall x y : PA_ob, PA_mor x y -> Prop.
Proof.
(* Goal: forall (_ : forall _ : PA_mor PA2 PA1, Type) (x y : PA_ob) (_ : PA_mor x y), Type *)
intros P x y; elim x; elim y.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
(* Goal: forall _ : PA_mor PA2 PA1, Type *)
(* Goal: forall _ : PA_mor PA2 PA2, Type *)
exact P.
(* Goal: forall _ : PA_mor PA2 PA2, Prop *)
intro x'; exact True.
Defined.

Lemma PA_21_ind :
 forall (P : PA_mor PA2 PA1 -> Prop) (x : PA_mor PA2 PA1), P x.
Proof.
(* Goal: forall (P : forall _ : PA_mor PA2 PA1, Type) (x : PA_mor PA2 PA1), P x *)
intros P x.
(* Goal: P x *)
change (PA_21_P P x) in |- *.
apply (PA_mor_ind (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_21_P P f));
(* Goal: forall (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 PA_I2), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA1 PA2)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
 simpl in |- *; auto.
Qed.

Lemma PA_21_T :
 (PA_mor PA2 PA1 -> Type) -> forall x y : PA_ob, PA_mor x y -> Type.
Proof.
(* Goal: forall (_ : forall _ : PA_mor PA2 PA1, Type) (x y : PA_ob) (_ : PA_mor x y), Type *)
intros P x y; elim x; elim y.
(* Goal: forall _ : PA_mor PA2 PA2, Type *)
intro x'; exact UnitType.
(* Goal: forall _ : PA_mor PA2 PA2, Type *)
intro x'; exact UnitType.
(* Goal: forall _ : PA_mor PA2 PA1, Type *)
(* Goal: forall _ : PA_mor PA2 PA2, Type *)
exact P.
(* Goal: forall _ : PA_mor PA2 PA2, Type *)
intro x'; exact UnitType.
Defined.

Lemma PA_21_rect :
 forall (P : PA_mor PA2 PA1 -> Type) (x : PA_mor PA2 PA1), P x.
Proof.
(* Goal: forall (P : forall _ : PA_mor PA2 PA1, Type) (x : PA_mor PA2 PA1), P x *)
intros P x.
(* Goal: P x *)
change (PA_21_T P x) in |- *.
apply (PA_mor_rect (P:=fun (x y : PA_ob) (f : PA_mor x y) => PA_21_T P f));
(* Goal: forall (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 PA_I2), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA1 PA2)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
 simpl in |- *; auto.
Qed.


(* egalite' *)

Definition Equal_PA_mor (x y : PA_ob) (f g : PA_mor x y) :=
  match f in (PA_mor x' y') return Prop with
  | PA_I1 => 
      (* PA_I1  *)  True
      (* PA_I2  *) 
  | PA_I2 => True
      (* PA_f i *) 
  | PA_f i =>
      match g in (PA_mor x' y') return Prop with
      | PA_I1 => 
          (* PA_I1  *)  False
          (* PA_I2  *) 
      | PA_I2 => False
          (* PA_f j *) 
      | PA_f j => k i =_S k j
      end
  end.

Lemma Equal_PA_mor_Equiv :
 forall x y : PA_ob, Equivalence (Equal_PA_mor (x:=x) (y:=y)).
Proof.
intros x y; apply Build_Equivalence;
 [ red in |- * | apply Build_Partial_equivalence; red in |- * ].
(* Goal: forall x0 : PA_mor x y, @Equal_PA_mor x y x0 x0 *)
(* Goal: forall (x0 y0 z : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0) (_ : @Equal_PA_mor x y y0 z), @Equal_PA_mor x y x0 z *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intro f; elim f.
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
simpl in |- *; trivial.
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
simpl in |- *; trivial.
(* Goal: forall i : I, @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i) *)
(* Goal: forall (x0 y0 z : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0) (_ : @Equal_PA_mor x y y0 z), @Equal_PA_mor x y x0 z *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intro i; simpl in |- *; apply Refl.
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intros f; elim f.
(* Goal: forall (y z : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 y) (_ : @Equal_PA_mor PA2 PA2 y z), @Equal_PA_mor PA2 PA2 PA_I2 z *)
(* Goal: forall (i : I) (y z : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y) (_ : @Equal_PA_mor PA1 PA2 y z), @Equal_PA_mor PA1 PA2 (PA_f i) z *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intros g h e1 e2.
(* Goal: @Equal_PA_mor PA1 PA1 PA_I1 h *)
(* Goal: forall (y z : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 y) (_ : @Equal_PA_mor PA2 PA2 y z), @Equal_PA_mor PA2 PA2 PA_I2 z *)
(* Goal: forall (i : I) (y z : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y) (_ : @Equal_PA_mor PA1 PA2 y z), @Equal_PA_mor PA1 PA2 (PA_f i) z *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
apply (PA_11_ind (P:=fun h : PA_mor PA1 PA1 => Equal_PA_mor PA_I1 h)).
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
simpl in |- *; trivial.
(* Goal: forall (y z : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 y) (_ : @Equal_PA_mor PA2 PA2 y z), @Equal_PA_mor PA2 PA2 PA_I2 z *)
(* Goal: forall (i : I) (y z : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y) (_ : @Equal_PA_mor PA1 PA2 y z), @Equal_PA_mor PA1 PA2 (PA_f i) z *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intros g h e1 e2.
(* Goal: @Equal_PA_mor PA2 PA2 PA_I2 h *)
(* Goal: forall (i : I) (y z : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y) (_ : @Equal_PA_mor PA1 PA2 y z), @Equal_PA_mor PA1 PA2 (PA_f i) z *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
apply (PA_22_ind (P:=fun h : PA_mor PA2 PA2 => Equal_PA_mor PA_I2 h)).
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
simpl in |- *; trivial.
(* Goal: forall (i : I) (y z : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y) (_ : @Equal_PA_mor PA1 PA2 y z), @Equal_PA_mor PA1 PA2 (PA_f i) z *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intros i g h.
lapply
 (PA_12_ind
    (P:=fun x : PA_mor PA1 PA2 =>
        Equal_PA_mor (PA_f i) x ->
        Equal_PA_mor x h -> Equal_PA_mor (PA_f i) h)).
(* Goal: forall (_ : forall (x : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) x) (_ : @Equal_PA_mor PA1 PA2 x h), @Equal_PA_mor PA1 PA2 (PA_f i) h) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) g) (_ : @Equal_PA_mor PA1 PA2 g h), @Equal_PA_mor PA1 PA2 (PA_f i) h *)
(* Goal: forall (i0 : I) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)) (_ : @Equal_PA_mor PA1 PA2 (PA_f i0) h), @Equal_PA_mor PA1 PA2 (PA_f i) h *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intros H H0 H1; apply (H g H0 H1).
(* Goal: forall (i0 : I) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)) (_ : @Equal_PA_mor PA1 PA2 (PA_f i0) h), @Equal_PA_mor PA1 PA2 (PA_f i) h *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intro j; unfold Equal_PA_mor at 1 in |- *; intro eqij.
lapply
 (PA_12_ind
    (P:=fun x : PA_mor PA1 PA2 =>
        Equal_PA_mor (PA_f j) x -> Equal_PA_mor (PA_f i) x)).
(* Goal: forall (_ : forall (x : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f j) x), @Equal_PA_mor PA1 PA2 (PA_f i) x) (_ : @Equal_PA_mor PA1 PA2 (PA_f j) h), @Equal_PA_mor PA1 PA2 (PA_f i) h *)
(* Goal: forall (i0 : I) (_ : @Equal_PA_mor PA1 PA2 (PA_f j) (PA_f i0)), @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0) *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intros H H0; apply (H h H0).
(* Goal: forall (i0 : I) (_ : @Equal_PA_mor PA1 PA2 (PA_f j) (PA_f i0)), @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0) *)
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
simpl in |- *; intros l eqjl.
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
(* *) apply Trans with (k j); trivial.
(* Goal: forall (x0 y0 : PA_mor x y) (_ : @Equal_PA_mor x y x0 y0), @Equal_PA_mor x y y0 x0 *)
intros f; elim f.
(* Goal: forall (y : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 y), @Equal_PA_mor PA2 PA2 y PA_I2 *)
(* Goal: forall (i : I) (y : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y), @Equal_PA_mor PA1 PA2 y (PA_f i) *)
intros g e1.
(* Goal: @Equal_PA_mor PA1 PA1 g PA_I1 *)
(* Goal: forall (y : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 y), @Equal_PA_mor PA2 PA2 y PA_I2 *)
(* Goal: forall (i : I) (y : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y), @Equal_PA_mor PA1 PA2 y (PA_f i) *)
apply (PA_11_ind (P:=fun g : PA_mor PA1 PA1 => Equal_PA_mor g PA_I1)).
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
simpl in |- *; trivial.
(* Goal: forall (y : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 y), @Equal_PA_mor PA2 PA2 y PA_I2 *)
(* Goal: forall (i : I) (y : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y), @Equal_PA_mor PA1 PA2 y (PA_f i) *)
intros g e1.
(* Goal: @Equal_PA_mor PA2 PA2 g PA_I2 *)
(* Goal: forall (i : I) (y : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y), @Equal_PA_mor PA1 PA2 y (PA_f i) *)
apply (PA_22_ind (P:=fun g : PA_mor PA2 PA2 => Equal_PA_mor g PA_I2)).
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
simpl in |- *; trivial.
(* Goal: forall (i : I) (y : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) y), @Equal_PA_mor PA1 PA2 y (PA_f i) *)
intros i g.
lapply
 (PA_12_ind
    (P:=fun g : PA_mor PA1 PA2 =>
        Equal_PA_mor (PA_f i) g -> Equal_PA_mor g (PA_f i))).
(* Goal: forall (_ : forall (x : PA_mor PA1 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) x), @Equal_PA_mor PA1 PA2 x (PA_f i)) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) g), @Equal_PA_mor PA1 PA2 g (PA_f i) *)
(* Goal: forall (i0 : I) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)), @Equal_PA_mor PA1 PA2 (PA_f i0) (PA_f i) *)
intros H H0; apply (H g H0).
(* Goal: True *)
(* Goal: forall i : I, P (PA_f i) *)
intro j; simpl in |- *; intro eqij; apply Sym; trivial.
Qed.

Canonical Structure PA_mor_setoid (x y : PA_ob) :=
  Build_Setoid (Equal_PA_mor_Equiv x y).

(* composition *)

Definition Comp_PA_mor (x y z : PA_ob) (f : PA_mor x y) :=
  match f in (PA_mor p p0) return (PA_mor p0 z -> PA_mor p z) with
  | PA_I1 => 
      (* PA_I1 *) 
      match z as p return (PA_mor PA1 p -> PA_mor PA1 p) with
      | PA1 =>
          (* PA1 *)  fun _ => PA_I1 
                     (* PA2 *) 
      | PA2 => fun g => g
      end
      (* PA_I2 *) 
  | PA_I2 =>
      match z as p return (PA_mor PA2 p -> PA_mor PA2 p) with
      | PA1 =>
          (* PA1 *) 
          fun g => PA_21_rect (fun _ => PA_mor PA2 PA1) g
          (* PA2 *) 
      | PA2 => fun _ => PA_I2
      end
      (* PA_f  *) 
  | PA_f x =>
      match z as p return (I -> PA_mor PA2 p -> PA_mor PA1 p) with
      | PA1 =>
          (* PA1 *) 
          fun _ g => PA_21_rect (fun _ => PA_mor PA1 PA1) g
          (* PA2 *) 
      | PA2 => fun i _ => PA_f i
      end x
  end.
(* *)

(* code complique' pour contourner bug Generalize *)

Lemma Comp_PA_fact1 :
 forall (f : PA_mor PA1 PA1) (x : PA_ob) (g : PA_mor PA1 x),
 Comp_PA_mor f g =_S g.
Proof.
intros f x g;
 apply (PA_11_ind (P:=fun x' : PA_mor PA1 PA1 => Comp_PA_mor x' g =_S g)).
(* Goal: @Equal (PA_mor_setoid PA2 x) (@Comp_PA_mor PA2 PA2 x PA_I2 g) g *)
generalize g.
(* Goal: forall g : PA_mor PA2 x, @Equal (PA_mor_setoid PA2 x) (@Comp_PA_mor PA2 PA2 x PA_I2 g) g *)
elim x.
(* Goal: forall (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 PA_I2), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA1 PA2)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
simpl in |- *; auto.
(* Goal: forall g : PA_mor PA1 PA2, @Equal (PA_mor_setoid PA1 PA2) (@Comp_PA_mor PA1 PA1 PA2 PA_I1 g) g *)
intro g1; apply Refl.
Qed.

Lemma Comp_PA_fact2 :
 forall (f : PA_mor PA2 PA2) (x : PA_ob) (g : PA_mor PA2 x),
 Comp_PA_mor f g =_S g.
Proof.
intros f x g;
 apply (PA_22_ind (P:=fun x' : PA_mor PA2 PA2 => Comp_PA_mor x' g =_S g)).
(* Goal: @Equal (PA_mor_setoid PA2 x) (@Comp_PA_mor PA2 PA2 x PA_I2 g) g *)
generalize g.
(* Goal: forall g : PA_mor PA2 x, @Equal (PA_mor_setoid PA2 x) (@Comp_PA_mor PA2 PA2 x PA_I2 g) g *)
elim x.
intro g1;
 apply
  (PA_21_ind
     (fun x' : PA_mor PA2 PA1 =>
      PA_21_rect (fun _ : PA_mor PA2 PA1 => PA_mor PA2 PA1) g1 =_S g1) g1).
(* Goal: forall (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 PA_I2), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA1 PA2)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
simpl in |- *; auto.
Qed.

Lemma Comp_PA_fact3 :
 forall (i : I) (g : PA_mor PA2 PA2), Comp_PA_mor (PA_f i) g =_S PA_f i.
Proof.
intros i g;
 apply
  (PA_22_ind
     (P:=fun x' : PA_mor PA2 PA2 => Comp_PA_mor (PA_f i) x' =_S PA_f i)).
(* Goal: @Equal (PA_mor_setoid PA1 PA2) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) PA_I2) (PA_f i) *)
apply Refl.
Qed.

Lemma Comp_PA_fact4 :
 forall (i : I) (g : PA_mor PA2 PA1) (h : PA_mor PA1 PA1),
 Comp_PA_mor (PA_f i) g =_S h.
Proof.
intros i g h;
 apply
  (PA_21_ind (fun x' : PA_mor PA2 PA1 => Comp_PA_mor (PA_f i) g =_S h) g).
Qed.


(** **)

Lemma Comp_PA_congl : Congl_law Comp_PA_mor.
Proof.
(* Goal: @Congl_law PA_ob PA_mor_setoid Comp_PA_mor *)
unfold Congl_law in |- *.
(* Goal: forall (a b c : PA_ob) (f g : Carrier (PA_mor_setoid b c)) (h : Carrier (PA_mor_setoid a b)) (_ : @Equal (PA_mor_setoid b c) f g), @Equal (PA_mor_setoid a c) (@Comp_PA_mor a b c h f) (@Comp_PA_mor a b c h g) *)
intros x y z f g h.
(* Goal: @Equal (PA_mor_setoid PA2 x) (@Comp_PA_mor PA2 PA2 x PA_I2 g) g *)
generalize f; generalize g.
(* Goal: forall (g f : Carrier (PA_mor_setoid y z)) (_ : @Equal (PA_mor_setoid y z) f g), @Equal (PA_mor_setoid x z) (@Comp_PA_mor x y z h f) (@Comp_PA_mor x y z h g) *)
elim h; elim z.
(* cas 1*)
(* cas 1.1 *)
(* Goal: forall (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 PA_I2), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA1 PA2)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
simpl in |- *; auto.
(* cas 1.2 *)
(* Goal: forall (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 PA_I2), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA1 PA2)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
simpl in |- *; auto.
(* cas 2 *)
(* cas 2.1 *)
(* Goal: forall (g f : Carrier (PA_mor_setoid PA2 PA1)) (_ : @Equal (PA_mor_setoid PA2 PA1) f g), @Equal (PA_mor_setoid PA2 PA1) (@Comp_PA_mor PA2 PA2 PA1 PA_I2 f) (@Comp_PA_mor PA2 PA2 PA1 PA_I2 g) *)
(* Goal: forall (g f : Carrier (PA_mor_setoid PA2 PA2)) (_ : @Equal (PA_mor_setoid PA2 PA2) f g), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 f) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 g) *)
(* Goal: forall (i : I) (g f : Carrier (PA_mor_setoid PA2 PA1)) (_ : @Equal (PA_mor_setoid PA2 PA1) f g), @Equal (PA_mor_setoid PA1 PA1) (@Comp_PA_mor PA1 PA2 PA1 (PA_f i) f) (@Comp_PA_mor PA1 PA2 PA1 (PA_f i) g) *)
(* Goal: forall (i : I) (g f : Carrier (PA_mor_setoid PA2 PA2)) (_ : @Equal (PA_mor_setoid PA2 PA2) f g), @Equal (PA_mor_setoid PA1 PA2) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) f) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) g) *)
intros f0 g0 H.
apply
 (PA_21_ind
    (fun x : PA_mor PA2 PA1 => Comp_PA_mor PA_I2 g0 =_S Comp_PA_mor PA_I2 f0)
    g0).
(* cas 2.2 *)
(* Goal: forall (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 PA_I2), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA1 PA2)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
simpl in |- *; auto.
(* cas 3 *)
(* cas 3.1 *)
(* Goal: forall (i : I) (g f : Carrier (PA_mor_setoid PA2 PA1)) (_ : @Equal (PA_mor_setoid PA2 PA1) f g), @Equal (PA_mor_setoid PA1 PA1) (@Comp_PA_mor PA1 PA2 PA1 (PA_f i) f) (@Comp_PA_mor PA1 PA2 PA1 (PA_f i) g) *)
(* Goal: forall (i : I) (g f : Carrier (PA_mor_setoid PA2 PA2)) (_ : @Equal (PA_mor_setoid PA2 PA2) f g), @Equal (PA_mor_setoid PA1 PA2) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) f) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) g) *)
intros i g0 f0 H.
apply
 (PA_21_ind
    (fun x : PA_mor PA2 PA1 =>
     Comp_PA_mor (PA_f i) f0 =_S Comp_PA_mor (PA_f i) g0) f0).
(* cas 3.2 *)
(* Goal: @Equal (PA_mor_setoid PA1 PA2) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) PA_I2) (PA_f i) *)
intros i g0 f0 H; apply Refl.
Qed.

Lemma Comp_PA_congr : Congr_law Comp_PA_mor.
Proof.
(* Goal: @Congr_law PA_ob PA_mor_setoid Comp_PA_mor *)
unfold Congr_law in |- *.
(* Goal: forall (a b c : PA_ob) (f g : Carrier (PA_mor_setoid a b)) (h : Carrier (PA_mor_setoid b c)) (_ : @Equal (PA_mor_setoid a b) f g), @Equal (PA_mor_setoid a c) (@Comp_PA_mor a b c f h) (@Comp_PA_mor a b c g h) *)
intros x y z f; elim f.
(* cas 1 *)
intro g;
 lapply
  (PA_11_ind
     (P:=fun x' : PA_mor PA1 PA1 =>
         forall h : PA_mor PA1 z,
         PA_I1 =_S x' -> Comp_PA_mor PA_I1 h =_S Comp_PA_mor x' h)).
(* Goal: forall (_ : forall (x : PA_mor PA1 PA2) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) x), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z x h)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
(* Goal: forall (i0 : I) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z (PA_f i0) h) *)
intros H h H0; apply (H g h H0).
(* Goal: forall (i0 : I) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z (PA_f i0) h) *)
elim z.
(* cas 1.1 *)
(* Goal: forall (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 PA_I2), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA1 PA2)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
simpl in |- *; auto.
(* cas 1.2 *)
(* Goal: @Equal (PA_mor_setoid PA1 PA2) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) PA_I2) (PA_f i) *)
intros h H; apply Refl.
(* cas 2 *)
intro g;
 lapply
  (PA_22_ind
     (P:=fun x' : PA_mor PA2 PA2 =>
         forall h : PA_mor PA2 z,
         Equal_PA_mor PA_I2 x' -> Comp_PA_mor PA_I2 h =_S Comp_PA_mor x' h)).
(* Goal: forall (_ : forall (x : PA_mor PA1 PA2) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) x), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z x h)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
(* Goal: forall (i0 : I) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z (PA_f i0) h) *)
intros H h H0; apply (H g h H0).
(* Goal: forall (i0 : I) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z (PA_f i0) h) *)
elim z.
(* cas 2.1 *)
intros h H;
 apply
  (PA_21_ind
     (fun x' : PA_mor PA2 PA1 => Comp_PA_mor PA_I2 h =_S Comp_PA_mor PA_I2 h)
     h).
(* cas 2.2 *)
(* Goal: forall (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA2 PA2 PA_I2 PA_I2), @Equal (PA_mor_setoid PA2 PA2) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) (@Comp_PA_mor PA2 PA2 PA2 PA_I2 h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA1 PA2)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
simpl in |- *; auto.
(* cas 3 *)
intros i g;
 lapply
  (PA_12_ind
     (P:=fun x' : PA_mor PA1 PA2 =>
         forall h : PA_mor PA2 z,
         Equal_PA_mor (PA_f i) x' ->
         Comp_PA_mor (PA_f i) h =_S Comp_PA_mor x' h)).
(* Goal: forall (_ : forall (x : PA_mor PA1 PA2) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) x), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z x h)) (h : Carrier (PA_mor_setoid PA2 z)) (_ : @Equal (PA_mor_setoid PA1 PA2) (PA_f i) g), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z g h) *)
(* Goal: forall (i0 : I) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z (PA_f i0) h) *)
intros H h H0; apply (H g h H0).
(* Goal: forall (i0 : I) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z (PA_f i0) h) *)
elim z.
(* cas 3.1 *)
intros j h H;
 apply
  (PA_21_ind
     (fun x' : PA_mor PA2 PA1 =>
      Comp_PA_mor (PA_f i) h =_S Comp_PA_mor (PA_f j) h) h).
(* cas 3.2 *)
(* Goal: forall (i0 : I) (h : PA_mor PA2 PA2) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)), @Equal (PA_mor_setoid PA1 PA2) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) h) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i0) h) *)
intros j h H; simpl in |- *; exact H.
Qed.

(** **)

Definition Comp_PA := Build_Comp Comp_PA_congl Comp_PA_congr.

Lemma Assoc_PA : Assoc_law Comp_PA.
Proof.
(* Goal: @Assoc_law PA_ob PA_mor_setoid Comp_PA *)
unfold Assoc_law in |- *.
(* Goal: forall (a b c d : PA_ob) (f : Carrier (PA_mor_setoid a b)) (g : Carrier (PA_mor_setoid b c)) (h : Carrier (PA_mor_setoid c d)), @Equal (PA_mor_setoid a d) (@Cat_comp PA_ob PA_mor_setoid Comp_PA a b d f (@Cat_comp PA_ob PA_mor_setoid Comp_PA b c d g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA a c d (@Cat_comp PA_ob PA_mor_setoid Comp_PA a b c f g) h) *)
intros x y z o4 f; elim f.
(* cas 1 *)
(* Goal: forall (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA2 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 z PA_I2 g) h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
intros g h.
(* Goal: @Equal (PA_mor_setoid PA2 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 z PA_I2 g) h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
apply Trans with (Comp_PA_mor g h).
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA1 o4 PA_I1 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 g h)) (@Comp_PA_mor PA1 z o4 g h) *)
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 z o4 g h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA1 z PA_I1 g) h) *)
(* Goal: forall (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA2 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 z PA_I2 g) h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
apply (Comp_PA_fact1 PA_I1 (Comp_PA_mor g h)).
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 z o4 g h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA1 z PA_I1 g) h) *)
(* Goal: forall (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA2 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 z PA_I2 g) h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
apply (Comp_PA_congr (f:=g) (g:=Comp_PA_mor PA_I1 g) h).
(* Goal: @Equal (PA_mor_setoid PA1 PA2) (PA_f i) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) g) *)
apply Sym.
(* Goal: @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA1 z PA_I1 g) g *)
(* Goal: forall (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA2 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 z PA_I2 g) h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
apply (Comp_PA_fact1 PA_I1 g).
(* cas 2 *)
(* Goal: forall (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA2 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 z PA_I2 g) h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
intros g h.
(* Goal: @Equal (PA_mor_setoid PA2 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 z PA_I2 g) h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
apply Trans with (Comp_PA_mor g h).
(* Goal: @Equal (PA_mor_setoid PA2 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Comp_PA_mor PA2 z o4 g h) *)
(* Goal: @Equal (PA_mor_setoid PA2 o4) (@Comp_PA_mor PA2 z o4 g h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 z PA_I2 g) h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
apply (Comp_PA_fact2 PA_I2 (Comp_PA_mor g h)).
(* Goal: @Equal (PA_mor_setoid PA2 o4) (@Comp_PA_mor PA2 z o4 g h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 z PA_I2 g) h) *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
apply (Comp_PA_congr (f:=g) (g:=Comp_PA_mor PA_I2 g) h).
(* Goal: @Equal (PA_mor_setoid PA1 PA2) (PA_f i) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) g) *)
apply Sym.
(* Goal: @Equal (PA_mor_setoid PA2 z) (@Comp_PA_mor PA2 PA2 z PA_I2 g) g *)
(* Goal: forall (i : I) (g : Carrier (PA_mor_setoid PA2 z)) (h : Carrier (PA_mor_setoid z o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 z o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 z o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 z (PA_f i) g) h) *)
apply (Comp_PA_fact2 PA_I2 g).
(* cas 3 *) 
(* Goal: forall (i0 : I) (h : PA_mor PA2 z) (_ : @Equal_PA_mor PA1 PA2 (PA_f i) (PA_f i0)), @Equal (PA_mor_setoid PA1 z) (@Comp_PA_mor PA1 PA2 z (PA_f i) h) (@Comp_PA_mor PA1 PA2 z (PA_f i0) h) *)
intro i; elim z.
intros g h;
 apply
  (PA_21_ind
     (fun x : PA_mor PA2 PA1 =>
      Comp_PA_mor (PA_f i) (Comp_PA_mor g h) =_S
      Comp_PA_mor (Comp_PA_mor (PA_f i) g) h) g).
(* Goal: forall (g : Carrier (PA_mor_setoid PA2 PA2)) (h : Carrier (PA_mor_setoid PA2 o4)), @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 g h)) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
intros g h; apply Trans with (Comp_PA_mor (PA_f i) h).
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 o4 g h)) (@Comp_PA_mor PA1 PA2 o4 (PA_f i) h) *)
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 PA2 o4 (PA_f i) h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
apply (Comp_PA_congl (f:=Comp_PA_mor g h) (g:=h) (PA_f i)).
(* Goal: @Equal (PA_mor_setoid PA2 o4) (@Comp_PA_mor PA2 PA2 o4 g h) h *)
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 PA2 o4 (PA_f i) h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
apply (Comp_PA_fact2 g h).
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 PA2 o4 (PA_f i) h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
simpl in |- *.
(* Goal: @Equal_PA_mor PA1 o4 (match o4 as p return (forall (_ : I) (_ : PA_mor PA2 p), PA_mor PA1 p) with | PA1 => fun (_ : I) (g : PA_mor PA2 PA1) => PA_21_rect (fun _ : PA_mor PA2 PA1 => PA_mor PA1 PA1) g | PA2 => fun (i : I) (_ : PA_mor PA2 PA2) => PA_f i end i h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
apply (Comp_PA_congr (f:=PA_f i) (g:=Comp_PA_mor (PA_f i) g) h).
(* Goal: @Equal (PA_mor_setoid PA1 PA2) (PA_f i) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) g) *)
apply Sym.
(* Goal: @Equal (PA_mor_setoid PA1 PA2) (@Comp_PA_mor PA1 PA2 PA2 (PA_f i) g) (PA_f i) *)
apply (Comp_PA_fact3 i g).
Qed.

Definition Id_PA (x : PA_ob) :=
  match x as x' return (PA_mor x' x') with
  | PA1 => (* PA1 *)  PA_I1 
      (* PA2 *) 
  | PA2 => PA_I2
  end.

Lemma Idl_PA : Idl_law Comp_PA Id_PA.
Proof.
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 PA2 o4 (PA_f i) h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
unfold Idl_law in |- *; simpl in |- *.
(* Goal: forall (a b : PA_ob) (f : PA_mor a b), @Equal_PA_mor a b (@Cat_comp PA_ob PA_mor_setoid Comp_PA a a b (Id_PA a) f) f *)
intros x y; elim x; intro f.
(* Goal: @Equal_PA_mor PA1 y (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA1 y (Id_PA PA1) f) f *)
(* Goal: @Equal_PA_mor PA2 y (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 y (Id_PA PA2) f) f *)
apply (Comp_PA_fact1 PA_I1 f).
(* Goal: @Equal_PA_mor PA2 y (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 y (Id_PA PA2) f) f *)
apply (Comp_PA_fact2 PA_I2 f).
Qed.

Lemma Idr_PA : Idr_law Comp_PA Id_PA.
Proof.
(* Goal: @Equal (PA_mor_setoid PA1 o4) (@Comp_PA_mor PA1 PA2 o4 (PA_f i) h) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 o4 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) g) h) *)
unfold Idr_law in |- *; simpl in |- *.
(* Goal: forall (a b : PA_ob) (f : PA_mor b a), @Equal_PA_mor b a f (@Cat_comp PA_ob PA_mor_setoid Comp_PA b a a f (Id_PA a)) *)
intros x y f; elim f.
(* Goal: @Equal_PA_mor PA1 PA1 PA_I1 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA1 PA1 PA_I1 (Id_PA PA1)) *)
(* Goal: @Equal_PA_mor PA2 PA2 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 PA2 PA_I2 (Id_PA PA2)) *)
(* Goal: forall i : I, @Equal_PA_mor PA1 PA2 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) (Id_PA PA2)) *)
apply (Comp_PA_fact1 PA_I1 PA_I1).
(* Goal: @Equal_PA_mor PA2 PA2 PA_I2 (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA2 PA2 PA2 PA_I2 (Id_PA PA2)) *)
(* Goal: forall i : I, @Equal_PA_mor PA1 PA2 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) (Id_PA PA2)) *)
apply (Comp_PA_fact2 PA_I2 PA_I2).
(* Goal: forall i : I, @Equal_PA_mor PA1 PA2 (PA_f i) (@Cat_comp PA_ob PA_mor_setoid Comp_PA PA1 PA2 PA2 (PA_f i) (Id_PA PA2)) *)
intro i; apply (Comp_PA_fact3 i PA_I2).
Qed.

Canonical Structure PA := Build_Category Assoc_PA Idl_PA Idr_PA.

End pa_def.