(* 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        *)
(*****************************************************************************)
(*									     *)
(*	    Limits by Producys and equalizers              		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                        A.SAIBI         May 95			     *)
(*									     *)
(*****************************************************************************)

Require Export Equalizers1.
Require Export Products1.

Set Implicit Arguments.
Unset Strict Implicit.

Section thl.

Variables (C J : Category) (H1 : forall k : J -> C, Product1 k)
  (H2 : forall k : Arrs J -> C, Product1 k)
  (H3 : forall (a b : C) (f g : a --> b), Equalizer1_fg f g)
  (F : Functor J C).

Let Limit2_fg (a b : C) (f g : a --> b) := Build_Equalizer2 (H3 f g) Elt1.

(* IIi Fi *)

Definition Thl_k_Fi (i : J) := F i.

Definition Thl_l_Fi := H1 Thl_k_Fi.

Definition Thl_PI_Fi := Pi1 Thl_l_Fi.

(* ||u F(codomu) *)

Definition Thl_k_Fu (u : Arrs J) := F (Codom u).

Definition Thl_l_Fu := H2 Thl_k_Fu.

Definition Thl_PI_Fu := Pi1 Thl_l_Fu.

(* qq u. fu : IIi Fi -> ku (= F(codomu)) *)

Definition Thl_fu (u : Arrs J) := Proj1 Thl_l_Fi (Codom u).

(* donc E! f : IIi Fi -> ||u F(codomu) tq ... *)

Definition Thl_f : Thl_PI_Fi --> Thl_PI_Fu := Pd1_diese Thl_l_Fu Thl_fu.

