(* 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        *)
(*****************************************************************************)
(*									     *)
(*	                       Equalizers                		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

Require Export Equalizers.
Require Export PA.
Require Export Limit.

Set Implicit Arguments.
Unset Strict Implicit.

(* PA -> C *)

Section equalizer_limit_def.

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

Definition FPA_ob (x : PA k) := match x with
                                | PA1 => a
                                | PA2 => b
                                end.

Definition FPA_mor (x y : PA k) (f : x --> y) :=
  match f in (PA_mor _ x' y') return (Carrier (FPA_ob x' --> FPA_ob y')) with
  | PA_I1 => Id a
  | PA_I2 => Id b
  | PA_f i => k i
  end.

Lemma FPA_map_law : forall x y : PA_ob, Map_law (FPA_mor (x:=x) (y:=y)).
Proof.
(* Goal: forall x y : PA_ob, @Map_law (@Hom (@PA C a b I k) x y) (@Hom C (FPA_ob x) (FPA_ob y)) (@FPA_mor x y) *)
unfold Map_law in |- *; simpl in |- *.
(* Goal: forall (x y : PA_ob) (x0 y0 : PA_mor I x y) (_ : @Equal_PA_mor C a b I k x y x0 y0), @Equal (@Hom C (FPA_ob x) (FPA_ob y)) (@FPA_mor x y x0) (@FPA_mor x y y0) *)
intros x y f; elim f.
(* 1 *)
simpl in |- *; intros g H;
 apply (PA_11_ind (P:=fun x : PA_mor_setoid k PA1 PA1 => Id a =_S FPA_mor x)).
(* Goal: @Equal (@Hom C b b) (@Id C b) (@FPA_mor PA2 PA2 (PA_I2 I)) *)
(* Goal: forall (i : I) (y : PA_mor I PA1 PA2) (_ : @Equal_PA_mor C a b I k PA1 PA2 (@PA_f I i) y), @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@FPA_mor PA1 PA2 (@PA_f I i)) (@FPA_mor PA1 PA2 y) *)
simpl in |- *; apply Refl.
(* 2 *)
simpl in |- *; intros g H;
 apply
  (PA_22_ind (P:=fun x' : PA_mor_setoid k PA2 PA2 => Id b =_S FPA_mor x')).
(* Goal: @Equal (@Hom C b b) (@Id C b) (@FPA_mor PA2 PA2 (PA_I2 I)) *)
(* Goal: forall (i : I) (y : PA_mor I PA1 PA2) (_ : @Equal_PA_mor C a b I k PA1 PA2 (@PA_f I i) y), @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@FPA_mor PA1 PA2 (@PA_f I i)) (@FPA_mor PA1 PA2 y) *)
simpl in |- *; apply Refl.
(* 3 *)
intros i g;
 lapply
  (PA_12_ind
     (P:=fun x' : PA_mor_setoid k PA1 PA2 =>
         Equal_PA_mor k (PA_f i) x' -> k i =_S FPA_mor x')).
(* Goal: forall (_ : forall (x : PA_mor I PA1 PA2) (_ : @Equal_PA_mor C a b I k PA1 PA2 (@PA_f I i) x), @Equal (@Hom C a b) (k i) (@FPA_mor PA1 PA2 x)) (_ : @Equal_PA_mor C a b I k PA1 PA2 (@PA_f I i) g), @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@FPA_mor PA1 PA2 (@PA_f I i)) (@FPA_mor PA1 PA2 g) *)
(* Goal: forall (i0 : I) (_ : @Equal_PA_mor C a b I k PA1 PA2 (@PA_f I i) (@PA_f I i0)), @Equal (@Hom C a b) (k i) (@FPA_mor PA1 PA2 (@PA_f I i0)) *)
intros H H0; apply (H g H0).
(* Goal: forall (i0 : I) (_ : @Equal_PA_mor C a b I k PA1 PA2 (@PA_f I i) (@PA_f I i0)), @Equal (@Hom C a b) (k i) (@FPA_mor PA1 PA2 (@PA_f I i0)) *)
simpl in |- *; auto.
Qed.

Canonical Structure FPA_map (x y : PA k) :=
  Build_Map (FPA_map_law (x:=x) (y:=y)).

