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.
 unfold Map_law''0 in |- *; intros s1 s2 H.
 unfold SET_lcone_tau_fun in |- ×.
 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 :
 ∀ (i j : J) (g : i --> j) (tau : SET_lim),
 SET_lcone_tau j tau =_S FMor F g (SET_lcone_tau i tau).
Proof.
intros i j g sigma.
unfold SET_lcone_tau in |- *; simpl in |- *; unfold SET_lcone_tau_fun in |- ×.
apply (EqC sigma g Elt).
Qed.


 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.


   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.
   unfold Map_law in |- ×.
   intros a b; elim a; elim b; simpl in |- *; intro H.
   apply Refl.
   Qed.

   Canonical Structure SET_diese1_tau := Build_Map SET_diese1_tau_map_law.

   End set_diese1_tau_def.


  Lemma SET_diese1_tau_cone_law : Cone_law SET_diese1_tau.
  Proof.
  unfold Cone_law in |- *; intros i j g; simpl in |- ×.
  unfold Ext in |- *; simpl in |- ×.
  intro a; elim a; simpl in |- ×.
  unfold Comp_fun in |- *; simpl in |- ×.
  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.
 unfold Map_law0'' in |- *; intros x y H; simpl in |- ×.
 unfold Equal_NT, SET_diese1 in |- *; simpl in |- ×.
 unfold Ext in |- *; simpl in |- *; intros i a.
 elim a; simpl in |- ×.
 apply Pres1; trivial.
 Qed.

 Canonical Structure SET_diese := Build_Map0'' SET_diese_map_law.

 End set_diese.


Lemma SET_coUAlaw1 :
 ∀ (X : SET) (tau : Cone X F) (i : J) (x : X),
 tau i x =_S SET_lcone_tau i (SET_diese tau x).
Proof.
simpl in |- *; intros X tau i x.
unfold SET_lcone_tau_fun, SET_diese1 in |- *; simpl in |- ×.
apply Refl.
Qed.

Lemma SET_coUAlaw2 :
 ∀ (X : SET) (tau : Cone X F) (g : Map0'' X SET_lim),
 (∀ (i : J) (x : X), tau i x =_S SET_lcone_tau i (g x)) →
 ∀ x : X, g x =_S'' SET_diese tau x.
Proof.
intros X tau g H x; simpl in |- ×.
unfold Equal_NT in |- *; simpl in |- *; intro i; simpl in |- *;
 unfold Ext in |- *; simpl in |- ×.
intro e; elim e; simpl in |- ×.
apply Sym; apply (H i x).
Qed.

End set_c.