Lemma Thl_diag1 : forall u : Arrs J, Thl_fu u =_S Thl_f o Proj1 Thl_l_Fu u.
Proof.
(* Goal: forall u : Arrs J, @Equal (@Hom C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Codom J u))) (Thl_fu u) (@Comp C Thl_PI_Fi Thl_PI_Fu (Thl_k_Fu u) Thl_f (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
exact (Prf_pd1_law1 Thl_l_Fu Thl_fu).
Qed.

(* qq u. gu : IIi Fi --p(domu)--> F(domu) --Fu--> ku (= F(codomu)) *)

Definition Thl_gu (u : Arrs J) := Proj1 Thl_l_Fi (Dom u) o FMor F (Arrow u).

(* donc E! g : IIi Fi -> ||u F(codomu) tq ... *)

Definition Thl_g := Pd1_diese Thl_l_Fu Thl_gu.

Lemma Thl_diag2 : forall u : Arrs J, Thl_gu u =_S Thl_g o Proj1 Thl_l_Fu u.
Proof.
(* Goal: forall u : Arrs J, @Equal (@Hom C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u))) (Thl_gu u) (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
exact (Prf_pd1_law1 Thl_l_Fu Thl_gu).
Qed.

(* equalizer de f et g *)

Definition Thl_l_fg := Limit2_fg Thl_f Thl_g.

Definition Thl_d := E1_ob Thl_l_fg.
  
Definition Thl_e := E1_mor Thl_l_fg.
 
(* construction du limiting cone *)

Definition Thl_mu_tau (j : J) := Thl_e o Proj1 Thl_l_Fi j.

Lemma Thl_mu_cone_law : Cone_law Thl_mu_tau.
Proof.
(* Goal: @Cone_law J C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) F Thl_mu_tau *)
unfold Cone_law in |- *; intros j k u; unfold Thl_mu_tau in |- *.
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F k)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi k) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi k)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F j) (@FOb J C F k) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi j) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j)) (@FMor J C F j k u)) *)
(* *) apply Trans with (Thl_e o Thl_f o Proj1 Thl_l_Fu (Build_Arrs u)).
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u)) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u)))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
apply Comp_l.
(* Goal: @Equal (@Hom C Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u))) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi k) (@Comp C Thl_PI_Fi Thl_PI_Fu (Thl_k_Fu (@Build_Arrs J j k u)) Thl_f (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u))) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C Thl_PI_Fi Thl_PI_Fu (Thl_k_Fu (@Build_Arrs J j k u)) Thl_f (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F j) (@FOb J C F k) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi j) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j)) (@FMor J C F j k u)) *)
apply (Thl_diag1 (Build_Arrs u)).
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C Thl_PI_Fi Thl_PI_Fu (Thl_k_Fu (@Build_Arrs J j k u)) Thl_f (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F j) (@FOb J C F k) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi j) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j)) (@FMor J C F j k u)) *)
(* *) apply Trans with (Thl_e o Proj1 Thl_l_Fi j o FMor F u).
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F k)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C Thl_PI_Fi Thl_PI_Fu (Thl_k_Fu (@Build_Arrs J j k u)) Thl_f (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@FOb J C F k) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u))) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F k)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@FOb J C F k) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F j) (@FOb J C F k) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi j) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j)) (@FMor J C F j k u)) *)
(* *) apply Trans with (Thl_e o Thl_g o Proj1 Thl_l_Fu (Build_Arrs u)).
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C Thl_PI_Fi Thl_PI_Fu (Thl_k_Fu (@Build_Arrs J j k u)) Thl_f (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu (@Build_Arrs J j k u)) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu (@Build_Arrs J j k u)) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@FOb J C F k) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u))) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F k)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@FOb J C F k) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F j) (@FOb J C F k) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi j) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j)) (@FMor J C F j k u)) *)
(* *) apply Trans with ((Thl_e o Thl_f) o Proj1 Thl_l_Fu (Build_Arrs u)).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Ass.
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fu (Thl_k_Fu (@Build_Arrs J j k u)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi Thl_PI_Fu Thl_e Thl_f) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu (@Build_Arrs J j k u)) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu (@Build_Arrs J j k u)) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@FOb J C F k) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u))) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F k)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@FOb J C F k) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F j) (@FOb J C F k) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi j) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j)) (@FMor J C F j k u)) *)
(* *) apply Trans with ((Thl_e o Thl_g) o Proj1 Thl_l_Fu (Build_Arrs u)).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c Thl_PI_Fi (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Thl_diese c tau) Thl_e) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) (@ApNT J C (@Const J C c) F tau i) *)
apply Comp_r.
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi Thl_PI_Fu Thl_e Thl_f) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_e Thl_g) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu (@Build_Arrs J j k u)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_e Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu (@Build_Arrs J j k u)) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fu (@Build_Arrs J j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fu (@Build_Arrs J j k u)) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu (@Build_Arrs J j k u)) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u)))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@FOb J C F k) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u))) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F k)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@FOb J C F k) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F j) (@FOb J C F k) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi j) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j)) (@FMor J C F j k u)) *)
apply (Prf_E1_law1 Thl_l_fg Elt1 Elt2).
(* Goal: @Equal (@Hom C c (@FOb J C F (@Codom J u))) (@Comp C c (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) Thl_h (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u))) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u)) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u)))) *)
(* Goal: @Equal (@Hom C c (@FOb J C F (@Codom J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u)) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u)))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
apply Ass1.
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u)) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u)))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
apply Comp_l.
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@ApNT J C (@Const J C c) F tau i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Sym.
(* Goal: @Equal (@Hom C Thl_PI_Fi (@FOb J C F k)) (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u)) (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu (@Build_Arrs J j k u)) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu (@Build_Arrs J j k u))) *)
(* Goal: @Equal (@Hom C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F k)) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@FOb J C F k) Thl_e (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi j) (@FOb J C F k) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j) (@FMor J C F j k u))) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F j) (@FOb J C F k) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi j) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi j)) (@FMor J C F j k u)) *)
exact (Thl_diag2 (Build_Arrs u)).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Ass.
Qed.
 
