(* 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        *)
(*****************************************************************************)
(*									     *)
(*	             HomFoncteur  Hom(a,-) is Complete        		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)


Require Export HomFunctor.
Require Export Pres_Limits.

Set Implicit Arguments.
Unset Strict Implicit.

(* exemple : les Hom-Foncteurs preservent toutes les Limites *)

Section funset_pres.

Variables (J C : Category) (F : Functor J C) (l : Limit F) (c : C).

Definition FS_lim := c --> Lim l.

Definition FS_lcone := Limiting_cone l o_C FunSET c.

 Section fs_diese.

(* soit X un setoid, soit tau : cone(X,FoH) (i.e. Delta(X) -> FoH) 
   pour tout x:|X|, nous construisons un 
   Tx : cone(c,F) (i.e. Delta(c) -> F)
   telque Tx(i) = tau(i)(x) *)

 Variables (X : SET) (tau : Cone X (F o_F FunSET c)).

  Section fs_diese_mor_def.

  Variable x : X.

  Definition FS_cone_tau (i : J) := tau i x.

  (* revient a` prouver: tau(j)(x) = tau(i)(x) o Fg *)
  (* s'obtient apre`s simplification de Eq_cone sur tau *)

  Lemma FS_cone_tau_cone_law : Cone_law FS_cone_tau.
  Proof.
(* Goal: @Cone_law J C c F FS_cone_tau *)
  unfold Cone_law, FS_cone_tau in |- *.
(* Goal: forall (i j : Ob J) (g : Carrier (@Hom J i j)), @Equal (@Hom C c (@FOb J C F j)) (@Ap (@FOb J SET (@Const J SET X) j) (@FOb J SET (@Comp_Functor J C SET F (@FunSET C c)) j) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau j) x) (@Comp C c (@FOb J C F i) (@FOb J C F j) (@Ap (@FOb J SET (@Const J SET X) i) (@FOb J SET (@Comp_Functor J C SET F (@FunSET C c)) i) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) x) (@FMor J C F i j g)) *)
  intros i j g.
(* Goal: @Equal (@Hom C c (@FOb J C F j)) (@Ap (@FOb J SET (@Const J SET X) j) (@FOb J SET (@Comp_Functor J C SET F (@FunSET C c)) j) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau j) x) (@Comp C c (@FOb J C F i) (@FOb J C F j) (@Ap (@FOb J SET (@Const J SET X) i) (@FOb J SET (@Comp_Functor J C SET F (@FunSET C c)) i) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) x) (@FMor J C F i j g)) *)
  apply (EqC tau g x).
  Qed.

  Definition FS_cone := Build_Cone FS_cone_tau_cone_law.

 (* soit X un setoid, soit tau : cone(X,FoH) (i.e. Delta(X) -> FoH) 
    construisons tau# : X -> C(c,(Lim F))
    de'finissons tau#(x) par (Tx)# car l est une (Limit F) *)

  Definition FS_diese_mor := Lim_diese l FS_cone.

  End fs_diese_mor_def.  

 Lemma FS_diese_map_law : Map_law FS_diese_mor.
 Proof.
(* Goal: @Map_law X (@Hom C c (@Lim J C F l)) FS_diese_mor *)
 unfold Map_law in |- *; intros x y H.
(* Goal: @Equal (@Hom C c (@Lim J C F l)) (FS_diese_mor x) (FS_diese_mor y) *)
 unfold FS_diese_mor in |- *.
(* Goal: @Equal (@Hom C c (@Lim J C F l)) (@Lim_diese J C F (@Lim J C F l) (@Limiting_cone J C F l) (@Prf_Islimit J C F l) c (FS_cone x)) (@Lim_diese J C F (@Lim J C F l) (@Limiting_cone J C F l) (@Prf_Islimit J C F l) c (FS_cone y)) *)
 apply (Ldiese_map l).
(* Goal: @Equal_NT J C (@Const J C c) F (FS_cone x) (FS_cone y) *)
 simpl in |- *; unfold Equal_NT in |- *; intro i; simpl in |- *.
(* Goal: @Equal (@Hom C (@Const_ob J C c i) (@FOb J C F i)) (FS_cone_tau x i) (FS_cone_tau y i) *)
 unfold FS_cone_tau in |- *.
(* Goal: @Equal (@Hom C (@Const_ob J C c i) (@FOb J C F i)) (@Ap (@FOb J SET (@Const J SET X) i) (@FOb J SET (@Comp_Functor J C SET F (@FunSET C c)) i) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) x) (@Ap (@FOb J SET (@Const J SET X) i) (@FOb J SET (@Comp_Functor J C SET F (@FunSET C c)) i) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) y) *)
 apply Pres1; assumption.
 Qed.

 Canonical Structure FS_diese := Build_Map FS_diese_map_law.

