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


Require Export SET.
Require Export Single.
Require Export Limit.
Require Export Map0_dup1.

Set Implicit Arguments.
Unset Strict Implicit.

Section set_c.

Variables (J : Category) (F : Functor J SET).

Definition SET_lim := Cones Single F.

 Section set_lcone_tau_def.

 Variable i : J.

 Definition SET_lcone_tau_fun (sigma : SET_lim) := sigma i Elt.

 Lemma SET_lcone_tau_map_law : Map_law''0 SET_lcone_tau_fun.
 Proof.
(* Goal: @Map_law''0 SET_lim (@FOb J SET F i) SET_lcone_tau_fun *)
 unfold Map_law''0 in |- *; intros s1 s2 H.
(* Goal: @Equal (@FOb J SET F i) (SET_lcone_tau_fun s1) (SET_lcone_tau_fun s2) *)
 unfold SET_lcone_tau_fun in |- *.
(* Goal: @Equal (@FOb J SET F i) (@Ap (@FOb J SET (@Const J SET Single) i) (@FOb J SET F i) (@ApNT J SET (@Const J SET Single) F s1 i) Elt) (@Ap (@FOb J SET (@Const J SET Single) i) (@FOb J SET F i) (@ApNT J SET (@Const J SET Single) F s2 i) Elt) *)
 apply (H i Elt).
 Qed.

 Canonical Structure SET_lcone_tau := Build_Map''0 SET_lcone_tau_map_law.

 End set_lcone_tau_def.

Lemma SET_lcone_cone_law :
 forall (i j : J) (g : i --> j) (tau : SET_lim),
 SET_lcone_tau j tau =_S FMor F g (SET_lcone_tau i tau).
Proof.
(* Goal: forall (i j : Ob J) (g : Carrier (@Hom J i j)) (tau : Carrier'' SET_lim), @Equal (@FOb J SET F j) (@Ap''0 SET_lim (@FOb J SET F j) (SET_lcone_tau j) tau) (@Ap (@FOb J SET F i) (@FOb J SET F j) (@FMor J SET F i j g) (@Ap''0 SET_lim (@FOb J SET F i) (SET_lcone_tau i) tau)) *)
intros i j g sigma.
(* Goal: @Equal (@FOb J SET F i) (SET_lcone_tau_fun s1) (SET_lcone_tau_fun s2) *)
unfold SET_lcone_tau in |- *; simpl in |- *; unfold SET_lcone_tau_fun in |- *.
(* Goal: @Equal (@FOb J SET F j) (@Ap (@FOb J SET (@Const J SET Single) j) (@FOb J SET F j) (@ApNT J SET (@Const J SET Single) F sigma j) Elt) (@Ap (@FOb J SET F i) (@FOb J SET F j) (@FMor J SET F i j g) (@Ap (@FOb J SET (@Const J SET Single) i) (@FOb J SET F i) (@ApNT J SET (@Const J SET Single) F sigma i) Elt)) *)
apply (EqC sigma g Elt).
Qed.

