Require Export HomFunctor.
Require Export Pres_Limits.

Set Implicit Arguments.
Unset Strict Implicit.


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.


 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.


  Lemma FS_cone_tau_cone_law : Cone_law FS_cone_tau.
  Proof.
  unfold Cone_law, FS_cone_tau in |- ×.
  intros i j g.
  apply (EqC tau g x).
  Qed.

  Definition FS_cone := Build_Cone FS_cone_tau_cone_law.


  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.
 unfold Map_law in |- *; intros x y H.
 unfold FS_diese_mor in |- ×.
 apply (Ldiese_map l).
 simpl in |- *; unfold Equal_NT in |- *; intro i; simpl in |- ×.
 unfold FS_cone_tau in |- ×.
 apply Pres1; assumption.
 Qed.

 Canonical Structure FS_diese := Build_Map FS_diese_map_law.

End fs_diese.


Lemma FS_limit1 : Limit_law1 FS_lcone FS_diese.
Proof.
unfold Limit_law1, Limit_eq in |- *; simpl in |- ×.
intros X tau i.
unfold Ext in |- *; intro x.
unfold Comp_cone in |- *; simpl in |- ×.
unfold FunSET_mor1, FS_diese_mor in |- *; simpl in |- ×.
apply (Prf_limit1 l (FS_cone tau x) i).
Qed.


Lemma FS_limit2 : Limit_law2 FS_lcone FS_diese.
Proof.
unfold Limit_law2 in |- *; intros X tau f.
unfold Limit_eq, FS_diese in |- *; simpl in |- ×.
unfold Ext in |- *; simpl in |- ×.
unfold FunSET_mor1, FS_diese_mor in |- ×.
intros H x.
unfold FunSET_ob in |- ×.
apply (Prf_limit2 l).
unfold Limit_eq in |- *; simpl in |- ×.
intro i; apply (H i x).
Qed.

Lemma FunSET_Preserves_l : Preserves_1limit (FunSET c) l.
Proof.
exact (Build_IsLimit FS_limit1 FS_limit2).
Defined.

End funset_pres.


Lemma FunSET_continuous :
 ∀ (C : Category) (c : C), Continuous (FunSET c).
Proof.
unfold Continuous, Preserves_limits in |- *; intros C c J F l.
exact (FunSET_Preserves_l l c).
Defined.