Lemma FPA_comp_law : Fcomp_law FPA_map.
Proof.
(* Goal: @Fcomp_law (@PA C a b I k) C FPA_ob FPA_map *)
unfold Fcomp_law in |- *.
(* Goal: forall (a0 b0 c : Ob (@PA C a b I k)) (f : Carrier (@Hom (@PA C a b I k) a0 b0)) (g : Carrier (@Hom (@PA C a b I k) b0 c)), @Equal (@Hom C (FPA_ob a0) (FPA_ob c)) (@Ap (@Hom (@PA C a b I k) a0 c) (@Hom C (FPA_ob a0) (FPA_ob c)) (FPA_map a0 c) (@Comp (@PA C a b I k) a0 b0 c f g)) (@Comp C (FPA_ob a0) (FPA_ob b0) (FPA_ob c) (@Ap (@Hom (@PA C a b I k) a0 b0) (@Hom C (FPA_ob a0) (FPA_ob b0)) (FPA_map a0 b0) f) (@Ap (@Hom (@PA C a b I k) b0 c) (@Hom C (FPA_ob b0) (FPA_ob c)) (FPA_map b0 c) g)) *)
intros x y z f; elim f.
(* 1 *)
(* Goal: forall g : Carrier (@Hom (@PA C a b I k) PA2 z), @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) (@Comp (@PA C a b I k) PA2 PA2 z (PA_I2 I) g)) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
intro g.
(* Goal: @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) (@Comp (@PA C a b I k) PA2 PA2 z (PA_I2 I) g)) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* *) apply Trans with (FPA_map _ _ g).
(* Goal: @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) (@Comp (@PA C a b I k) PA2 PA2 z (PA_I2 I) g)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g) *)
(* Goal: @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
apply Pres1.
(* Goal: @Equal (@Hom (@PA C a b I k) PA1 z) (@Comp (@PA C a b I k) PA1 PA1 z (PA_I1 I) g) g *)
(* Goal: @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) g) (@Comp C (FPA_ob PA1) (FPA_ob PA1) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA1) (@Hom C (FPA_ob PA1) (FPA_ob PA1)) (FPA_map PA1 PA1) (PA_I1 I)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) g)) *)
(* Goal: forall g : Carrier (@Hom (@PA C a b I k) PA2 z), @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) (@Comp (@PA C a b I k) PA2 PA2 z (PA_I2 I) g)) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
apply (Comp_PA_fact1 k (PA_I1 I) g).
(* Goal: @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
simpl in |- *; apply Idl1.
(* 2 *)
(* Goal: forall g : Carrier (@Hom (@PA C a b I k) PA2 z), @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) (@Comp (@PA C a b I k) PA2 PA2 z (PA_I2 I) g)) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
intro g.
(* Goal: @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) (@Comp (@PA C a b I k) PA2 PA2 z (PA_I2 I) g)) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* *) apply Trans with (FPA_map _ _ g).
(* Goal: @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) (@Comp (@PA C a b I k) PA2 PA2 z (PA_I2 I) g)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g) *)
(* Goal: @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
apply Pres1.
(* Goal: @Equal (@Hom (@PA C a b I k) PA2 z) (@Comp (@PA C a b I k) PA2 PA2 z (PA_I2 I) g) g *)
(* Goal: @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
apply (Comp_PA_fact2 k (PA_I2 I) g).
(* Goal: @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
simpl in |- *; apply Idl1.
(* 3 *)
(* Goal: forall g : Carrier (@Hom (@PA C a b I k) PA2 z), @Equal (@Hom C (FPA_ob PA2) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) (@Comp (@PA C a b I k) PA2 PA2 z (PA_I2 I) g)) (@Comp C (FPA_ob PA2) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) (PA_I2 I)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
(* Goal: forall (i : I) (g : Carrier (@Hom (@PA C a b I k) PA2 z)), @Equal (@Hom C (FPA_ob PA1) (FPA_ob z)) (@Ap (@Hom (@PA C a b I k) PA1 z) (@Hom C (FPA_ob PA1) (FPA_ob z)) (FPA_map PA1 z) (@Comp (@PA C a b I k) PA1 PA2 z (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob z) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 z) (@Hom C (FPA_ob PA2) (FPA_ob z)) (FPA_map PA2 z) g)) *)
intro i; elim z; intro g.
apply
 (PA_21_ind
    (fun x' : PA_mor I PA2 PA1 =>
     FPA_mor (Comp_PA_mor (PA_f i) g) =_S k i o FPA_mor g) g).
(* Goal: @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@Comp (@PA C a b I k) PA1 PA2 PA2 (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob PA2) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) g)) *)
simpl in |- *.
(* Goal: @Equal (@Hom C a b) (k i) (@Comp C a b b (k i) (@FPA_mor PA2 PA2 g)) *)
apply (PA_22_ind (P:=fun x : PA_mor I PA2 PA2 => k i =_S k i o FPA_mor x)).
(* Goal: @Equal (@Hom C a b) (k i) (@Comp C a b (FPA_ob PA2) (k i) (@FPA_mor PA2 PA2 (PA_I2 I))) *)
simpl in |- *; apply Idr. 
Qed.

