(* 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        *)
(*****************************************************************************)
(*									     *)
(*	   A sufficient condition for a Comma to be Complete        	     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

Require Export Pres_Limits.
Require Export Comma_proj.

Set Implicit Arguments.
Unset Strict Implicit.

Section comma_complete.

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

Hypothesis A_comp_for_J : forall F : Functor J A, Limit F.
Hypothesis G_pres_JA : forall F : Functor J A, Preserves_limits F G.

Variables (x : X) (F : Functor J (Comma G x)).

Let F' := F o_F Comma_proj G x.

Let l_F' := A_comp_for_J F'.

Let l_GF' := G_pres_JA l_F'.

(* construction d'un cone Delta(x)->F' o G *)

Definition Tc_tau (i : J) := Mor_com_ob (F i).

Lemma Tc_tau_cone_law : Cone_law (F:=F' o_F G) Tc_tau.
Proof.
(* Goal: @Cone_law J A (@Ob_com_ob A X G x axf) F' Tc_t_tau *)
unfold Cone_law in |- *; intros i j g.
(* Goal: @Equal (@Hom X x (@FOb J X (@Comp_Functor J A X F' G) j)) (Tc_tau j) (@Comp X x (@FOb J X (@Comp_Functor J A X F' G) i) (@FOb J X (@Comp_Functor J A X F' G) j) (Tc_tau i) (@FMor J X (@Comp_Functor J A X F' G) i j g)) *)
apply (Prf_com_law (FMor F g)).
Qed.

Definition Tc_cone := Build_Cone Tc_tau_cone_law.

(* limite objet pour F *)

Canonical Structure Tc_limF := Build_Com_ob (Lim_diese l_GF' Tc_cone).

(* limiting cone pour F *)

Lemma Tc_limconeF_tau_com_law :
 forall i : J, Com_law (axf:=Tc_limF) (bxg:=F i) (Limiting_cone l_F' i).
Proof.
(* Goal: forall i : Ob J, @Com_law A X G x Tc_limF (@FOb J (@Comma A X G x) F i) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i) *)
unfold Com_law in |- *; intro i.
(* Goal: @Equal (@Hom X x (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)))) (@Mor_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x Tc_limF)) (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i))) (@Mor_com_ob A X G x Tc_limF) (@FMor A X G (@Ob_com_ob A X G x Tc_limF) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i))) *)
apply Sym; exact (Prf_limit1 l_GF' Tc_cone i).
Qed.

Canonical Structure Tc_limconeF_tau (i : J) :=
  Build_Com_arrow (Tc_limconeF_tau_com_law i).

Lemma Tc_limconeF_cone_law : Cone_law Tc_limconeF_tau.
Proof.
(* Goal: @Cone_law J (@Comma A X G x) Tc_limF F Tc_limconeF_tau *)
unfold Cone_law in |- *; simpl in |- *.
(* Goal: forall (i j : Ob J) (g : Carrier (@Hom J i j)), @Equal_com_arrow A X G x Tc_limF (@FOb J (@Comma A X G x) F j) (Tc_limconeF_tau j) (@Comp (@Comma A X G x) Tc_limF (@FOb J (@Comma A X G x) F i) (@FOb J (@Comma A X G x) F j) (Tc_limconeF_tau i) (@FMor J (@Comma A X G x) F i j g)) *)
intros i j g.
(* Goal: @Equal_com_arrow A X G x Tc_limF (@FOb J (@Comma A X G x) F j) (Tc_limconeF_tau j) (@Comp (@Comma A X G x) Tc_limF (@FOb J (@Comma A X G x) F i) (@FOb J (@Comma A X G x) F j) (Tc_limconeF_tau i) (@FMor J (@Comma A X G x) F i j g)) *)
unfold Equal_com_arrow in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (@Lim J A F' l_F') (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F j))) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') j) (@Comp_com_mor A X G x Tc_limF (@FOb J (@Comma A X G x) F i) (@FOb J (@Comma A X G x) F j) (Tc_limconeF_tau i) (@FMor J (@Comma A X G x) F i j g)) *)
unfold Comp_com_mor in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (@Lim J A F' l_F') (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F j))) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') j) (@Comp A (@Lim J A F' l_F') (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F j)) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i) (@Mor_com_arrow A X G x (@FOb J (@Comma A X G x) F i) (@FOb J (@Comma A X G x) F j) (@FMor J (@Comma A X G x) F i j g))) *)
apply (Eq_cone (Limiting_cone l_F') g).
Qed.

Definition Tc_limconeF := Build_Cone Tc_limconeF_cone_law.

(* operation # *)

 Section ctdiese.
  
 Variables (axf : Comma G x) (t : Cone axf F).

 Definition Tc_t_tau (i : J) := Mor_com_arrow (t i).

 Lemma Tc_t_tau_cone_law : Cone_law (c:=Ob_com_ob axf) (F:=F') Tc_t_tau.
 Proof.
(* Goal: @Cone_law J A (@Ob_com_ob A X G x axf) F' Tc_t_tau *)
 unfold Cone_law in |- *; intros i j g.
(* Goal: @Equal (@Hom A (@Ob_com_ob A X G x axf) (@FOb J A F' j)) (Tc_t_tau j) (@Comp A (@Ob_com_ob A X G x axf) (@FOb J A F' i) (@FOb J A F' j) (Tc_t_tau i) (@FMor J A F' i j g)) *)
 generalize (Eq_cone t g).
(* Goal: forall _ : @Equal (@Hom (@Comma A X G x) axf (@FOb J (@Comma A X G x) F j)) (@ApNT J (@Comma A X G x) (@Const J (@Comma A X G x) axf) F t j) (@Comp (@Comma A X G x) axf (@FOb J (@Comma A X G x) F i) (@FOb J (@Comma A X G x) F j) (@ApNT J (@Comma A X G x) (@Const J (@Comma A X G x) axf) F t i) (@FMor J (@Comma A X G x) F i j g)), @Equal (@Hom A (@Ob_com_ob A X G x axf) (@FOb J A F' j)) (Tc_t_tau j) (@Comp A (@Ob_com_ob A X G x axf) (@FOb J A F' i) (@FOb J A F' j) (Tc_t_tau i) (@FMor J A F' i j g)) *)
 intro H.
(* Goal: @Equal (@Hom A (@Ob_com_ob A X G x axf) (@FOb J A F' j)) (Tc_t_tau j) (@Comp A (@Ob_com_ob A X G x axf) (@FOb J A F' i) (@FOb J A F' j) (Tc_t_tau i) (@FMor J A F' i j g)) *)
 apply Trans with (FMor (Comma_proj G x) (t i o FMor F g)).
(* Goal: @Equal (@Hom A (@FOb (@Comma A X G x) A (@Comma_proj A X G x) (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@FOb (@Comma A X G x) A (@Comma_proj A X G x) (@FOb J (@Comma A X G x) F j))) (Tc_t_tau j) (@FMor (@Comma A X G x) A (@Comma_proj A X G x) (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i) (@FOb J (@Comma A X G x) F j) (@Comp (@Comma A X G x) (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i) (@FOb J (@Comma A X G x) F i) (@FOb J (@Comma A X G x) F j) (@ApNT J (@Comma A X G x) (@Const J (@Comma A X G x) axf) F t i) (@FMor J (@Comma A X G x) F i j g))) *)
(* Goal: @Equal (@Hom A (@FOb (@Comma A X G x) A (@Comma_proj A X G x) (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@FOb (@Comma A X G x) A (@Comma_proj A X G x) (@FOb J (@Comma A X G x) F j))) (@FMor (@Comma A X G x) A (@Comma_proj A X G x) (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i) (@FOb J (@Comma A X G x) F j) (@Comp (@Comma A X G x) (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i) (@FOb J (@Comma A X G x) F i) (@FOb J (@Comma A X G x) F j) (@ApNT J (@Comma A X G x) (@Const J (@Comma A X G x) axf) F t i) (@FMor J (@Comma A X G x) F i j g))) (@Comp A (@Ob_com_ob A X G x axf) (@FOb J A F' i) (@FOb J A F' j) (Tc_t_tau i) (@FMor J A F' i j g)) *)
 exact (Pres (FMap (Comma_proj G x) axf (F j)) H).
(* Goal: @Equal (@Hom A (@FOb (@Comma A X G x) A (@Comma_proj A X G x) (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@FOb (@Comma A X G x) A (@Comma_proj A X G x) (@FOb J (@Comma A X G x) F j))) (@FMor (@Comma A X G x) A (@Comma_proj A X G x) (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i) (@FOb J (@Comma A X G x) F j) (@Comp (@Comma A X G x) (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i) (@FOb J (@Comma A X G x) F i) (@FOb J (@Comma A X G x) F j) (@ApNT J (@Comma A X G x) (@Const J (@Comma A X G x) axf) F t i) (@FMor J (@Comma A X G x) F i j g))) (@Comp A (@Ob_com_ob A X G x axf) (@FOb J A F' i) (@FOb J A F' j) (Tc_t_tau i) (@FMor J A F' i j g)) *)
 exact (Prf_Fcomp_law (Comma_proj G x) (t i) (FMor F g)).
 Qed.

 Definition Tc_t_cone := Build_Cone Tc_t_tau_cone_law.

 Lemma Tc_t_cone_com_law :
  Com_law (axf:=axf) (bxg:=Tc_limF) (Lim_diese l_F' Tc_t_cone).
 Proof.
(* Goal: @Com_law A X G x axf Tc_limF (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone) *)
 unfold Com_law in |- *; unfold Mor_com_ob at 1 in |- *; simpl in |- *.
(* Goal: @Equal (@Hom X x (@FOb A X G (@Lim J A F' l_F'))) (@Lim_diese J X (@Comp_Functor J A X F' G) (@FOb A X G (@Lim J A F' l_F')) (@Comp_cone J A X (@Lim J A F' l_F') F' (@Limiting_cone J A F' l_F') G) l_GF' x Tc_cone) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Lim J A F' l_F')) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone))) *)
 apply Sym; apply (Prf_limit2 l_GF').
(* Goal: @Limit_eq J X (@Comp_Functor J A X F' G) (@FOb A X G (@Lim J A F' l_F')) (@Comp_cone J A X (@Lim J A F' l_F') F' (@Limiting_cone J A F' l_F') G) x Tc_cone (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Lim J A F' l_F')) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone))) *)
 unfold Limit_eq in |- *; simpl in |- *; intro i.
 apply
  Trans
   with
     (Mor_com_ob axf
      o FMor G (Lim_diese l_F' Tc_t_cone) o FMor G (Limiting_cone l_F' i)).
(* Goal: @Equal (@Hom X x (@FOb A X G (@FOb J A F' i))) (@Comp X x (@FOb A X G (@Lim J A F' l_F')) (@Comp_FOb J A X F' G i) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Lim J A F' l_F')) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone))) (@Comp_cone_tau J A X (@Lim J A F' l_F') F' (@Limiting_cone J A F' l_F') G i)) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@FOb J A F' i)) (@Mor_com_ob A X G x axf) (@Comp X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Lim J A F' l_F')) (@FOb A X G (@FOb J A F' i)) (@FMor A X G (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone)) (@FMor A X G (@FOb J A (@Const J A (@Lim J A F' l_F')) i) (@FOb J A F' i) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i)))) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (@FOb J A F' i))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@FOb J A F' i)) (@Mor_com_ob A X G x axf) (@Comp X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Lim J A F' l_F')) (@FOb A X G (@FOb J A F' i)) (@FMor A X G (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone)) (@FMor A X G (@FOb J A (@Const J A (@Lim J A F' l_F')) i) (@FOb J A F' i) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i)))) (Tc_tau i) *)
 apply Ass1.
(* Goal: @Equal (@Hom X x (@FOb A X G (@FOb J A F' i))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@FOb J A F' i)) (@Mor_com_ob A X G x axf) (@Comp X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Lim J A F' l_F')) (@FOb A X G (@FOb J A F' i)) (@FMor A X G (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone)) (@FMor A X G (@FOb J A (@Const J A (@Lim J A F' l_F')) i) (@FOb J A F' i) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i)))) (Tc_tau i) *)
 apply Trans with (Mor_com_ob axf o FMor G (Tc_t_tau i)).