Definition Thl_mu := Build_Cone Thl_mu_cone_law.

 Section taudiese.

 (* construction de l'ope'ration # *)

 Variables (c : C) (tau : Cone c F).

 (* Bug trad *)

 Definition Thl_h := Pd1_diese Thl_l_Fi (c:=c) (fun i : J => tau i).

 Lemma Thl_diag3 : forall i : J, tau i =_S Thl_h o Proj1 Thl_l_Fi i.
 Proof.
(* Goal: forall i : Ob J, @Equal (@Hom C (@FOb J C (@Const J C c) i) (@FOb J C F i)) (@ApNT J C (@Const J C c) F tau i) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) Thl_h (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
 intro i; apply (Prf_pd1_law1 Thl_l_Fi (r:=c) (fun i : J => tau i) i).
 Qed.

 (* hof = hog *)
 (* hof = (IIFcodu)# (+) *)
 (* tau(codu) = h o p(codu)   Thl_diag3 *)
 (*           = h o f o p(u)  Thl_diag1 *)
 (* on a (+) par unicite' de IIFcodu *)

 (* hog = (IIFcodu)# (**) *)
 (* p(domu) o Fu = g o p(u) Thl_diag2 *)
 (* h o p(domu) o Fu = h o g o p(u) *)
 (* tau(domu)   o Fu = h o g o p(u) Thl_diag3 *)
 (* tau(codomu)      = h o f o p(u) tau est un cone *)
	
 Lemma Thl_diag4 : Thl_h o Thl_f =_S Thl_h o Thl_g.
 Proof.
 (* *) apply
        Trans
         with (Pd1_diese Thl_l_Fu (c:=c) (fun u : Arrs J => tau (Codom u))).
 apply
  (Prf_pd1_law2 (l:=Thl_l_Fu) (r:=c) (h:=fun u : Arrs J => tau (Codom u))).
(* Goal: @Product_eq C (Arrs J) Thl_k_Fu (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu) c (fun u : Arrs J => @ApNT J C (@Const J C c) F tau (@Codom J u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) *)
 unfold Product_eq in |- *; intro u.
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@ApNT J C (@Const J C c) F tau (@Codom J u)) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) Thl_PI_Fu Thl_h Thl_f) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
(* Goal: @Equal (@Hom C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu)) (@Pd1_diese C (Arrs J) Thl_k_Fu Thl_l_Fu c (fun u : Arrs J => @ApNT J C (@Const J C c) F tau (@Codom J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) *)
 (* *) apply Trans with (Thl_h o Proj1 Thl_l_Fi (Codom u)).
(* Goal: @Equal (@Hom C c (Thl_k_Fi (@Codom J u))) (@ApNT J C (@Const J C c) F tau (@Codom J u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Codom J u)) Thl_h (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Codom J u))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi (@Codom J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Codom J u)) Thl_h (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Codom J u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) Thl_PI_Fu Thl_h Thl_f) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
(* Goal: @Equal (@Hom C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu)) (@Pd1_diese C (Arrs J) Thl_k_Fu Thl_l_Fu c (fun u : Arrs J => @ApNT J C (@Const J C c) F tau (@Codom J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) *)
 apply (Thl_diag3 (Codom u)).
(* Goal: @Equal (@Hom C c (Thl_k_Fi (@Codom J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Codom J u)) Thl_h (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Codom J u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) Thl_PI_Fu Thl_h Thl_f) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
(* Goal: @Equal (@Hom C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu)) (@Pd1_diese C (Arrs J) Thl_k_Fu Thl_l_Fu c (fun u : Arrs J => @ApNT J C (@Const J C c) F tau (@Codom J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) *)
 (* *) apply Trans with (Thl_h o Thl_f o Proj1 Thl_l_Fu u).
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u)) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u)))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 apply Comp_l.
(* Goal: @Equal (@Hom C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Codom J u)) (@Comp C Thl_PI_Fi Thl_PI_Fu (Thl_k_Fu u) Thl_f (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C Thl_PI_Fi Thl_PI_Fu (Thl_k_Fu u) Thl_f (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) Thl_PI_Fu Thl_h Thl_f) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
(* Goal: @Equal (@Hom C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu)) (@Pd1_diese C (Arrs J) Thl_k_Fu Thl_l_Fu c (fun u : Arrs J => @ApNT J C (@Const J C c) F tau (@Codom J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) *)
 apply (Thl_diag1 u).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
 apply Ass.
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@ApNT J C (@Const J C c) F tau i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
 apply Sym.
 apply
  (Prf_pd1_law2 (l:=Thl_l_Fu) (r:=c) (h:=fun u : Arrs J => tau (Codom u))).
(* Goal: @Product_eq C (Arrs J) Thl_k_Fu (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu) c (fun u : Arrs J => @ApNT J C (@Const J C c) F tau (@Codom J u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) *)
 unfold Product_eq in |- *; intro u.
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@ApNT J C (@Const J C c) F tau (@Codom J u)) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 (* *) apply Trans with (tau (Dom u) o FMor F (Arrow u)).
(* Goal: @Equal (@Hom C (@FOb J C (@Const J C c) (@Dom J u)) (@FOb J C F (@Codom J u))) (@ApNT J C (@Const J C c) F tau (@Codom J u)) (@Comp C (@FOb J C (@Const J C c) (@Dom J u)) (@FOb J C F (@Dom J u)) (@FOb J C F (@Codom J u)) (@ApNT J C (@Const J C c) F tau (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u))) *)
(* Goal: @Equal (@Hom C (@FOb J C (@Const J C c) (@Dom J u)) (@FOb J C F (@Codom J u))) (@Comp C (@FOb J C (@Const J C c) (@Dom J u)) (@FOb J C F (@Dom J u)) (@FOb J C F (@Codom J u)) (@ApNT J C (@Const J C c) F tau (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 apply (Eq_cone tau (Arrow u)).
(* Goal: @Equal (@Hom C (@FOb J C (@Const J C c) (@Dom J u)) (@FOb J C F (@Codom J u))) (@Comp C (@FOb J C (@Const J C c) (@Dom J u)) (@FOb J C F (@Dom J u)) (@FOb J C F (@Codom J u)) (@ApNT J C (@Const J C c) F tau (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 (* *) apply Trans with ((Thl_h o Proj1 Thl_l_Fi (Dom u)) o FMor F (Arrow u)).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c Thl_PI_Fi (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Thl_diese c tau) Thl_e) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) (@ApNT J C (@Const J C c) F tau i) *)
 apply Comp_r.
(* Goal: @Equal (@Hom C c (Thl_k_Fi (@Dom J u))) (@ApNT J C (@Const J C c) F tau (@Dom J u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) Thl_h (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u))) *)
(* Goal: @Equal (@Hom C c (@FOb J C F (@Codom J u))) (@Comp C c (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) Thl_h (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u))) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 apply (Thl_diag3 (Dom u)).
(* Goal: @Equal (@Hom C c (@FOb J C F (@Codom J u))) (@Comp C c (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) Thl_h (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u))) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 (* *) apply Trans with (Thl_h o Proj1 Thl_l_Fi (Dom u) o FMor F (Arrow u)).
(* Goal: @Equal (@Hom C c (@FOb J C F (@Codom J u))) (@Comp C c (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) Thl_h (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u))) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u)) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u)))) *)
(* Goal: @Equal (@Hom C c (@FOb J C F (@Codom J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u)) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u)))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 apply Ass1.
(* Goal: @Equal (@Hom C c (@FOb J C F (@Codom J u))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u)) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u)))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 (* *) apply Trans with (Thl_h o Thl_g o Proj1 Thl_l_Fu u).
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@FOb J C F (@Codom J u)) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u)))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 apply Comp_l.
(* Goal: @Equal (@Hom C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u)) (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi (@Dom J u)) (@FOb J C F (@Codom J u)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi (@Dom J u)) (@FMor J C F (@Dom J u) (@Codom J u) (@Arrow J u))) (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fu u)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fu u) Thl_h (@Comp C (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) Thl_g (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u))) (@Comp C c (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) (Thl_k_Fu u) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (@Pi1 C (Arrs J) Thl_k_Fu Thl_l_Fu) Thl_h Thl_g) (@Proj1 C (Arrs J) Thl_k_Fu Thl_l_Fu u)) *)
 apply (Thl_diag2 u).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
 apply Ass.
 Qed.

 (* posons tau# = h# *)

 Definition Thl_diese := E1_diese Thl_l_fg (Prf_law1_fg Thl_diag4).

 End taudiese.

(* universalite' *)

Lemma Thl_limit1 : Limit_law1 Thl_mu Thl_diese.
Proof.
(* Goal: @Limit_law1 J C F (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_mu Thl_diese *)
unfold Limit_law1, Limit_eq in |- *; intros c tau; simpl in |- *; intro i.
(* Goal: @Equal (@Hom C c (@FOb J C F i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F i) (@Thl_diese c tau) (Thl_mu_tau i)) (@ApNT J C (@Const J C c) F tau i) *)
(* *) apply Trans with ((Thl_diese tau o Thl_e) o Proj1 Thl_l_Fi i).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F i) (@Thl_diese c tau) (Thl_mu_tau i)) (@Comp C c Thl_PI_Fi (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Thl_diese c tau) Thl_e) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c Thl_PI_Fi (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Thl_diese c tau) Thl_e) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) (@ApNT J C (@Const J C c) F tau i) *)
(* *) apply Trans with (Thl_diese tau o Thl_e o Proj1 Thl_l_Fi i).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (@FOb J C F i) (@Thl_diese c tau) (Thl_mu_tau i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) (@Thl_diese c tau) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) (@Thl_diese c tau) (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c Thl_PI_Fi (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Thl_diese c tau) Thl_e) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c Thl_PI_Fi (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Thl_diese c tau) Thl_e) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) (@ApNT J C (@Const J C c) F tau i) *)
apply Refl.
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Ass.
(* *) apply
       Trans
        with
          (Pd1_diese Thl_l_Fi (c:=c) (fun i : J => tau i) o Proj1 Thl_l_Fi i).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c Thl_PI_Fi (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Thl_diese c tau) Thl_e) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) (@ApNT J C (@Const J C c) F tau i) *)