Lemma FPA_id_law : Fid_law FPA_map.
Proof.
(* Goal: @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@Comp (@PA C a b I k) PA1 PA2 PA2 (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob PA2) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) g)) *)
unfold Fid_law in |- *; simpl in |- *.
(* Goal: @Equal (@Hom C b b) (@Id C b) (@FPA_mor PA2 PA2 (PA_I2 I)) *)
(* Goal: forall (i : I) (y : PA_mor I PA1 PA2) (_ : @Equal_PA_mor C a b I k PA1 PA2 (@PA_f I i) y), @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@FPA_mor PA1 PA2 (@PA_f I i)) (@FPA_mor PA1 PA2 y) *)
intro x; elim x; simpl in |- *; apply Refl.
Qed.

Canonical Structure FPA := Build_Functor FPA_comp_law FPA_id_law.

SubClass Equalizer1 := Limit FPA.

(* The Type I must be non empty *)

Structure Equalizer2 : Type :=  {Prf_equalizer1 :> Equalizer1; Witness : I}.

Variable l : Equalizer2.

Definition E1_ob := Lim l.

Definition E1_mor : E1_ob --> a := Limiting_cone l PA1.
 
Lemma Prf_E1_law1 : Equalizer_law1 k E1_mor.
Proof.
(* Goal: @Equalizer_law1 C a b I k E1_ob E1_mor *)
unfold Equalizer_law1, Equalizer_eq, E1_mor in |- *.
(* Goal: forall i j : I, @Equal (@Hom C E1_ob b) (@Comp C E1_ob a b (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1) (k i)) (@Comp C E1_ob a b (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1) (k j)) *)
intros i j.
(* Goal: @Equal (@Hom C E1_ob b) (@Comp C E1_ob a b (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1) (k i)) (@Comp C E1_ob a b (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1) (k j)) *)
(* *) apply Trans with (Limiting_cone l PA2). 
(* Goal: @Equal (@Hom C (@FOb (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) PA2) (@FOb (@PA C a b I k) C FPA PA2)) (@Comp C E1_ob a b (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1) (k i)) (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA2) *)
(* Goal: @Equal (@Hom C (@FOb (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) PA2) (@FOb (@PA C a b I k) C FPA PA2)) (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA2) (@Comp C E1_ob a b (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1) (k j)) *)
apply (EqC1 (Limiting_cone l) (PA_f i)).
(* Goal: @Equal (@Hom C (@FOb (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) PA2) (@FOb (@PA C a b I k) C FPA PA2)) (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA2) (@Comp C E1_ob a b (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1) (k j)) *)
apply (EqC (Limiting_cone l) (PA_f j)).
Qed.

