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

Require Export Pullbacks.
Require Export Setoid_prop.
Require Export SET.
Require Export SetoidPROD.

Set Implicit Arguments.
Unset Strict Implicit.

Section s_pulb_def.

Variables (A B C : Setoid) (f : Map A B) (g : Map C B).

Definition S_pulb_pred (axc : SPROD A C) :=
  f (Sprod_l axc) =_S g (Sprod_r axc).

Lemma S_pulb_reg : Reg_law S_pulb_pred.
Proof.
(* Goal: @Reg_law (SPROD A C) S_pulb_pred *)
unfold Reg_law, S_pulb_pred in |- *; intros a1xc1 a2xc2 H1 H2.
(* Goal: @Equal B (@Ap A B f (@Sprod_l A C a2xc2)) (@Ap C B g (@Sprod_r A C a2xc2)) *)
elim H1; intros H3 H4.
(* Goal: @Equal B (@Ap A B f (@Sprod_l A C a2xc2)) (@Ap C B g (@Sprod_r A C a2xc2)) *)
apply Trans with (f (Sprod_l a1xc1)).
(* Goal: @Equal B (@Ap A B f (@Sprod_l A C a2xc2)) (@Ap A B f (@Sprod_l A C a1xc1)) *)
(* Goal: @Equal B (@Ap A B f (@Sprod_l A C a1xc1)) (@Ap C B g (@Sprod_r A C a2xc2)) *)
apply Pres1; apply Sym; assumption.
(* Goal: @Equal B (@Ap A B f (@Sprod_l A C a1xc1)) (@Ap C B g (@Sprod_r A C a2xc2)) *)
apply Trans with (g (Sprod_r a1xc1)).
(* Goal: @Equal B (@Ap A B f (@Sprod_l A C a1xc1)) (@Ap C B g (@Sprod_r A C a1xc1)) *)
(* Goal: @Equal B (@Ap C B g (@Sprod_r A C a1xc1)) (@Ap C B g (@Sprod_r A C a2xc2)) *)
assumption.
(* Goal: @Equal B (@Ap A B f (@Sprod_l A C a1xc1)) (@Ap C B g (@Sprod_r A C a1xc1)) *)
(* Goal: @Equal B (@Ap C B g (@Sprod_r A C a1xc1)) (@Ap C B g (@Sprod_r A C a2xc2)) *)
apply Pres1; assumption.
Qed.

Canonical Structure S_pulb_constr := Build_Setoid_pred S_pulb_reg.

Definition S_pulb_prod := SubSetoid S_pulb_constr.

Definition S_pulb_p := RestrictedMap (Proj1_SPROD A C) S_pulb_constr.

Definition S_pulb_q := RestrictedMap (Proj2_SPROD A C) S_pulb_constr.

Lemma S_pulb_law1 : Pullback_law1 f g S_pulb_p S_pulb_q.
Proof.
(* Goal: @Pullback_law1 SET A B C f g (@SubSetoid (SPROD A C) S_pulb_constr) S_pulb_p S_pulb_q *)
unfold Pullback_law1, Pullback_eq1 in |- *; simpl in |- *.
unfold Ext in |- *; simpl in |- *; intro x; elim x; unfold Comp_fun in |- *;
 simpl in |- *.
(* Goal: forall (Elt_sub : Sprod A C) (_ : S_pulb_pred Elt_sub), @Equal B (@Ap A B f (@Sprod_l A C Elt_sub)) (@Ap C B g (@Sprod_r A C Elt_sub)) *)
trivial.
Qed.

 Section s_pulb_diese_def.

 Variables (D : Setoid) (t1 : Map D A) (t2 : Map D C).
 Hypothesis H : Pullback_eq1 f g t1 t2.
 
 Lemma Check_S_pulb_constr :
  forall d : D, S_pulb_constr (Build_Sprod (t1 d) (t2 d)).
 Proof.
(* Goal: forall d : Carrier D, @Pred (SPROD A C) S_pulb_constr (@Build_Sprod A C (@Ap D A t1 d) (@Ap D C t2 d)) *)
 intro d; exact (H d).
 Qed. 

 Canonical Structure S_pulb_fun (d : D) :=
   Build_SubType (Check_S_pulb_constr d).
 
 Lemma S_pulb_map_law : Map_law S_pulb_fun.
 Proof. 
 unfold Map_law in |- *; simpl in |- *; unfold Equal_Sprod in |- *;
  simpl in |- *.
