proposition: Lemma FunSET_continuous : forall (C : Category) (c : C), Continuous (FunSET c).
proof: Proof. unfold Continuous, Preserves_limits in |- *; intros C c J F l. exact (FunSET_Preserves_l l c). Defined.
imports: HomFunctor Pres_Limits