(* construire a` partir de h, un cone r -> fpa *)
(* C'est la` ou` on a besoin que I ne soit pas vide *)

 Section e1_diese_def.

 Variables (r : C) (h : r --> a).
 Hypothesis p : Equalizer_eq k h.

 Definition E_tau (x : PA k) :=
   match x as x' return (Carrier (r --> FPA x')) with
   | PA1 => h
   | PA2 => h o k (Witness l)
   end.
 
 Lemma E_tau_cone_law : Cone_law E_tau.
 Proof.
(* Goal: @Cone_law (@PA C a b I k) C r FPA E_tau *)
 unfold Cone_law in |- *; intros x o2 f.
(* Goal: @Equal (@Hom C r (@FOb (@PA C a b I k) C FPA o2)) (E_tau o2) (@Comp C r (@FOb (@PA C a b I k) C FPA x) (@FOb (@PA C a b I k) C FPA o2) (E_tau x) (@FMor (@PA C a b I k) C FPA x o2 f)) *)
 elim f.
 (* 1 *)
(* Goal: @Equal (@Hom C a b) (k i) (@Comp C a b (FPA_ob PA2) (k i) (@FPA_mor PA2 PA2 (PA_I2 I))) *)
 unfold FMor in |- *; simpl in |- *; apply Idr.
 (* 2 *)
(* Goal: @Equal (@Hom C a b) (k i) (@Comp C a b (FPA_ob PA2) (k i) (@FPA_mor PA2 PA2 (PA_I2 I))) *)
 unfold FMor in |- *; simpl in |- *; apply Idr.
 (* 3 *)
(* Goal: @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@Comp (@PA C a b I k) PA1 PA2 PA2 (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob PA2) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) g)) *)
 unfold FMor in |- *; simpl in |- *.
(* Goal: forall i : I, @Equal (@Hom C r b) (@Comp C r a b h (k (Witness l))) (@Comp C r a b h (k i)) *)
 intro i; apply (p (Witness l) i).
 Qed.
 
 Definition E_NT := Build_Cone E_tau_cone_law.

 Definition E1_diese : r --> E1_ob := Lim_diese l E_NT.
 
 End e1_diese_def.

Lemma Prf_E1_law2 : Equalizer_law2 E1_mor E1_diese.
Proof.
(* Goal: @Equalizer_law2 C a b I k E1_ob E1_mor E1_diese *)
unfold Equalizer_law2, E1_mor, Equalizer_eq in |- *.
(* Goal: forall (r : Ob C) (h : Carrier (@Hom C r a)) (p : forall i j : I, @Equal (@Hom C r b) (@Comp C r a b h (k i)) (@Comp C r a b h (k j))), @Equal (@Hom C r a) h (@Comp C r E1_ob a (@E1_diese r h p) (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1)) *)
intros r h p.
(* Goal: @Equal (@Hom C r a) h (@Comp C r E1_ob a (@E1_diese r h p) (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1)) *)
apply Sym; apply (Prf_limit1 l (E_NT p) PA1).
Qed.

Lemma Prf_E1_law3 : Equalizer_law3 E1_mor E1_diese.
Proof.
(* Goal: @Equalizer_law3 C a b I k E1_ob E1_mor E1_diese *)
unfold Equalizer_law3, E1_mor, Equalizer_eq in |- *.
(* Goal: forall (r : Ob C) (h : Carrier (@Hom C r a)) (p : forall i j : I, @Equal (@Hom C r b) (@Comp C r a b h (k i)) (@Comp C r a b h (k j))) (l0 : Carrier (@Hom C r E1_ob)) (_ : @Equal (@Hom C r a) h (@Comp C r E1_ob a l0 (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1))), @Equal (@Hom C r E1_ob) l0 (@E1_diese r h p) *)
intros r h p q H.
(* Goal: @Equal (@Hom C r E1_ob) q (@E1_diese r h p) *)
unfold E1_diese in |- *; apply (Prf_limit2 l).
(* Goal: @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@Comp (@PA C a b I k) PA1 PA2 PA2 (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob PA2) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) g)) *)
unfold Limit_eq in |- *; simpl in |- *.
(* Goal: @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@Comp (@PA C a b I k) PA1 PA2 PA2 (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob PA2) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) g)) *)
intro x; elim x; simpl in |- *.
(* Goal: @Equal (@Hom C r a) (@Comp C r (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l)) a q (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1)) h *)
(* Goal: @Equal (@Hom C r b) (@Comp C r (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l)) b q (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA2)) (@Comp C r a b h (k (Witness l))) *)
apply Sym; apply H.
(* Goal: @Equal (@Hom C r b) (@Comp C r (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l)) b q (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA2)) (@Comp C r a b h (k (Witness l))) *)
(* *) apply Trans with ((q o E1_mor) o k (Witness l)).
(* Goal: @Equal (@Hom C r b) (@Comp C r (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l)) b q (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA2)) (@Comp C r a b (@Comp C r E1_ob a q E1_mor) (k (Witness l))) *)
(* Goal: @Equal (@Hom C r b) (@Comp C r a b (@Comp C r E1_ob a q E1_mor) (k (Witness l))) (@Comp C r a b h (k (Witness l))) *)
(* *) apply Trans with (q o E1_mor o k (Witness l)).
(* Goal: @Equal (@Hom C r b) (@Comp C r (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l)) b q (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA2)) (@Comp C r E1_ob b q (@Comp C E1_ob a b E1_mor (k (Witness l)))) *)
(* Goal: @Equal (@Hom C r b) (@Comp C r E1_ob b q (@Comp C E1_ob a b E1_mor (k (Witness l)))) (@Comp C r a b (@Comp C r E1_ob a q E1_mor) (k (Witness l))) *)
(* Goal: @Equal (@Hom C r b) (@Comp C r a b (@Comp C r E1_ob a q E1_mor) (k (Witness l))) (@Comp C r a b h (k (Witness l))) *)
apply Comp_l.
(* Goal: @Equal (@Hom C E1_ob b) (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA2) (@Comp C E1_ob a b E1_mor (k (Witness l))) *)
(* Goal: @Equal (@Hom C r b) (@Comp C r E1_ob b q (@Comp C E1_ob a b E1_mor (k (Witness l)))) (@Comp C r a b (@Comp C r E1_ob a q E1_mor) (k (Witness l))) *)
(* Goal: @Equal (@Hom C r b) (@Comp C r a b (@Comp C r E1_ob a q E1_mor) (k (Witness l))) (@Comp C r a b h (k (Witness l))) *)
apply (EqC (Limiting_cone l) (PA_f (Witness l))).
(* Goal: @Equal (@Hom C r b) (@Comp C r E1_ob b q (@Comp C E1_ob a b E1_mor (k (Witness l)))) (@Comp C r a b (@Comp C r E1_ob a q E1_mor) (k (Witness l))) *)
(* Goal: @Equal (@Hom C r b) (@Comp C r a b (@Comp C r E1_ob a q E1_mor) (k (Witness l))) (@Comp C r a b h (k (Witness l))) *)
apply Ass.
(* Goal: @Equal (@Hom C r a) (@Comp C r (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l)) a q (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA1)) h *)
(* Goal: @Equal (@Hom C r b) (@Comp C r (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l)) b q (@ApNT (@PA C a b I k) C (@Const (@PA C a b I k) C (@Lim (@PA C a b I k) C FPA (Prf_equalizer1 l))) FPA (@Limiting_cone (@PA C a b I k) C FPA (Prf_equalizer1 l)) PA2)) (@Comp C r a b h (k (Witness l))) *)
apply Comp_r; apply Sym; apply H.
Qed.

Canonical Structure Equalizer2_to_Equalizer :=
  Build_Equalizer Prf_E1_law1 Prf_E1_law2 Prf_E1_law3.

End equalizer_limit_def.

Coercion Equalizer2_to_Equalizer : Equalizer2 >-> Equalizer.

(* cas particuliers *)

(* de deux morhismes *)

Section equaz_fg.

Variables (C : Category) (a b : C) (f g : a --> b).

Definition K_fg (i : TwoElts) := match i with
                                 | Elt1 => f
                                 | Elt2 => g
                                 end.

Definition J_fg := PA K_fg.

Definition F_fg := FPA K_fg.

SubClass Equalizer1_fg := Equalizer1 K_fg.

Lemma Prf_law1_fg :
 forall (r : C) (h : r --> a), h o f =_S h o g -> Equalizer_eq K_fg h.
Proof.
(* Goal: forall (r : Ob C) (h : Carrier (@Hom C r a)) (_ : @Equal (@Hom C r b) (@Comp C r a b h f) (@Comp C r a b h g)), @Equalizer_eq C a b TwoElts K_fg r h *)
intros r h H; unfold Equalizer_eq in |- *.
(* Goal: @Equal (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@Comp (@PA C a b I k) PA1 PA2 PA2 (@PA_f I i) g)) (@Comp C (FPA_ob PA1) (FPA_ob PA2) (FPA_ob PA2) (@Ap (@Hom (@PA C a b I k) PA1 PA2) (@Hom C (FPA_ob PA1) (FPA_ob PA2)) (FPA_map PA1 PA2) (@PA_f I i)) (@Ap (@Hom (@PA C a b I k) PA2 PA2) (@Hom C (FPA_ob PA2) (FPA_ob PA2)) (FPA_map PA2 PA2) g)) *)
intros i j; elim i; elim j; simpl in |- *.
(* Goal: @Equal (@Hom C r b) (@Comp C r a b h g) (@Comp C r a b h g) *)
apply Refl.
(* Goal: @Equal (@Hom C r b) (@Comp C r a b h f) (@Comp C r a b h g) *)
(* Goal: @Equal (@Hom C r b) (@Comp C r a b h g) (@Comp C r a b h f) *)
(* Goal: @Equal (@Hom C r b) (@Comp C r a b h g) (@Comp C r a b h g) *)
apply H.
(* Goal: @Equal (@Hom C r b) (@Comp C r a b h g) (@Comp C r a b h f) *)
(* Goal: @Equal (@Hom C r b) (@Comp C r a b h g) (@Comp C r a b h g) *)
apply Sym; trivial.
(* Goal: @Equal (@Hom C r b) (@Comp C r a b h g) (@Comp C r a b h g) *)
apply Refl.
Qed.

End equaz_fg.

(* Equalizer du hom-set C(a,b) *)

Section equaz_hom.

Variables (C : Category) (a b : C).

Definition K_hom (f : a --> b) := f.

Definition J_hom := PA K_hom.

Definition F_hom := FPA K_hom.

SubClass Equalizer1_hom := Equalizer1 K_hom.

End equaz_hom.