apply Comp_r.
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@ApNT J C (@Const J C c) F tau i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Sym.
(* Goal: @Equal (@Hom C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi)) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (@Thl_diese c tau) Thl_e) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) (@ApNT J C (@Const J C c) F tau i) *)
apply (Prf_E1_law2 Thl_l_fg (Prf_law1_fg (Thl_diag4 tau))).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@ApNT J C (@Const J C c) F tau i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Sym.
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@ApNT J C (@Const J C c) F tau i) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply (Thl_diag3 tau i).
Qed.

(* hyp: t o mu(i) = tau(i) *)
(* s` prouver: t = tau# (=h#) *)
(* par universalite' de e, revient a` prouver:
   h = t o e 
   or, (rappel) h =def (i|->tau(i))# pour ||Fi
   donc par universalite' de IIFi, revient a` prouver:
   qq i:Ob(J). tau(i) = t o e o p(i) 
   vrai par hyp car mu(i) =def e o p(i) *)

Lemma Thl_limit2 : Limit_law2 Thl_mu Thl_diese.
Proof.
(* Goal: @Limit_law2 J C F (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_mu Thl_diese *)
unfold Limit_law2, Limit_eq in |- *; intros c tau t H.
(* Goal: @Equal (@Hom C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) t (@Thl_diese c tau) *)
unfold Thl_diese in |- *; apply (Prf_E1_law3 (l:=Thl_l_fg)).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@ApNT J C (@Const J C c) F tau i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Sym.
(* Goal: @Equal (@Hom C c Thl_PI_Fi) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Thl_h c tau) *)
unfold Thl_h in |- *.
(* Goal: @Equal (@Hom C c Thl_PI_Fi) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Pd1_diese C (Ob J) Thl_k_Fi Thl_l_Fi c (fun i : Ob J => @ApNT J C (@Const J C c) F tau i)) *)
apply (Prf_pd1_law2 (l:=Thl_l_Fi)); unfold Product_eq in |- *; intro i.
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@ApNT J C (@Const J C c) F tau i) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Trans with (t o Thl_e o Proj1 Thl_l_Fi i).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@ApNT J C (@Const J C c) F tau i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Sym.
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@ApNT J C (@Const J C c) F tau i) *)
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
exact (H i).
(* Goal: @Equal (@Hom C c (Thl_k_Fi i)) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) (Thl_k_Fi i) t (@Comp C (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi (Thl_k_Fi i) Thl_e (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i))) (@Comp C c (@Pi1 C (Ob J) Thl_k_Fi Thl_l_Fi) (Thl_k_Fi i) (@Comp C c (@E1_ob C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg) Thl_PI_Fi t (@E1_mor C Thl_PI_Fi Thl_PI_Fu TwoElts (@K_fg C Thl_PI_Fi Thl_PI_Fu Thl_f Thl_g) Thl_l_fg)) (@Proj1 C (Ob J) Thl_k_Fi Thl_l_Fi i)) *)
apply Ass.
Qed.

Definition Thl_islimit := Build_IsLimit Thl_limit1 Thl_limit2.

Definition Thl_limit := Build_Limit Thl_islimit.

End thl.