(* Goal: @Equal (@Hom X x (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@FOb J A F' i)) (@Mor_com_ob A X G x axf) (@Comp X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Lim J A F' l_F')) (@FOb A X G (@FOb J A F' i)) (@FMor A X G (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone)) (@FMor A X G (@FOb J A (@Const J A (@Lim J A F' l_F')) i) (@FOb J A F' i) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i)))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i))) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i))) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i))) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i))) (Tc_tau i) *)
 apply Comp_l.
(* Goal: @Equal (@Hom X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)))) (@Comp X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Lim J A F' l_F')) (@FOb A X G (@FOb J A F' i)) (@FMor A X G (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone)) (@FMor A X G (@FOb J A (@Const J A (@Lim J A F' l_F')) i) (@FOb J A F' i) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i))) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i)) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i))) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i))) (Tc_tau i) *)
 apply Trans with (FMor G (Lim_diese l_F' Tc_t_cone o Limiting_cone l_F' i)).
(* Goal: @Equal (@Hom X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@FOb J A F' i))) (@Comp X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Lim J A F' l_F')) (@FOb A X G (@FOb J A F' i)) (@FMor A X G (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone)) (@FMor A X G (@FOb J A (@Const J A (@Lim J A F' l_F')) i) (@FOb J A F' i) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i))) (@FMor A X G (@Ob_com_ob A X G x axf) (@FOb J A F' i) (@Comp A (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@FOb J A F' i) (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i))) *)
(* Goal: @Equal (@Hom X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@FOb J A F' i))) (@FMor A X G (@Ob_com_ob A X G x axf) (@FOb J A F' i) (@Comp A (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@FOb J A F' i) (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i))) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i)) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i))) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i))) (Tc_tau i) *)
 apply FComp1.
(* Goal: @Equal (@Hom X (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@FOb J A F' i))) (@FMor A X G (@Ob_com_ob A X G x axf) (@FOb J A F' i) (@Comp A (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@FOb J A F' i) (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i))) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i)) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i))) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i))) (Tc_tau i) *)
 unfold FMor in |- *; apply (Pres (FMap G (Ob_com_ob axf) (Ob_com_ob (F i)))). 
(* Goal: @Equal (@Hom A (@Ob_com_ob A X G x axf) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i))) (@Comp A (@Ob_com_ob A X G x axf) (@Lim J A F' l_F') (@FOb J A F' i) (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) Tc_t_cone) (@ApNT J A (@Const J A (@Lim J A F' l_F')) F' (@Limiting_cone J A F' l_F') i)) (Tc_t_tau i) *)
(* Goal: @Equal (@Hom X x (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i))) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i))) (Tc_tau i) *)
 apply (Prf_limit1 l_F' Tc_t_cone i).
(* Goal: @Equal (@Hom X x (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)))) (@Comp X x (@FOb A X G (@Ob_com_ob A X G x axf)) (@FOb A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i))) (@Mor_com_ob A X G x axf) (@FMor A X G (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) (@Const J (@Comma A X G x) axf) i)) (@Ob_com_ob A X G x (@FOb J (@Comma A X G x) F i)) (Tc_t_tau i))) (Tc_tau i) *)
 apply Sym; apply (Prf_com_law (t i)).
 Qed.

 Canonical Structure Tc_diese := Build_Com_arrow Tc_t_cone_com_law.

 End ctdiese.
  

