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


Require Export Limit.
Require Export Discr.
Require Export Products.

Set Implicit Arguments.
Unset Strict Implicit.

(* Foncteur de I~ (cate'gorie discrete obtenue a` partir de I) vers C *)

Section products_limit_def.

Variables (C : Category) (I : Type) (a : I -> C).

Definition FunDiscr_ob (i : Discr I) := a i.

Definition FunDiscr_arrow (i j : Discr I) (f : i --> j) :=
  match f in (Discr_mor d d0) return (Carrier (a d --> a d0)) with
  | Build_Discr_mor k => Id (a k)
  end.

Lemma FunDiscr_map_law :
 forall i j : I, Map_law (FunDiscr_arrow (i:=i) (j:=j)).
Proof.
(* Goal: forall i j : I, @Map_law (@Hom (Discr I) i j) (@Hom C (a i) (a j)) (@FunDiscr_arrow i j) *)
unfold Map_law in |- *.
(* Goal: forall (i j : I) (x y : Carrier (@Hom (Discr I) i j)) (_ : @Equal (@Hom (Discr I) i j) x y), @Equal (@Hom C (a i) (a j)) (@FunDiscr_arrow i j x) (@FunDiscr_arrow i j y) *)
intros i j f; elim f; intros k f1 H.
apply
 (Discr_mor_ind1
    (P:=fun f1 : Discr_mor k k =>
        FunDiscr_arrow (Build_Discr_mor k) =_S FunDiscr_arrow f1)).
(* Goal: @Equal (@Hom C (a k) (a k)) (@FunDiscr_arrow k k (@Build_Discr_mor I k)) (@FunDiscr_arrow k k (@Build_Discr_mor I k)) *)
simpl in |- *; apply Refl.
Qed.

Canonical Structure FunDiscr_map (i j : Discr I) :=
  Build_Map (FunDiscr_map_law (i:=i) (j:=j)).

Lemma FunDiscr_comp_law : Fcomp_law FunDiscr_map.
Proof.
(* Goal: @Fcomp_law (Discr I) C a FunDiscr_map *)
unfold Fcomp_law in |- *; intros i j k f.
(* Goal: forall g : Carrier (@Hom (Discr I) j k), @Equal (@Hom C (a i) (a k)) (@Ap (@Hom (Discr I) i k) (@Hom C (a i) (a k)) (FunDiscr_map i k) (@Comp (Discr I) i j k f g)) (@Comp C (a i) (a j) (a k) (@Ap (@Hom (Discr I) i j) (@Hom C (a i) (a j)) (FunDiscr_map i j) f) (@Ap (@Hom (Discr I) j k) (@Hom C (a j) (a k)) (FunDiscr_map j k) g)) *)
elim f; simpl in |- *.
(* Goal: forall (a0 : I) (g : @Discr_mor I a0 k), @Equal (@Hom C (a a0) (a k)) (@FunDiscr_arrow a0 k (@Comp (Discr I) a0 a0 k (@Build_Discr_mor I a0) g)) (@Comp C (a a0) (a a0) (a k) (@Id C (a a0)) (@FunDiscr_arrow a0 k g)) *)
intros i' g; elim g; simpl in |- *.
(* Goal: forall a0 : I, @Equal (@Hom C (a a0) (a a0)) (@Id C (a a0)) (@Comp C (a a0) (a a0) (a a0) (@Id C (a a0)) (@Id C (a a0))) *)
intro i''; unfold Comp in |- *; apply (Prf_idr (c:=C)).
Qed.

Lemma FunDiscr_id_law : Fid_law FunDiscr_map.
Proof.
(* Goal: @Fid_law (Discr I) C a FunDiscr_map *)
unfold Fid_law in |- *; simpl in |- *.
(* Goal: forall a0 : I, @Equal (@Hom C (a a0) (a a0)) (@Id C (a a0)) (@Id C (a a0)) *)
intro i; apply Refl.
Qed.

Canonical Structure FunDiscr :=
  Build_Functor FunDiscr_comp_law FunDiscr_id_law.

(* produit d'une famille d'objets *)

SubClass Product1 := Limit FunDiscr.

Variable l : Product1.

(* ||ai *)

Definition Pi1 := Lim l.

(* pi : ||ai -> ai *)

Definition Proj1 (i : I) : Pi1 --> a i := Limiting_cone l i.

(* construire a` partir d'une famille fj:c->ai, une NT tau:Delta(c)->F *)

 Section pd1_diese_def.

 Variables (c : C) (f : forall j : I, c --> FunDiscr j).

 Definition Product_tau (j : Discr I) := f j.

 Lemma Product_tau_cone_law : Cone_law Product_tau.
 Proof.
(* Goal: @Cone_law (Discr I) C c FunDiscr Product_tau *)
 unfold Cone_law, Product_tau in |- *; simpl in |- *.
(* Goal: forall (i j : I) (g : @Discr_mor I i j), @Equal (@Hom C c (a j)) (f j) (@Comp C c (a i) (a j) (f i) (@FMor (Discr I) C FunDiscr i j g)) *)
 intros a' b g; elim g; simpl in |- *; intro i.
(* Goal: @Equal (@Hom C c (a i)) (f i) (@Comp C c (a i) (a i) (f i) (@FMor (Discr I) C FunDiscr i i (@Build_Discr_mor I i))) *)
 unfold FMor in |- *; simpl in |- *.
(* Goal: @Equal (@Hom C c (a i)) (f i) (@Comp C c (a i) (a i) (f i) (@Id C (a i))) *)
 apply Idr.
 Qed.

 Definition Product_nt := Build_Cone Product_tau_cone_law.

 Definition Pd1_diese : c --> Pi1 := Lim_diese l Product_nt.

 End pd1_diese_def.

Lemma Prf_pd1_law1 : Product_law1 Proj1 Pd1_diese.
Proof.
(* Goal: @Product_law1 C I a Pi1 Proj1 Pd1_diese *)
unfold Product_law1, Product_eq in |- *; intros c f j.
(* Goal: @Equal (@Hom C c (a j)) (f j) (@Comp C c Pi1 (a j) (@Pd1_diese c f) (Proj1 j)) *)
apply Sym; apply (Prf_limit1 l (Product_nt f) j).
Qed.

Lemma Prf_pd1_law2 : Product_law2 Proj1 Pd1_diese.
Proof.
(* Goal: @Product_law2 C I a Pi1 Proj1 Pd1_diese *)
unfold Product_law2, Product_eq in |- *; intros c f g H.
(* Goal: @Equal (@Hom C c Pi1) g (@Pd1_diese c f) *)
unfold Pd1_diese in |- *; apply (Prf_limit2 l).

unfold Limit_eq in |- *; simpl in |- *; unfold Product_tau in |- *;
 simpl in |- *.
(* Goal: forall i : I, @Equal (@Hom C c (a i)) (@Comp C c (@Lim (Discr I) C FunDiscr l) (a i) g (@ApNT (Discr I) C (@Const (Discr I) C (@Lim (Discr I) C FunDiscr l)) FunDiscr (@Limiting_cone (Discr I) C FunDiscr l) i)) (f i) *)
intro i; apply Sym; apply (H i).
Qed.

Canonical Structure Product1_to_Product :=
  Build_Product Prf_pd1_law1 Prf_pd1_law2.

End products_limit_def.

Coercion Product1_to_Product : Product1 >-> Product.



