(* 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 Functor which is a Right Adjoint is Continuous		     *)
(*                      (part of Freyd's Theorem)             		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

Require Export Adj_UA.
Require Export Pres_Limits.

Set Implicit Arguments.
Unset Strict Implicit.

(* *)

Section ladj_pres.

Variables (C D : Category) (G : Functor C D) (la : LeftAdj G) 
  (J : Category) (H : Functor J C) (l : Limit H).

(* pour tout d : D et tau : Delta(d) -> T o G,
   sigma(i) = phi_1<d,Ti>(tau(i)) *)

 Section lp_diese.

 Variables (d : D) (tau : Cone d (H o_F G)).

 Definition Lp_sigma_tau (i : J) := ApAphi_inv la (tau i:d --> G (H i)).

 (* sigma est en fait un cone(T,Fd) ou` F est l'adjoint de G *)

 Lemma Lp_sigma_tau_cone_law : Cone_law Lp_sigma_tau.
 Proof.
(* Goal: @Cone_law J C (@FOb D C (@Adjoint C D G la) d) H Lp_sigma_tau *)
 unfold Cone_law, Lp_sigma_tau in |- *.
(* Goal: forall (i j : Ob J) (g : Carrier (@Hom J i j)), @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H j)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H j) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau j)) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i) (@FOb J C H j) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i)) (@FMor J C H i j g)) *)
 intros i j g.
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H j)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H j) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau j)) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i) (@FOb J C H j) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i)) (@FMor J C H i j g)) *)
 (* *) apply Trans with (ApAphi_inv la (tau i o FMor G (FMor H g))).
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) (@FOb J D (@Const J D d) i)) (@FOb J C H j)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H j) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau j)) (@ApAphi_inv C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H j) (@Adj_l C D G la) (@Comp D (@FOb J D (@Const J D d) i) (@FOb J D (@Comp_Functor J C D H G) i) (@FOb C D G (@FOb J C H j)) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) (@FMor C D G (@FOb J C H i) (@FOb J C H j) (@FMor J C H i j g)))) *)
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) (@FOb J D (@Const J D d) i)) (@FOb J C H j)) (@ApAphi_inv C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H j) (@Adj_l C D G la) (@Comp D (@FOb J D (@Const J D d) i) (@FOb J D (@Comp_Functor J C D H G) i) (@FOb C D G (@FOb J C H j)) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) (@FMor C D G (@FOb J C H i) (@FOb J C H j) (@FMor J C H i j g)))) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i) (@FOb J C H j) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i)) (@FMor J C H i j g)) *)
 apply Aphi_invPres.
(* Goal: @Equal (@Hom D (@FOb J D (@Const J D d) i) (@FOb C D G (@FOb J C H j))) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau j) (@Comp D (@FOb J D (@Const J D d) i) (@FOb J D (@Comp_Functor J C D H G) i) (@FOb C D G (@FOb J C H j)) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) (@FMor C D G (@FOb J C H i) (@FOb J C H j) (@FMor J C H i j g))) *)
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) (@FOb J D (@Const J D d) i)) (@FOb J C H j)) (@ApAphi_inv C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H j) (@Adj_l C D G la) (@Comp D (@FOb J D (@Const J D d) i) (@FOb J D (@Comp_Functor J C D H G) i) (@FOb C D G (@FOb J C H j)) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) (@FMor C D G (@FOb J C H i) (@FOb J C H j) (@FMor J C H i j g)))) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i) (@FOb J C H j) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i)) (@FMor J C H i j g)) *)
 apply (Eq_cone tau g).
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) (@FOb J D (@Const J D d) i)) (@FOb J C H j)) (@ApAphi_inv C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H j) (@Adj_l C D G la) (@Comp D (@FOb J D (@Const J D d) i) (@FOb J D (@Comp_Functor J C D H G) i) (@FOb C D G (@FOb J C H j)) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) (@FMor C D G (@FOb J C H i) (@FOb J C H j) (@FMor J C H i j g)))) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i) (@FOb J C H j) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i)) (@FMor J C H i j g)) *)
 apply (Adj_eq5 la (FMor H g) (tau i)).
 Qed.

 Definition Lp_sigma := Build_Cone Lp_sigma_tau_cone_law.

 (* construction de tau# *)
 (* tau# = phi<d,limT>(sigma#) *)

 Definition Lp_diese : d --> G (Lim l) := ApAphi la (Lim_diese l Lp_sigma).
 
 End lp_diese.
 
Lemma Lp_coUAlaw1 : Limit_law1 (Limiting_cone l o_C G) Lp_diese.
Proof.
(* Goal: @Limit_law1 J D (@Comp_Functor J C D H G) (@FOb C D G (@Lim J C H l)) (@Comp_cone J C D (@Lim J C H l) H (@Limiting_cone J C H l) G) Lp_diese *)
unfold Limit_law1, Limit_eq in |- *; simpl in |- *; intros d tau i.
(* Goal: forall _ : forall i : Ob J, @Equal (@Hom D d (@Comp_FOb J C D H G i)) (@Comp D d (@FOb C D G (@Lim J C H l)) (@Comp_FOb J C D H G i) t (@Comp_cone_tau J C D (@Lim J C H l) H (@Limiting_cone J C H l) G i)) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i), @Equal (@Hom D d (@FOb C D G (@Lim J C H l))) t (@Lp_diese d tau) *)
unfold Comp_cone_tau, Lp_diese in |- *.
(* *) apply
       Trans
        with (ApAphi la (Lim_diese l (Lp_sigma tau) o Limiting_cone l i)).
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@ApAphi_inv C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) t) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp D d (@FOb C D G (@Lim J C H l)) (@FOb C D G (@FOb J C H i)) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)))) *)
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp D d (@FOb C D G (@Lim J C H l)) (@FOb C D G (@FOb J C H i)) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)))) (@ApNT J C (@Const J C (@FOb D C (@Adjoint C D G la) d)) H (@Lp_sigma d tau) i) *)
apply Sym.
(* Goal: @Equal (@Hom D d (@FOb C D G (@FOb J C H i))) (@ApAphi C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau)) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i))) (@Comp D d (@FOb C D G (@Lim J C H l)) (@Comp_FOb J C D H G i) (@ApAphi C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau))) (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i))) *)
(* Goal: @Equal (@Hom D d (@FOb C D G (@FOb J C H i))) (@ApAphi C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau)) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i))) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) *)
apply (Adj_eq3 la (Limiting_cone l i) (Lim_diese l (Lp_sigma tau))).
(* Goal: @Equal (@Hom D d (@FOb C D G (@FOb J C H i))) (@ApAphi C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau)) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i))) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) *)
(* *) apply Trans with (ApAphi la (ApAphi_inv (c:=H i) la (tau i))).
(* Goal: @Equal (@Hom D (@FOb J D (@Const J D d) i) (@FOb C D G (@FOb J C H i))) (@ApAphi C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau)) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i))) (@ApAphi C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H i) (@Adj_l C D G la) (@ApAphi_inv C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i))) *)
(* Goal: @Equal (@Hom D (@FOb J D (@Const J D d) i) (@FOb C D G (@FOb J C H i))) (@ApAphi C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H i) (@Adj_l C D G la) (@ApAphi_inv C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i))) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) *)
unfold Comp_FOb in |- *; apply AphiPres.
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) (@FOb J D (@Const J D d) i)) (@FOb J C H i)) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau)) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)) (@ApAphi_inv C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i)) *)
(* Goal: @Equal (@Hom D (@FOb J D (@Const J D d) i) (@FOb C D G (@FOb J C H i))) (@ApAphi C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H i) (@Adj_l C D G la) (@ApAphi_inv C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i))) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) *)
apply (Prf_limit1 l (Lp_sigma tau) i).
(* Goal: @Equal (@Hom D (@FOb J D (@Const J D d) i) (@FOb C D G (@FOb J C H i))) (@ApAphi C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H i) (@Adj_l C D G la) (@ApAphi_inv C D (@Adjoint C D G la) G (@FOb J D (@Const J D d) i) (@FOb J C H i) (@Adj_l C D G la) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i))) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i) *)
apply (Idl_inv (NTa_areIso la (Build_POb1 d (H i))) (tau i)).
Qed.

Lemma Lp_coUAlaw2 : Limit_law2 (Limiting_cone l o_C G) Lp_diese.
Proof.
(* Goal: @Limit_law2 J D (@Comp_Functor J C D H G) (@FOb C D G (@Lim J C H l)) (@Comp_cone J C D (@Lim J C H l) H (@Limiting_cone J C H l) G) Lp_diese *)
unfold Limit_law2, Limit_eq in |- *; simpl in |- *; intros d tau t.
(* Goal: forall _ : forall i : Ob J, @Equal (@Hom D d (@Comp_FOb J C D H G i)) (@Comp D d (@FOb C D G (@Lim J C H l)) (@Comp_FOb J C D H G i) t (@Comp_cone_tau J C D (@Lim J C H l) H (@Limiting_cone J C H l) G i)) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i), @Equal (@Hom D d (@FOb C D G (@Lim J C H l))) t (@Lp_diese d tau) *)
unfold Comp_cone_tau, Lp_diese in |- *.
(* Goal: forall _ : forall i : Ob J, @Equal (@Hom D d (@Comp_FOb J C D H G i)) (@Comp D d (@FOb C D G (@Lim J C H l)) (@Comp_FOb J C D H G i) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i))) (@ApNT J D (@Const J D d) (@Comp_Functor J C D H G) tau i), @Equal (@Hom D d (@FOb C D G (@Lim J C H l))) t (@ApAphi C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau))) *)
intro H'.
(* Goal: @Equal (@Hom D d (@FOb C D G (@Lim J C H l))) t (@ApAphi C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau))) *)
(* *) apply Trans with (ApAphi la (ApAphi_inv la t)).
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@ApAphi_inv C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) t) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp D d (@FOb C D G (@Lim J C H l)) (@FOb C D G (@FOb J C H i)) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)))) *)
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp D d (@FOb C D G (@Lim J C H l)) (@FOb C D G (@FOb J C H i)) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)))) (@ApNT J C (@Const J C (@FOb D C (@Adjoint C D G la) d)) H (@Lp_sigma d tau) i) *)
apply Sym.
(* Goal: @Equal (@Hom D d (@FOb C D G (@Lim J C H l))) (@ApAphi C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) (@ApAphi_inv C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) t)) t *)
(* Goal: @Equal (@Hom D d (@FOb C D G (@Lim J C H l))) (@ApAphi C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) (@ApAphi_inv C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) t)) (@ApAphi C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau))) *)
apply (Idl_inv (NTa_areIso la (Build_POb1 d (Lim l))) t).
(* Goal: @Equal (@Hom D d (@FOb C D G (@Lim J C H l))) (@ApAphi C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) (@ApAphi_inv C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) t)) (@ApAphi C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) (@Lim_diese J C H (@Lim J C H l) (@Limiting_cone J C H l) (@Prf_Islimit J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau))) *)
apply AphiPres; apply (Prf_limit2 l).
(* Goal: @Limit_eq J C H (@Lim J C H l) (@Limiting_cone J C H l) (@FOb D C (@Adjoint C D G la) d) (@Lp_sigma d tau) (@ApAphi_inv C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) t) *)
unfold Limit_eq in |- *; intro i.
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@ApAphi_inv C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) t) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)) (@ApNT J C (@Const J C (@FOb D C (@Adjoint C D G la) d)) H (@Lp_sigma d tau) i) *)
(* *) apply Trans with (ApAphi_inv la (t o FMor G (Limiting_cone l i))).
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@ApAphi_inv C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) t) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp D d (@FOb C D G (@Lim J C H l)) (@FOb C D G (@FOb J C H i)) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)))) *)
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp D d (@FOb C D G (@Lim J C H l)) (@FOb C D G (@FOb J C H i)) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)))) (@ApNT J C (@Const J C (@FOb D C (@Adjoint C D G la) d)) H (@Lp_sigma d tau) i) *)
apply Sym.
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp D d (@FOb C D G (@Lim J C H l)) (@FOb C D G (@FOb J C H i)) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)))) (@Comp C (@FOb D C (@Adjoint C D G la) d) (@Lim J C H l) (@FOb J C H i) (@ApAphi_inv C D (@Adjoint C D G la) G d (@Lim J C H l) (@Adj_l C D G la) t) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)) *)
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp D d (@FOb C D G (@Lim J C H l)) (@FOb C D G (@FOb J C H i)) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)))) (@ApNT J C (@Const J C (@FOb D C (@Adjoint C D G la) d)) H (@Lp_sigma d tau) i) *)
apply (Adj_eq5 la (Limiting_cone l i) t).
(* Goal: @Equal (@Hom C (@FOb D C (@Adjoint C D G la) d) (@FOb J C H i)) (@ApAphi_inv C D (@Adjoint C D G la) G d (@FOb J C H i) (@Adj_l C D G la) (@Comp D d (@FOb C D G (@Lim J C H l)) (@FOb C D G (@FOb J C H i)) t (@FMor C D G (@FOb J C (@Const J C (@Lim J C H l)) i) (@FOb J C H i) (@ApNT J C (@Const J C (@Lim J C H l)) H (@Limiting_cone J C H l) i)))) (@ApNT J C (@Const J C (@FOb D C (@Adjoint C D G la) d)) H (@Lp_sigma d tau) i) *)
simpl in |- *; unfold Lp_sigma_tau in |- *; apply Aphi_invPres; apply (H' i).
Qed.

Lemma Ladj_Pres1 : Preserves_1limit G l.
Proof.
(* Goal: @Preserves_1limit J C D H G l *)
apply (Build_IsLimit Lp_coUAlaw1 Lp_coUAlaw2).
Defined.

End ladj_pres.

(* Si G admet un adjoint, alors il Preserve toutes les Limites *)

Lemma Ladj_continuous :
 forall (C D : Category) (G : Functor C D), LeftAdj G -> Continuous G.
Proof.
(* Goal: forall (C D : Category) (G : Functor C D) (_ : @LeftAdj C D G), @Continuous C D G *)
unfold Continuous, Preserves_limits in |- *; intros C D G la J H l.
(* Goal: @Preserves_1limit J C D H G l *)
apply (Ladj_Pres1 la l).
Defined.