Lemma Tc_UA_law1 : Limit_law1 Tc_limconeF Tc_diese. 
Proof.
(* Goal: @Limit_law1 J (@Comma A X G x) F Tc_limF Tc_limconeF Tc_diese *)
unfold Limit_law1, Limit_eq in |- *; intros axf t.
(* Goal: forall i : Ob J, @Equal (@Hom (@Comma A X G x) axf (@FOb J (@Comma A X G x) F i)) (@Comp (@Comma A X G x) axf Tc_limF (@FOb J (@Comma A X G x) F i) (@Tc_diese axf t) (@ApNT J (@Comma A X G x) (@Const J (@Comma A X G x) Tc_limF) F Tc_limconeF i)) (@ApNT J (@Comma A X G x) (@Const J (@Comma A X G x) axf) F t i) *)
intro i; apply (Prf_limit1 l_F' (Tc_t_cone t) i).
Qed.

Lemma Tc_UA_law2 : Limit_law2 Tc_limconeF Tc_diese. 
Proof.
(* Goal: @Limit_law2 J (@Comma A X G x) F Tc_limF Tc_limconeF Tc_diese *)
unfold Limit_law2, Limit_eq in |- *; intros axf t g.
intro H; unfold Tc_diese in |- *; simpl in |- *;
(* Goal: @Equal_com_arrow A X G x Tc_limF (@FOb J (@Comma A X G x) F j) (Tc_limconeF_tau j) (@Comp (@Comma A X G x) Tc_limF (@FOb J (@Comma A X G x) F i) (@FOb J (@Comma A X G x) F j) (Tc_limconeF_tau i) (@FMor J (@Comma A X G x) F i j g)) *)
 unfold Equal_com_arrow in |- *; simpl in |- *.
(* Goal: @Equal (@Hom A (@Ob_com_ob A X G x axf) (@Lim J A F' l_F')) (@Mor_com_arrow A X G x axf Tc_limF g) (@Lim_diese J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Prf_Islimit J A F' l_F') (@Ob_com_ob A X G x axf) (@Tc_t_cone axf t)) *)
apply (Prf_limit2 l_F').
(* Goal: @Limit_eq J A F' (@Lim J A F' l_F') (@Limiting_cone J A F' l_F') (@Ob_com_ob A X G x axf) (@Tc_t_cone axf t) (@Mor_com_arrow A X G x axf Tc_limF g) *)
exact H.
Qed.

Definition Comma_l_F := Build_IsLimit Tc_UA_law1 Tc_UA_law2. 

Definition Comma_l_F1 := Build_Limit Comma_l_F.

End comma_complete.


Lemma Comma_complete :
 forall (X A : Category) (G : Functor A X),
 Complete A -> Continuous G -> forall x : X, Complete (Comma G x).
Proof.
(* Goal: forall (X A : Category) (G : Functor A X) (_ : Complete A) (_ : @Continuous A X G) (x : Ob X), Complete (@Comma A X G x) *)
intros X A G cA cG x.
(* Goal: Complete (@Comma A X G x) *)
unfold Complete in |- *; intros J F.
(* Goal: @Limit J (@Comma A X G x) F *)
exact (Comma_l_F1 (cA J) (cG J) F).
Defined.


        