End fs_diese.

(* ve'rifions que le # qu'on vient de construire peut former
   un (co)universal arrow *)
(* revient a` prouver: 
   qq X un setoid, qq tau : cone(X,FoH) (i.e. Delta(X) -> FoH) 
   qq i : J, qq x : |X|.
   tau(i)(x) = tau#(x) o mu(i) 
   i.e. Tx(i) = (Tx)# o mu(i)  qui n'est rien d'autre que eq_Ucone 
                               pour le cone Tx *)

Lemma FS_limit1 : Limit_law1 FS_lcone FS_diese.
Proof.
(* Goal: @Limit_law1 J SET (@Comp_Functor J C SET F (@FunSET C c)) (@FOb C SET (@FunSET C c) (@Lim J C F l)) FS_lcone FS_diese *)
unfold Limit_law1, Limit_eq in |- *; simpl in |- *.
(* Goal: forall (c0 : Setoid) (tau : @Cone J SET c0 (@Comp_Functor J C SET F (@FunSET C c))) (i : Ob J), @Ext c0 (@FunSET_ob C c (@FOb J C F i)) (@Comp SET c0 (@FunSET_ob C c (@Lim J C F l)) (@FunSET_ob C c (@FOb J C F i)) (@FS_diese c0 tau) (@Comp_cone_tau J C SET (@Lim J C F l) F (@Limiting_cone J C F l) (@FunSET C c) i)) (@ApNT J SET (@Const J SET c0) (@Comp_Functor J C SET F (@FunSET C c)) tau i) *)
intros X tau i.
(* Goal: @Ext X (@FunSET_ob C c (@FOb J C F i)) (@Comp SET X (@FunSET_ob C c (@Lim J C F l)) (@FunSET_ob C c (@FOb J C F i)) (@FS_diese X tau) (@Comp_cone_tau J C SET (@Lim J C F l) F (@Limiting_cone J C F l) (@FunSET C c) i)) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) *)
unfold Ext in |- *; intro x.
(* Goal: @Equal (@FunSET_ob C c (@FOb J C F i)) (@Ap X (@FunSET_ob C c (@FOb J C F i)) (@Comp SET X (@FunSET_ob C c (@Lim J C F l)) (@FunSET_ob C c (@FOb J C F i)) (@FS_diese X tau) (@Comp_cone_tau J C SET (@Lim J C F l) F (@Limiting_cone J C F l) (@FunSET C c) i)) x) (@Ap X (@FunSET_ob C c (@FOb J C F i)) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) x) *)
unfold Comp_cone in |- *; simpl in |- *.
(* Goal: @Equal (@FunSET_ob C c (@FOb J C F i)) (@FunSET_mor1 C c (@Const_ob J C (@Lim J C F l) i) (@FOb J C F i) (@ApNT J C (@Const J C (@Lim J C F l)) F (@Limiting_cone J C F l) i) (@FS_diese_mor X tau x)) (@Ap X (@FunSET_ob C c (@FOb J C F i)) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) x) *)
unfold FunSET_mor1, FS_diese_mor in |- *; simpl in |- *.
(* Goal: @Equal (@FunSET_ob C c (@FOb J C F i)) (@Comp C c (@Const_ob J C (@Lim J C F l) i) (@FOb J C F i) (@Lim_diese J C F (@Lim J C F l) (@Limiting_cone J C F l) (@Prf_Islimit J C F l) c (@FS_cone X tau x)) (@ApNT J C (@Const J C (@Lim J C F l)) F (@Limiting_cone J C F l) i)) (@Ap X (@FunSET_ob C c (@FOb J C F i)) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) x) *)
apply (Prf_limit1 l (FS_cone tau x) i).
Qed.

(* revient a` prouver que:
   f(x) o mu(i) = (Tx)i  =>
   f(x) = (Tx)#
   correspondant a` l'axiome d'universalite' de l *)
   
Lemma FS_limit2 : Limit_law2 FS_lcone FS_diese.
Proof.
(* Goal: @Limit_law2 J SET (@Comp_Functor J C SET F (@FunSET C c)) (@FOb C SET (@FunSET C c) (@Lim J C F l)) FS_lcone FS_diese *)
unfold Limit_law2 in |- *; intros X tau f.
(* Goal: forall _ : @Limit_eq J SET (@Comp_Functor J C SET F (@FunSET C c)) (@FOb C SET (@FunSET C c) (@Lim J C F l)) FS_lcone X tau f, @Equal (@Hom SET X (@FOb C SET (@FunSET C c) (@Lim J C F l))) f (@FS_diese X tau) *)
unfold Limit_eq, FS_diese in |- *; simpl in |- *.
(* Goal: forall _ : forall i : Ob J, @Ext X (@FunSET_ob C c (@FOb J C F i)) (@Comp SET X (@FunSET_ob C c (@Lim J C F l)) (@FunSET_ob C c (@FOb J C F i)) f (@Comp_cone_tau J C SET (@Lim J C F l) F (@Limiting_cone J C F l) (@FunSET C c) i)) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i), @Ext X (@FunSET_ob C c (@Lim J C F l)) f (@Build_Map X (@Hom C c (@Lim J C F l)) (@FS_diese_mor X tau) (@FS_diese_map_law X tau)) *)
unfold Ext in |- *; simpl in |- *.
(* Goal: forall (_ : forall (i : Ob J) (x : Carrier X), @Equal (@FunSET_ob C c (@FOb J C F i)) (@FunSET_mor1 C c (@Const_ob J C (@Lim J C F l) i) (@FOb J C F i) (@ApNT J C (@Const J C (@Lim J C F l)) F (@Limiting_cone J C F l) i) (@Ap X (@FunSET_ob C c (@Lim J C F l)) f x)) (@Ap X (@FunSET_ob C c (@FOb J C F i)) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) x)) (x : Carrier X), @Equal (@FunSET_ob C c (@Lim J C F l)) (@Ap X (@FunSET_ob C c (@Lim J C F l)) f x) (@FS_diese_mor X tau x) *)
unfold FunSET_mor1, FS_diese_mor in |- *.
(* Goal: forall (_ : forall (i : Ob J) (x : Carrier X), @Equal (@FunSET_ob C c (@FOb J C F i)) (@Comp C c (@Const_ob J C (@Lim J C F l) i) (@FOb J C F i) (@Ap X (@FunSET_ob C c (@Lim J C F l)) f x) (@ApNT J C (@Const J C (@Lim J C F l)) F (@Limiting_cone J C F l) i)) (@Ap X (@FunSET_ob C c (@FOb J C F i)) (@ApNT J SET (@Const J SET X) (@Comp_Functor J C SET F (@FunSET C c)) tau i) x)) (x : Carrier X), @Equal (@FunSET_ob C c (@Lim J C F l)) (@Ap X (@FunSET_ob C c (@Lim J C F l)) f x) (@Lim_diese J C F (@Lim J C F l) (@Limiting_cone J C F l) (@Prf_Islimit J C F l) c (@FS_cone X tau x)) *)
intros H x.
(* Goal: @Equal (@FunSET_ob C c (@Lim J C F l)) (@Ap X (@FunSET_ob C c (@Lim J C F l)) f x) (@Lim_diese J C F (@Lim J C F l) (@Limiting_cone J C F l) (@Prf_Islimit J C F l) c (@FS_cone X tau x)) *)
unfold FunSET_ob in |- *.
(* Goal: @Equal (@Hom C c (@Lim J C F l)) (@Ap X (@Hom C c (@Lim J C F l)) f x) (@Lim_diese J C F (@Lim J C F l) (@Limiting_cone J C F l) (@Prf_Islimit J C F l) c (@FS_cone X tau x)) *)
apply (Prf_limit2 l).
(* Goal: @Limit_eq J C F (@Lim J C F l) (@Limiting_cone J C F l) c (@FS_cone X tau x) (@Ap X (@Hom C c (@Lim J C F l)) f x) *)
unfold Limit_eq in |- *; simpl in |- *.
(* Goal: forall i : Ob J, @Equal (@Hom C c (@FOb J C F i)) (@Comp C c (@Lim J C F l) (@FOb J C F i) (@Ap X (@Hom C c (@Lim J C F l)) f x) (@ApNT J C (@Const J C (@Lim J C F l)) F (@Limiting_cone J C F l) i)) (@FS_cone_tau X tau x i) *)
intro i; apply (H i x).
Qed.

Lemma FunSET_Preserves_l : Preserves_1limit (FunSET c) l.
Proof.
(* Goal: @Preserves_1limit J C SET F (@FunSET C c) l *)
exact (Build_IsLimit FS_limit1 FS_limit2).
Defined.

End funset_pres.


(* on en d'eduit que C(c,-) Preserve toutes les Limites *)

Lemma FunSET_continuous :
 forall (C : Category) (c : C), Continuous (FunSET c). 
Proof.
(* Goal: forall (C : Category) (c : Ob C), @Continuous C SET (@FunSET C c) *)
unfold Continuous, Preserves_limits in |- *; intros C c J F l.
(* Goal: @Preserves_1limit J C SET F (@FunSET C c) l *)
exact (FunSET_Preserves_l l c).
Defined.