(* construction tau# pour tout tau : DElta(X) -> F *)

 Section set_diese.

 Variables (X : SET) (tau : Cones X F).

  Section set_diese1_def.

  Variable x : X.

   Section set_diese1_tau_def.

   Variable i : J.

   (* (h(x)i)(Elt) =  tau(i)(x) *)

   Definition SET_diese1_tau_fun (a : Single) :=
     match a with
     | Elt => tau i x
     end.

   Lemma SET_diese1_tau_map_law : Map_law SET_diese1_tau_fun.
   Proof.
(* Goal: @Map_law Single (@FOb J SET F i) SET_diese1_tau_fun *)
   unfold Map_law in |- *.
(* Goal: forall (x y : Carrier Single) (_ : @Equal Single x y), @Equal (@FOb J SET F i) (SET_diese1_tau_fun x) (SET_diese1_tau_fun y) *)
   intros a b; elim a; elim b; simpl in |- *; intro H.
(* Goal: @Equal (@FOb J SET F i) (@Ap (@Const_ob J SET X i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x) (@Ap (@Const_ob J SET X i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x) *)
   apply Refl.
   Qed.

   Canonical Structure SET_diese1_tau := Build_Map SET_diese1_tau_map_law.
 
   End set_diese1_tau_def.

 (* h(x) : DElta({*}) -> F *)

  Lemma SET_diese1_tau_cone_law : Cone_law SET_diese1_tau.
  Proof.
(* Goal: @Cone_law J SET Single F SET_diese1_tau *)
  unfold Cone_law in |- *; intros i j g; simpl in |- *.
(* Goal: @Ext Single (@FOb J SET F j) (SET_diese1_tau j) (@Comp SET Single (@FOb J SET F i) (@FOb J SET F j) (SET_diese1_tau i) (@FMor J SET F i j g)) *)
  unfold Ext in |- *; simpl in |- *.
(* Goal: forall x : UnitType, @Equal (@FOb J SET F j) (SET_diese1_tau_fun j x) (@Comp_fun Single (@FOb J SET F i) (@FOb J SET F j) (SET_diese1_tau i) (@FMor J SET F i j g) x) *)
  intro a; elim a; simpl in |- *.
(* Goal: @Equal (@FOb J SET F j) (@Ap (@Const_ob J SET X j) (@FOb J SET F j) (@ApNT J SET (@Const J SET X) F tau j) x) (@Comp_fun Single (@FOb J SET F i) (@FOb J SET F j) (SET_diese1_tau i) (@FMor J SET F i j g) Elt) *)
  unfold Comp_fun in |- *; simpl in |- *.
(* Goal: @Equal (@FOb J SET F j) (@Ap (@Const_ob J SET X j) (@FOb J SET F j) (@ApNT J SET (@Const J SET X) F tau j) x) (@Ap (@FOb J SET F i) (@FOb J SET F j) (@FMor J SET F i j g) (@Ap (@Const_ob J SET X i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x)) *)
  apply (EqC tau g x).
  Qed.

  Definition SET_diese1 : SET_lim := Build_Cone SET_diese1_tau_cone_law.

  End set_diese1_def.

 Lemma SET_diese_map_law : Map_law0'' SET_diese1.
 Proof.
(* Goal: @Map_law0'' X SET_lim SET_diese1 *)
 unfold Map_law0'' in |- *; intros x y H; simpl in |- *.
(* Goal: @Equal_NT J SET (@Const J SET Single) F (SET_diese1 x) (SET_diese1 y) *)
 unfold Equal_NT, SET_diese1 in |- *; simpl in |- *.
(* Goal: forall a : Ob J, @Ext (@Const_ob J SET Single a) (@FOb J SET F a) (SET_diese1_tau x a) (SET_diese1_tau y a) *)
 unfold Ext in |- *; simpl in |- *; intros i a.
(* Goal: @Equal (@FOb J SET F i) (SET_diese1_tau_fun x i a) (SET_diese1_tau_fun y i a) *)
 elim a; simpl in |- *.
(* Goal: @Equal (@FOb J SET F i) (@Ap (@Const_ob J SET X i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x) (@Ap (@Const_ob J SET X i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) y) *)
 apply Pres1; trivial.
 Qed.

 Canonical Structure SET_diese := Build_Map0'' SET_diese_map_law.

 End set_diese.
 
(* universalite' *)

Lemma SET_coUAlaw1 :
 forall (X : SET) (tau : Cone X F) (i : J) (x : X),
 tau i x =_S SET_lcone_tau i (SET_diese tau x).
Proof.
(* Goal: forall (X : Ob SET) (tau : @Cone J SET X F) (i : Ob J) (x : Carrier X), @Equal (@FOb J SET F i) (@Ap (@FOb J SET (@Const J SET X) i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x) (@Ap''0 SET_lim (@FOb J SET F i) (SET_lcone_tau i) (@Ap0'' X SET_lim (@SET_diese X tau) x)) *)
simpl in |- *; intros X tau i x.
(* Goal: @Equal (@FOb J SET F i) (@Ap (@Const_ob J SET X i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x) (SET_lcone_tau_fun i (@SET_diese1 X tau x)) *)
unfold SET_lcone_tau_fun, SET_diese1 in |- *; simpl in |- *.
(* Goal: @Equal (@FOb J SET F i) (@Ap (@Const_ob J SET X i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x) (@Ap (@Const_ob J SET X i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x) *)
apply Refl.
Qed.

Lemma SET_coUAlaw2 :
 forall (X : SET) (tau : Cone X F) (g : Map0'' X SET_lim),
 (forall (i : J) (x : X), tau i x =_S SET_lcone_tau i (g x)) ->
 forall x : X, g x =_S'' SET_diese tau x.
Proof.
(* Goal: forall (X : Ob SET) (tau : @Cone J SET X F) (g : Map0'' X SET_lim) (_ : forall (i : Ob J) (x : Carrier X), @Equal (@FOb J SET F i) (@Ap (@FOb J SET (@Const J SET X) i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x) (@Ap''0 SET_lim (@FOb J SET F i) (SET_lcone_tau i) (@Ap0'' X SET_lim g x))) (x : Carrier X), @Equal'' SET_lim (@Ap0'' X SET_lim g x) (@Ap0'' X SET_lim (@SET_diese X tau) x) *)
intros X tau g H x; simpl in |- *.
unfold Equal_NT in |- *; simpl in |- *; intro i; simpl in |- *;
(* Goal: @Ext Single (@FOb J SET F j) (SET_diese1_tau j) (@Comp SET Single (@FOb J SET F i) (@FOb J SET F j) (SET_diese1_tau i) (@FMor J SET F i j g)) *)
 unfold Ext in |- *; simpl in |- *.
(* Goal: forall x0 : UnitType, @Equal (@FOb J SET F i) (@Ap (@Const_ob J SET Single i) (@FOb J SET F i) (@ApNT J SET (@Const J SET Single) F (@Ap0'' X SET_lim g x) i) x0) (@SET_diese1_tau_fun X tau x i x0) *)
intro e; elim e; simpl in |- *.
(* Goal: @Equal (@FOb J SET F i) (@Ap (@Const_ob J SET Single i) (@FOb J SET F i) (@ApNT J SET (@Const J SET Single) F (@Ap0'' X SET_lim g x) i) Elt) (@Ap (@Const_ob J SET X i) (@FOb J SET F i) (@ApNT J SET (@Const J SET X) F tau i) x) *)
apply Sym; apply (H i x).
Qed.

End set_c.