(* Goal: forall (Elt_sub : Sprod A C) (_ : S_pulb_pred Elt_sub), @Equal B (@Ap A B f (@Sprod_l A C Elt_sub)) (@Ap C B g (@Sprod_r A C Elt_sub)) *)
 intros x y H1; split; apply Pres1; trivial.
 Qed.

 Canonical Structure S_pulb_diese := Build_Map S_pulb_map_law.

 End s_pulb_diese_def.

Lemma S_pulb_law2 : Pullback_law2 S_pulb_p S_pulb_diese.
Proof.
(* Goal: @Pullback_law2 SET A B C f g (@SubSetoid (SPROD A C) S_pulb_constr) S_pulb_p S_pulb_diese *)
unfold Pullback_law2, Pullback_eq2 in |- *; simpl in |- *.
(* Goal: forall (r : Setoid) (t1 : Map r A) (t2 : Map r C) (pe : @Pullback_eq1 SET A B C f g r t1 t2), @Ext r C t2 (@Comp SET r (@SubSetoid (SPROD A C) S_pulb_constr) C (@S_pulb_diese r t1 t2 pe) S_pulb_q) *)
unfold Ext in |- *; simpl in |- *; intros; simpl in |- *.
(* Goal: @Equal C (@Ap r C t2 x) (@Ap r C t2 x) *)
apply Refl.
Qed.

Lemma S_pulb_law3 : Pullback_law3 S_pulb_q S_pulb_diese.
Proof.
(* Goal: @Pullback_law3 SET A B C f g (@SubSetoid (SPROD A C) S_pulb_constr) S_pulb_q S_pulb_diese *)
unfold Pullback_law3, Pullback_eq2 in |- *; simpl in |- *.
(* Goal: forall (r : Setoid) (t1 : Map r A) (t2 : Map r C) (pe : @Pullback_eq1 SET A B C f g r t1 t2), @Ext r C t2 (@Comp SET r (@SubSetoid (SPROD A C) S_pulb_constr) C (@S_pulb_diese r t1 t2 pe) S_pulb_q) *)
unfold Ext in |- *; simpl in |- *; intros; simpl in |- *.
(* Goal: @Equal C (@Ap r C t2 x) (@Ap r C t2 x) *)
apply Refl.
Qed.

Lemma S_pulb_law4 : Pullback_law4 S_pulb_p S_pulb_q S_pulb_diese.
Proof.
(* Goal: @Pullback_law4 SET A B C f g (@SubSetoid (SPROD A C) S_pulb_constr) S_pulb_p S_pulb_q S_pulb_diese *)
unfold Pullback_law4, Pullback_eq2 in |- *; simpl in |- *.
(* Goal: forall (r : Setoid) (t1 : Map r A) (t2 : Map r C) (pe : @Pullback_eq1 SET A B C f g r t1 t2) (g : Map r (@SubSetoid (SPROD A C) S_pulb_constr)) (_ : @Ext r A t1 (@Comp SET r (@SubSetoid (SPROD A C) S_pulb_constr) A g S_pulb_p)) (_ : @Ext r C t2 (@Comp SET r (@SubSetoid (SPROD A C) S_pulb_constr) C g S_pulb_q)), @Ext r (@SubSetoid (SPROD A C) S_pulb_constr) g (@S_pulb_diese r t1 t2 pe) *)
unfold Ext in |- *; simpl in |- *; intros D t1 t2 H h H1 H2 x.
(* Goal: @Equal_Sprod A C (@Elt_sub (SPROD A C) S_pulb_constr (@Ap D (@SubSetoid (SPROD A C) S_pulb_constr) h x)) (@Build_Sprod A C (@Ap D A t1 x) (@Ap D C t2 x)) *)
unfold Equal_Sprod in |- *; simpl in |- *; split.
(* Goal: @Equal A (@Sprod_l A C (@Elt_sub (SPROD A C) S_pulb_constr (@Ap D (@SubSetoid (SPROD A C) S_pulb_constr) h x))) (@Ap D A t1 x) *)
(* Goal: @Equal C (@Sprod_r A C (@Elt_sub (SPROD A C) S_pulb_constr (@Ap D (@SubSetoid (SPROD A C) S_pulb_constr) h x))) (@Ap D C t2 x) *)
apply Sym; apply H1.
(* Goal: @Equal C (@Sprod_r A C (@Elt_sub (SPROD A C) S_pulb_constr (@Ap D (@SubSetoid (SPROD A C) S_pulb_constr) h x))) (@Ap D C t2 x) *)
apply Sym; apply H2.
Qed.

Canonical Structure S_pulb :=
  Build_Pullback S_pulb_law1 S_pulb_law2 S_pulb_law3 S_pulb_law4.

End s_pulb_def.



